Re: 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.

You should not rely on the local constants ending up in the answer, but if
they do they should avoid giving the user a surprise.

> 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.

I think you are committing a subtle logical fallacy.

Note that I* is required to be a model of contents(iri) only, not of the
entire set of rules.

If p(l) is true in *some* I*, it does not mean that p(l) must be true in I.
For different I*'s, different l's will be in p. But for none of them p(l)
needs to be in I.


	--michael  


> Best, Jos
> -- 
> Jos de Bruijn            debruijn@inf.unibz.it
> +390471016224         http://www.debruijn.net/

Received on Friday, 11 April 2008 17:37:33 UTC