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

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

-- 
                          debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
One man that has a mind and knows it can
always beat ten men who haven't and don't.
   -- George Bernard Shaw