Re: Bugs in 2000/12 daml+oil reference on DAML collections

Ian Horrocks wrote:
> 
> On January 12, Dickinson, Ian J writes:
> 
> I'll skip the stuff about typos in the reference document
> 
> [snip]
> 
> Good point about Disjoint.
> 
> The reason for the different use of List in Disjoint and oneOf is that
> Disjoint is an axiom that makes an assertion about the elements of the
> list, but which does not define a new class. Note that this affects
> the semantic interpretation of each of the elements, but daml+oil does
> not assign any semantics to the Disjoint class itself.

I'm not sure what you mean by that; we the relevant axiom
is just as much about the Disjoint class as about the
classes inside a Disjoint:

Ax56.    (<=> (Type ?l Disjoint)
           (and (Type ?l List)
                (forall (?c) (=> (PropertyValue Item ?c ?l)
                                 (Type ?c Class)))
                (forall (?c1 ?c2) 
                        (=> (and (PropertyValue item ?c1 ?l)
                                 (PropertyValue item ?c2 ?l) 
                                 (not (= ?c1 ?c2))) 
                            (PropertyValue disjointWith ?c1 ?c2)))))
	-- http://www.daml.org/2000/12/axiomatic-semantics.html

>
> oneOf is not, by itself, an axiom: it is a class constructor.

What's a class constructor? oneOf is just a property; it
relates a class, say C, and a list, say L; it says
that something is in C (i.e. related to C by rdf:type) exactly
when it's in L (i.e. related to L by daml:item).

The relevant axiom is:

Ax84.    (<=> (PropertyValue oneOf ?c ?l) 
           (and (Type ?c Class)
                (Type ?l List)
                (forall (?x) (<=> (Type ?x ?c) 
                                  (PropertyValue item ?l ?x)))))

>  It
> builds a new class from the elements of the List and, only when it is
> used as a property of a class C do we have an axiom asserting that the
> interpretation of C is the same as the interpretation of the class
> built by oneOf.
> 
> However, this doesn't solve the problem with the daml:collection parse
> type. If daml:collection turns the enclosed elements into a List
> structure, then it doesn't make sense to use it inside another list
> without an intervening property. I don't like using equivalentTo (as
> suggested by Dan)

I don't find it syntactically appealing, but it works; equivalentTo
can always be used as a syntactic shim to relate two terms
that denote the same thing, no?

> as the List itself doesn't have any semantics,

Huh? List/first/rest have the usual semantics; e.g.
	(forall (?l1 ?l2 ?f ?r)
		(=> (and (daml:List ?l1) (daml:List ?l2)
			(daml:first ?l1 ?f) (daml:rest ?l1 ?r)
			(daml:first ?l2 ?f) (daml:rest ?l2 ?r))
			(daml:equivalentTo ?l1 ?l2) )

isn't that in the axiomatic semantics? (I've left out the Type and
PropertyValue
thingies; and daml:equivalentTo is interchangeable whith KIF's =
yes, that's explicit: Ax68)

http://www.daml.org/2000/12/axiomatic-semantics.html

Ugh.. I don't see any axioms about first/rest there;
Let's please add it.


> so its hard to see how it can be equivalent to anything.

Why? Even without list semantics, I can take any two
terms and say they're daml:equivalentTo each other, no?

> I would
> suggest that a better way to do it would be:
> 
>  <daml:Disjoint>
>    <daml:first rdf:resource="#Car"/>
>    <daml:rest rdf:parseType="daml:collection">
>      <rdfs:Class rdf:about="#Person"/>
>      <rdfs:Class rdf:about="#Plant"/>
>    </daml:rest>
>  </daml:Disjoint>

That works too.

> 
> Regards, Ian
> 
> > The second problem is that it would be nice if we could apply a simple
> > syntactic transformation [...]

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Friday, 12 January 2001 13:17:19 UTC