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

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.

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