W3C home > Mailing lists > Public > www-webont-wg@w3.org > May 2002

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

From: Dan Connolly <connolly@w3.org>
Date: 30 May 2002 15:16:19 -0500
To: patrick hayes <phayes@ai.uwf.edu>
Cc: connolly@jammer.dm93.org, www-webont-wg@w3.org
Message-Id: <1022789779.25651.210.camel@dirk>

On Thu, 2002-05-30 at 14:37, patrick hayes wrote:
> >The following closure rules apply:
> >
> >  ?l ont:first ?x.       ==> ?l ont:item ?x.
> >
> >  ?l ont:rest ?r.
> >  ?r ont:first ?x.	==> ?l ont:item ?x.
> ?Should that be
> ?l ont:rest ?r.
> ?r ont:item ?x.	==> ?l ont:item ?x
> in order to recurse?


You guys are reading closely!

> >cardinality:
> >if ?nl is a numeral for ?n (i.e. ?nl is a string that is a lexical
> >representation of the integer ?n), and <IS(?p), ?nl> is in
> >IEXT(I(ont:cardinality)) and <?s, ?o> is in IEXT(?p), then
> >the size of the set { ?x: <?s, ?x> is in IEXT(?p) } is ?n.
> Why not just say... that numerals denote numbers as a blanket 
> assumption,

umm... because sometimes they're movie titles?
I don't think I understand.

> and then state the condition in the interpretation? The 
> numbers part is kind of automagical, but at least you are being open 
> about that (and it can be handled by assuming that numerals have a 
> fixedpont semantics in any case.)
> The condition is then
> If <?p, ?n> in IEXT(I(ont:cardinality)) then
> |{?x: <?x,?s> in IEXT(?p)}| = ?n
> >
> >complementOf:
> >if <?s, ?o> is in IEXT(I(ont:complementOf)),
> >then ICEXT(?s) is the complement of ICEXT(?o)
> >relative to IR.
> >
> >differentIndividualFrom:
> >if <?s, ?o> is in IEXT(I(ont:differentIndividualFrom)),
> >then ?s is not equal to ?o.
> >
> >
> >disjointUnionOf:
> >1. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)),
> >and <?l, ?a> is in IEXT(I(ont:item)),
> >then ICEXT(?a) is a subset of ICEXT(?s).
> >
> >2. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)),
> >and <?l, ?a> is in IEXT(I(ont:first)),
> >and <?l, ?r> is in IEXT(I(ont:rest)),
> >and <?x, ?s> is in IEXT(I(rdf:type)),
> >then either ?x is in ICEXT(?a) or
> >there is a ?b where <?r, ?b> is in IEXT(I(ont:item)).
> >
> >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).

Huh? In the DAML+OIL model theory, the prose appeals
to all sorts of traditional set theoretic notions
when expressing constraints on interpretations...
it uses stuff like |{...}| to denote the
cardinality of sets and such.

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

No, ?l refers to something in IR, i.e. in the semantic domain,
not something in V, i.e. in the 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.)

I don't think I understand.

If there's an infinite list, or a cycle, it just won't
satisfy the definition I gave for pairwise-disjoint list.
I don't care if there are such things in the domain; they just
can't be objects of disjointUnionOf triples.

Constraints on interpretations are expressed using
semi-formal writing, no? If there's some rule
that says one can express contraints on interpretations thus:
  x in IC(?R) iff IR(?P)({x}) <= IC(?C)
but one cannot inductively/recursively define sets
in the domain, I'd like to know more about these rules.

By the way... 'the fixpoint condition for
the basic recursion theorems'... I'm not
familiar with that; how about a reference?

I don't see anything about it my favorite "crash course" source...

Ugh... this page nominated by google is completely greek
it points toward Kleene...

This isn't much help, except suggesting Cantor is
the author I should be looking for...

This seems to be the course I'm missing...

  15-453 Formal Languages, Automata, and Computation (FLAC)

> 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 hope I don't need to go there.

Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Thursday, 30 May 2002 16:16:42 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:56:43 UTC