RDF lists

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 Thursday, 19 September 2002 18:39:42 UTC