W3C home > Mailing lists > Public > www-rdf-logic@w3.org > January 2001

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

From: Dan Connolly <connolly@w3.org>
Date: Fri, 12 Jan 2001 12:46:14 -0600
Message-ID: <3A5F50F6.9633A5C2@w3.org>
To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
CC: horrocks@cs.man.ac.uk, www-rdf-logic@w3.org
"Peter F. Patel-Schneider" wrote:
> 
> There appears to be a type problem in the definition of DAML+OIL lists.
> 
> The problem is that there is no way of typing a list.  For example,
> Disjoint could be a list of anything---not necessarily a list of classes,
> as we want/require.

No way of typing a list? If you mean that there's no handy
idiom for it, OK. But there certainly is a way to say
what we mean; we've said it:

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

>  Note that this problem is not confined to DAML+OIL as
> RDF(S) itself has no (decent) mechanism for constraining the type of
> collection elements.

It's accurate to say that RDF(S) didn't standardize any idiom for
it; but I don't see it as a problem. If it's a useful idiom
for our community, we can certainly add, say, a listOver
property to relate a subclass of List with a class for the
elements of the list.

	(=> (PropertyValue listOver ?LC ?C)
		(forall (?e ?l)
			(=> (and (Type ?l ?LC)
			(PropertyValue item ?e ?


> DAML+OIL has a bigger problem, however, in Disjoint.  Disjoint is a
> subclass of List.  Does this mean that the rest of a Disjoint should also
> be a Disjoint?

That's a theorem, provable from Ax56: the empty list is
a Disjoint vacuously, and the induction step follows pretty easily.

>  This seems to make sense, but it can't be as lists have to
> be terminated by a nil, which is not a Disjoint, just a List.

Yes, nil is a Disjoint as well as a List; what made you think otherwise?

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Friday, 12 January 2001 13:46:24 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:38 GMT