Re: BLD issue: non-disjointness of internal and external predicate symbols

The principle was the easy of interfacing with FOL, as far as I remember. I see
no good argument for the principle "one constant - one meaning". Especially now
when OWL seems to be ditching it.
But I am ok with separating them. It is just a bad and unnecessary kludge.
Since we distinguish External(p) from p, it is just the same as having a
separate symbol space, esternalIRI. We could have used, for example,
p^^iri and p^^esternalIRI. But you wanted Builtin(...) which later became
External(...).


	--michael  

On Thu, 10 Jul 2008 17:32:36 +0200
Jos de Bruijn <debruijn@inf.unibz.it> wrote:

> Michael,
> 
> My argument is not about error-checking, but rather about the principle 
> that the same constant you use in different places should mean the same 
> thing.
> 
> But I'm also willing to compromise for the case of external frames, so 
> the compromise would be:
> 
> - we create additional sets for external functions and predicates that 
> are disjoint from the sets of "internal" symbols, and impose the 
> condition that internal function and predicate symbols may not be used 
> in external terms
> - we do not impose restrictions on symbols used in external frames
> 
> Let's see what the rest of the working group thinks about this.
> 
> Best, Jos
> 
> Michael Kifer wrote:
> > 
> > On Thu, 10 Jul 2008 17:03:25 +0200
> > Jos de Bruijn <debruijn@inf.unibz.it> wrote:
> > 
> >>
> >> Michael Kifer wrote:
> >>> This was not an omission, but I am fine with separating external from
> >>> non-external symbols for functions and predicates. 
> >> ok, good
> >>
> >>  > As to the frames, I do not think any of the symbols
> >>> should be required to be external.
> >> But then the same constant used in different contexts has a different 
> >> meaning, which I think was something we were trying to avoid in BLD.
> > 
> > Frames are reflexive by nature. So, in some other statement you may want to
> > say that some object (even external one) has a particular set of properties and
> > list them).
> > 
> > Frankly, I do not understand why is it a deal to allow the same, say predicate,
> > to appear inside External(...) and outside of it. The reason for separating the
> > symbols was to ease the interface with FOL. But separating external and
> > non-external symbols does not affect that.
> > 
> > Syntactically it is clear whether a symbol is used as external or internal, and
> > I see no reason to reinforce this with an additional syntactic kludge (I
> > conceded it just in the interests of peace :-).  If your argument is
> > error-checking then it is not our business. Systems that care about it would
> > build the appropriate error checkers.
> > 
> > 
> > 	--michael  
> > 
> >> Best, Jos
> >>
> >>>
> >>>
> >>> 	--michael  
> >>>
> >>>
> >>> On Thu, 10 Jul 2008 12:57:45 +0200
> >>> Jos de Bruijn <debruijn@inf.unibz.it> wrote:
> >>>
> >>>> There is an issue in BLD, which I unfortunately did not catch before.  I 
> >>>> think it is probably an omission in the definition, but it is a 
> >>>> substantive one.
> >>>> If we all agree that it is indeed an omission, we can probably address 
> >>>> the problem, create a new frozen version, and vote about publication in 
> >>>> the next phone conference on Tuesday.
> >>>> Personally, I am not ready to sign off on publication before this issue 
> >>>> is resolved.
> >>>>
> >>>> The issue is the following: in the definition of well-formed terms, the 
> >>>> set of all symbols is partitioned into predicate symbols, function 
> >>>> symbols, etc. however, no distinction is made between external and 
> >>>> "internal" symbols.  The consequence is that the same function or 
> >>>> predicate symbol can be used both in an external term and an internal 
> >>>> term, and these two terms have different meanings, i.e., the same 
> >>>> constant is interpreted differently based on the context, which is 
> >>>> something we explicitly wanted to avoid in BLD.  So, a built-in function 
> >>>> may be used outside an external term and will be uninterpreted.
> >>>>
> >>>> The problem is easy to fix by defining additional sets of external 
> >>>> predicate function symbols that are disjoint from the other sets of 
> >>>> symbols and defining appropriate restrictions on external terms (i.e., 
> >>>> the first function/predicate symbol in an external term must be an 
> >>>> external symbol).
> >>>> It becomes a bit more tricky when considering external frames, but 
> >>>> probably all constants used in an external frame should be external 
> >>>> individuals/functions/predicates.
> >>>>
> >>>> Best, Jos
>

Received on Thursday, 10 July 2008 15:47:43 UTC