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

This was not an omission, but I am fine with separating external from
non-external symbols for functions and predicates. As to the frames, I do not think any of the symbols
should be required to be external.



	--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 14:37:52 UTC