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

Anotations below.

I think the axiomatic semantics has what is needed for list,
first, and rest .  I have grabbed the sections in the document and included
them in this note.

Please let me know if you think there are remaining issues.

thx,
Deborah

Dan Connolly wrote:

deleting portions...

> Ian Horrocks wrote:
> >
> > On January 12, Dickinson, Ian J writes:
> >

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

in:  http://www.daml.org/2000/12/axiomatic-semantics.html

there is:
5.1.9.      List

%% “Seq” is a value of “subClassOf” for “List”.  (I.e., lists are sequences.)
Ax65.    (PropertyValue subClassOf List Seq)


and
5.2.22.  first


%% “first” is type “FunctionalProperty”.
Ax128.(Type first FunctionalProperty)

%% Saying that an object X is the value of “first” for an object L is
logically
equivalent to saying that L is type “List” and the value of “_1” for L is X.
(I.e.,
“first” is “_1” for lists.)
Ax129.(<=> (PropertyValue first ?l ?x)
                 (and (Type ?l List) (PropertyValue _1 ?l ?x)))

5.2.23.  rest


%% “rest” is type “FunctionalProperty”.
Ax130.(Type rest FunctionalProperty)

%% Saying that an object R is the value of “rest” for an object L is logically

equivalent to saying that L is type “List”, R is type “List”, and L has the
same
items in the same order as list R with one additional object as its first
item.
Ax131.(<=> (PropertyValue rest ?l ?r)
                 (and (Type ?l List)
                      (Type ?r List)
                      (exists (?x) (= ?l (cons ?x ?r)))))[11]

%% Note that the following can be inferred from the axioms regarding “oneOf”,
“domain”, and “range”:
Th25.    (PropertyValue domain rest List))
Th26.    (PropertyValue range rest List)


Did someone think they needed more than this?

--
 Deborah L. McGuinness
 Knowledge Systems Laboratory
 Gates Computer Science Building, 2A Room 241
 Stanford University, Stanford, CA 94305-9020
 email: dlm@ksl.stanford.edu
 URL: http://ksl.stanford.edu/people/dlm/index.html
 (voice) 650 723 9770    (stanford fax) 650 725 5850   (computer fax)  801 705
0941