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

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?

Yes.

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...
  http://www.earlham.edu/~peters/courses/logsys/lshome.htm

Ugh... this page nominated by google is completely greek
  http://nl.ijs.si/~damjan/kleene.html
it points toward Kleene...

This isn't much help, except suggesting Cantor is
the author I should be looking for...
http://wombat.doc.ic.ac.uk/foldoc/foldoc.cgi?General+Recursion+Theorem

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

  15-453 Formal Languages, Automata, and Computation (FLAC)
  http://www-2.cs.cmu.edu/~lblum/courses/flac/schedule.html


> 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