- From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
- Date: Fri, 20 Sep 2002 09:38:52 +0200
- To: "pat hayes <phayes" <phayes@ai.uwf.edu>
- Cc: w3c-rdfcore-wg@w3.org
Pat, I think I'm fine with that
how can we express that
when given
_:l1 rdf:first :a .
_:l1 rdf:rest :b .
_:l2 rdf:first :a .
_:l2 rdf:rest :b .
then _:l1 and _:l2 are tidy
(we have that "for some" is actually
"for one" in this case and I've missed
a notation for that important fact)
-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
pat hayes
<phayes@ai.uwf.edu To: w3c-rdfcore-wg@w3.org
> cc:
Sent by: Subject: RDF lists
w3c-rdfcore-wg-req
uest@w3.org
2002-09-20 12:39
AM
Since RDF now has DAML_style lists (right?), I thought it would be
good to get feedback on the proposed MT for them. So here it is: toss
back any comments, please.
-----------
Given a set S, we define a set of lists over S to be a set L
containing the empty sequence <> and all structures of the form <s,
l> where s is in S and l is in L.
As with any recursive 'definition', this in fact is an equation with
many possible solutions. The usual way to interpret this kind of
definition is in terms of a minimal solution of the equation. That
means that one would understand the set of lists to be the smallest
collection of things that would satisfy the recursion, which would be
all finitely deep lists which have no loops, i.e. structures of the
form <s1 <s2 <...<sn <>>...>>. On this view, every list defines a
finite sequence of elements of S. Other lists are possible, however,
which would also satisfy the recursive definition: infinitely deep
lists, for example, or looping lists of the form l = <s, l>.
Although it is possible to axiomatize a recursive 'definition' as a
logical assertion, there is no way to finitely axiomatize the least
fixed-point solution. We could impose it as a semantic condition; but
this condition, although intuitively sensible and in correspondence
to the usual semantics for computational languages, may have some
regrettable consequences when used, as here, in the context of a
descriptive language. In particular, there would be no way to
establish the completeness of any finitary inference process relative
to such a semantics. We therefore avoid making this stipulation, and
simply require that the set of lists in any interpretation be *some*
set which satisfies the recursive definition. Note that this means
that any set of lists will at least contain all the finite
non-looping lists.
The semantics of the rdf list vocabulary is then straightforward. In
any RDF interpretation I, we assume that
ICEXT(I(rdf:List)) is a set of lists over IR @@Note the use of 'a'
rather than 'the'.@@
I(rdf:nil) = <>
<x, y> in IEXT(I(rdf:first)) iff x = <y, l> for some l in
ICEXT(I(rdf:List))
<x, y> in IEXT(I(rdf:rest)) iff x = <s, y> for some s in IR
We note in passing that this semantics requires that the universe IR
is closed under the operation of constructing lists.
Any interpretation I of any RDF graph of the form
A1 rdf:type rdf:List .
A1 rdf:first B1 .
A1 rdf:rest A2 .
A2 rdf:first B2 .
A2 rdf:rest A3 .
...
An rdf:first Bn .
An rdf:rest rdf:nil .
has I(A1) = <I(B1), <I(B2), <... <I(Bn), <> >...>>. We will describe
this as a sequence and write it as [I(B1), ... , I(Bn)]. Sequences
are the ordered multisets of the elements of finite lists.
--------
--
---------------------------------------------------------------------
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 Friday, 20 September 2002 03:42:17 UTC