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

>Jeremy wrote:
>>>  I think there are two proposals that I think we can be confident would
>>>  work: one in which all the ontology stuff is dark, and one in which no
>>>  sets necessarily exist.
>Then peter wrote:
>
>>The first definitely works.  There is not yet an existence proof that the
>>second does indeed work, at least as an extension of the RDF model
>theory.
>[...]
>>  If you mean a same-syntax
>>extension, then, again, that is impossible for the uppper layers without
>>  going to a very non-standard logic.
>-- http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0236.html
>
>So tonight I started writing up a model theory. I worked
>out the details for about 10 of the 30 or so terms
>in DAML+OIL; I'm pretty sure the rest are straightforward,
>but it's getting tedious and I'm getting tired, so
>I'm taking a break for the night...
>
>Jeremy, wanna look this over and maybe fill in the next few terms?
>
>
>
>==========
>
>As in [RDFMT], an interpretation I of a vocabulary V is
>
>1. A non-empty set IR of resources, called the domain or universe of I.
>
>2. A mapping IEXT from IR into the powerset of IR x (IR union LV)
>    i.e. the set of sets of pairs <x,y> with x in IR and y in IR or LV
>
>3. A mapping IS from V into IR
>
>
>Every owl interpretations is an RDF interpretations (i.e. IR
>contains IS(rdf:type)) and an RDFS interpretation (i.e.
>the RDFS closure rules apply).
>
>Recall that ICEXT(x) abbreviates {y | <y,x> is in IEXT(I(rdf:type)) }.
>
>
>Likewise, let ICEXT(x) abbreviates {y | <y,x> is in IEXT(I(rdf:type)) }.
>
>Additionally, owl reserves the following vocabulary:
>
>     * cardinality
>     * complementOf
>     * differentIndividualFrom
>     * disjointUnionOf
>     * disjointWith
>     * equivalentTo
>     * hasClass
>     * hasValue
>     * imports
>     * intersectionOf
>     * inverseOf
>     * maxCardinality
>     * minCardinality
>     * oneOf
>     * onProperty
>     * Ontology
>     * Restriction
>     * sameClassAs
>     * sameIndividualAs
>     * samePropertyAs
>     * subClassOf
>     * subPropertyOf
>     * toClass
>     * TransitiveProperty
>     * UnambigousProperty
>     * unionOf
>     * UniqueProperty
>     * versionInfo
>
>     * first
>     * rest
>     * nil
>     * item
>     * List
>
>
>That is, it reserves the URI references
>   http://www.w3.org/2001/10/daml+oil#cardinality ,
>   http://www.w3.org/2001/10/daml+oil#complementOf ,
>and so on; in this document, we'll abbreviate these
>as ont:cardinality, ont:complementOf and so on.
>
>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?

>
>The following constraints on interpretations apply:
>
>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, 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). 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.

Pat
-- 
---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Thursday, 30 May 2002 15:37:18 UTC