# semantics of local constants - followup

From: Michael Kifer <kifer@cs.sunysb.edu>
Date: Sat, 12 Apr 2008 04:36:59 -0400
To: debruijn@inf.unibz.it (Jos de Bruijn)
cc: public-rif-wg@w3.org (RIF WG)
Message-ID: <29509.1207989419@cs.sunysb.edu>
```

Earlier I wrote:
>
> Jos wrote:
>
> > 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.

Sorry, the logical fallacy was mine. I tried to simplify things, confused
myself, and came up with a broken definition.

But a proper definition is not that difficult -- just have to stick to the
basic outline of the Roman framework. Define multidocument semantic structures
as follows.

Suppose you have documents d1, ..., dn. A semantic structure, I, for
d1,...,dn is a tuple of semantic structures (I1,...,In) such that

I1 |= contents(d1)
...
In |= contents(dn)

Then you start gluing those semantic structures. For general modules it is
slightly more involved, but for imports it is simple:

For every statement

Import(di)

which appears in dj, the following must hold:

Ii must coincide with Ij except that Ii_C, Ii_F, and Ii_CF can
differ from Ij_C, Ij_F, and Ij_CF on the local symbols.

--michael
```
Received on Saturday, 12 April 2008 18:05:46 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 2 June 2009 18:33:48 GMT