semantics of local constants [was: Re: imports + metadata]

Michael,

First about the intuition behind local identifiers:

 > In addition, I am not sure that your definition is necessarily the 
"right one."


Well, this depends on what local identifiers should be, and how local 
"local" is.

My intuition is that local identifiers are local to a specific rule set, 
so if you query the rule set you cannot rely on what these local 
identifiers look like and the identifiers ending up in your query answer 
might be different from those appearing in your rule set.


Then about the definition itself:

I think it is nice to have a semantic definition for imports, but I have 
some reservations about your definition:

>     I |= Directive(Import(iri))
> 
> iff for every I*
> 
>     I* |= contents(iri)
> 
> where I* is a semantic structure, which is the same as I except that I*_C, I*_F,
> I*_CF may differ from I_C, I_F, I_CF on the symbols ^^rif:local.

This looks a bit like universal quantification, which is not something 
we want to have, I think.

Consider a rule set R with one atom and one import statement:
p^^iri(a^^local)
Directive(Import(i))

and the rule set identified by i:
p^^iri(a^^local)

Consider a structure I such that p^^iri(a^^local) is true, so there is 
an element k in the set denoted by p.
Consider now any structure I* that is like I such that I*_C(a^^local)=l; 
if I* is a model of i, then l is necessarily in the set denoted by p. 
Since i must be satisfied by every such I*, it is necessarily the case 
that if I is a model of R, the set denoted by p includes all elements in 
D_ind, so
Forall ?x (p^^iri(?x)) must be satisfied.


Best, Jos
-- 
Jos de Bruijn            debruijn@inf.unibz.it
+390471016224         http://www.debruijn.net/
----------------------------------------------
Doubt is not a pleasant condition, but
certainty is absurd.
   - Voltaire