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

On January 12, Dan Connolly writes:
> 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)))))

Of course its a property, but its semantics mean that it effectively
"constructs" a class (whose instances are exactly the list items) and
asserts that it is equivalent to another class (the ?c class in
Ax84). In contrast, Disjoint makes some assertions about the
relationships between the classes in the list, but it doesn't
"construct" anything. Ax56 tells us what Disjoint means for the list
items, but it doesn't say anything about the interpretation of the
Disjoint class itself. If we used this class inside another
"constructor", like intersectionOf, we would have no way to determine
the semantics of the resulting class.

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

This doesn't really tell us what a list means, just when 2 lists are
equivalent. A list only has a meaning when we apply an "operator" to
it, such as oneOf or Disjoint.

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

Sure - I was thinking of sameClasAs. Equivalent to has the great
convenience of not actually meaning anything so we can use it wherever
we like :-)

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

Ian

Received on Friday, 12 January 2001 15:40:13 UTC