- From: Dan Connolly <connolly@w3.org>
- Date: Fri, 12 Jan 2001 12:46:14 -0600
- 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 UTC