RE: layering (5.3,5.10): a same-syntax model theory

> >
> >3. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)),
> >then ?l is a pairwise-disjoint list, defined
> >recursively
>
> Whoa. If this  really is a same-syntax extension then in order for
> this to be meaningful you need to show how recursion can be expressed
> in RDF (good luck). If you want to be able to say: look, I *know* the
> lists are finite since they are part of the graph, so obviously I can
> tail-recurse along them; then fine: but now you have built the lists
> into your syntax, so you aren't describing a same-syntax extension.
> Which is fine with me, let me say at once; but let's keep our
> terminology clear. You can use recursion on syntax, but you can't use
> it on things in the semantic domain unless you first show that the
> domain satisfies the fixpoint condition for the basic recursion
> theorems. (Same point, differently expressed: how do you know that
> the lists in the semantic domain, denoted by your list expressions,
> are finite? Finiteness isn't expressible in any RE language.)
>
> You could give RDF a different semantics (eg use minimal models) like
> the logic programmers do for Horn logic, but then it probably
> wouldn't mean what you want it to mean for other purposes.


I think this gives further ammunition to treating the daml:collection
thingys specially as I suggested earlier in this thread.

From previous with a small change:

Jeremy:
> An OWL interpretation built on an RDF interpretation has
> - a function I that maps nodes to things in the domain of discourse,
> - a fucntion IEXT that maps some things in the domain of discourse to
> properties
> - a function LEXT that maps some things in the domain of discourse to
> sets.
>   LEXT(I(ont:nil)) = {}
>
> if ?l is in ICEXT(ont:List) if and only if ?l is in the
> domain of LEXT.
>
> if ?l is in ICEXT(ont:List) and ?l != I(ont:nil) then
>   there must be some ?x and some ?r such that
>     < ?l, ?x > is in IEXT(I(ont:first))
>   and
>     < ?l, ?r > is in IEXT(I(ont:rest))
CHANGE
    and
      ?x is not a member of LEXT(?r)

>
> and moveover for all such ?x and ?r,
>   ?r is in the domain of LEXT and
>   LEXT(?l) = { ?x } union LEXT(?r)


The CHANGE means that when we create a list of thingies with the
daml:collection syntax (or its replacement) we are commiting to the
thingies being distinct intensions within the domain of discourse. The
class extent of any pair of these intensions may or may not differ.
i.e. if we have aaa and bbb as to uris in the same collection then:
  I(aaa) != I(bbb)
but
  ICEXT(I(aaa)) and ICEXT(I(bbb)) may be the same

Then, to return to the disjoint union.
We can say that:

3. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)),
then LEXT(?l) is a (finite?) set and
  for all ?a ?b in LEXT(?l) then
     ICEXT(?a) intersect ICEXT(?b) != empty
   implies
     ?a = ?b
and
   <?s, ?l > is in IEXT(I(ont:unionOf))

Personally I would not include the word 'finite'.
The only sets we are actually interested in (those constructed from the
daml:collection syntax), will be finite so it does not harm to have it.

This captures the disjoint union semantic precisely with no recourse to
any recursion.

Jeremy

Received on Friday, 31 May 2002 06:59:07 UTC