Re: function terms in Euler, n3, and RDF [was: gedcom-relation e

From: Sandro Hawke <sandro@w3.org>
Sent: Tuesday, March 06, 2001 3:50 PM
> > > [Dan Connolly writing:]
> > >
> > > In playing around with n3, we came up with a couple idioms for this.
> > >
> > > One is to encode "a sum of 4 and 3" as [a :Sum; :of 4; :and 3],
combined
> > > with knowledge that there is exactly one such sum.
>
> But why would there ever be "exactly one such sum" ?

er... that's the nature of the beast; the sum of any two integers exists
and is unique, kinda like the mother of any human being exists
and is unique, but without the complications of adoption,
fertilization techniques, and other real-world-messiness.

i.e. it's an axiomatic property of integers that

{ [ :of :x; :and :y]. # the sum exists, and...
 { :s1 :of :x; :and :y.
   :s2 :of :x; :and :y. } l:implies { :s1 = :s2 }. # it's unique.
} l:forAll :x, :y, :s1, :s2.

it's usually formalized as a theorem relative to axioms like

{ :x :of :x; :and :_0. # base case: 0 is the additive identity element
  [is :succ [:of :x; :and :y]] :of :x; :and [is :succ of :y] # induction
step.
} l:forAll :x, :y.

which looks awful/silly compared to the more conventional idiom
using lists:

daml:nil :sum int:_0.
{{ :xi :sum :t } l:implies { [daml:first :_0; daml:rest :xi] :sum :t}}
l:forAll :xi, :t.
{{ [daml:first :x; daml:rest :xi] :sum :t } l:implies
     { [daml:first [is :succ of :x]; daml:rest :xi] :sum [is :succ of :t]}}
l:forAll :x, :xi, :t.

(ok, so that's kinda awful too. And I don't have ready access to an n3
parser
to syntax-check it. Oh well...)

> > >                                                    If you make the
domain
> > > of :of and :and be :Sum (aka :Integer) and recall that = denotes
> > > daml:equivalentTo,
> > > you can write "the sum of 4 and 3 is 7" as
> > >   [ :of 4; :and 3 ] = 7.
>
> And without that qualification, this doesn't work.

I think TimBL answered that part, but then so did you...

> > > The other idiom is somewhat more traditional, making use of the list
> > > syntax-sugar in n3, where (a b) denotes the same thing
> > > as [ daml:first a; daml:rest [ daml:first b; daml:rest daml:nil ]].
> > > Using that, we can write "the pair 3,4 has sum 7: as
> > >   (3 4) :sum 7.
>
> That works.  Expanded out, that's
>    :anon1 arith:sum 7;
>           daml:first 3;
>   daml:rest :anon2.
>    :anon2 daml:first 4;
>           daml:rest daml:nil.
>
> In general, I think it's better practice to name the elements of a
> tuple (making it what?  an "object"?  a "record"?  an "associative
> array"?  a relation in its own right?).

Sometimes. But sum generalizes so nicely to the n-ary case that
the list idiom is awfully appealing.

>  People are used to anonymous
> (positional) parts for the addition relation, but I'll name them
> anyway:
>
>    :anon1 a arith:BinarySum
>          arith:left 3
> arith:right 4
> arith:result :_7

arith:left is exactly the same as :of , and
arith:right is exactly the same as :and.

Perhaps :of and :and were too obscure/clever names. Evidently so.


> > > Dan Connolly, W3C http://www.w3.org/People/Connolly/
>
> Sandro Hawke, W3C http://www.w3.org/People/Sandro/

Received on Wednesday, 7 March 2001 01:14:36 UTC