[Aldor-l] Axioms in Aldor [was: Re: "has" and "with" and bug]

[Bill Page]

On 9/5/07, Christian Aistleitner wrote:
>
> On Mon, 20 Aug 2007 14:32:14 +0200, Martin Rubey wrote:
>
> > "Christian Aistleitner" <tmgisi at gmx.at> writes:
> >
> >> attaching the semantics to the function instead of the domain is a
> >> crucial difference!  At least for me, commutativity is a property of
> >> the function and not of the domain.
> >
> > I very much like this summary, therefore I quote it :-)
> >
> > Now, any idea how this should be done in (an extension of) Aldor?
>
> No, not really.
>

The way this is done in Axiom now is to provide a property with a
parameter. So a property like (actually used in Axiom):

  commutative("*")

should be interpreted (by the programmer) as claiming that for the
operator *, the following holds

  a * b = b * a

for all a and b.

In Aldor I think that this might be done by a category constructor like:

  define commutative(A,B,f:A->B): category with {
    --assert a*b = b*a
  }

and used something like this

  testdomain(): somecategory with {
    *:(%,%)-> %;
    ...
    if % has commutative(%,%,*) then ...

> >  What would or could it buy us?
>
> Lots and lots of things. Assume in some Aldor Code, you have
> (for whatever reason)
>
>    gcd( gcd( some large positive integer, some other large posivite integer), 1 )
>
> If Aldor would know, that in this domain "gcd( some large positive
> integer, 1 )" always yields 1, Aldor might infer that the above gcd
> computation will yield 1, no matter what values "some large positive
> integer" or "some other large posivite integer" represent. It might
> optimize the time taking gcd computation away!
>
> Assume the following function:
>
>    f( a: Integer ):() == {
>      b:Integer := a*a;
>      if b >= 0 then
>      {
>        ...
>      } else {
>        ...
>      }
>    }
>
> If Aldor would "know" how *$Integer behaves, it might warn you that the
> else branch of f cannot be reached.
>

I think that having the *compiler* know about such things is quite
different (and must more ambitious) than just allowing the programmer
to write code that can make and test such assertions.

> And last but not least, Aldor might help you doing correctness proofs of
> your programs.
>

This was yet another subject that was discussed at the recent Aldor
workshop. Stephen Watt made several suggestions about possible changes
to the Aldor language to support "axioms" and/or assertions at the
level of the Aldor compiler. I hope that some of the draft slides that
were electronically sketched during the workshop can be made available
online to refresh my memory and remind the authors of the ideas that
they had at the time of the workshop. In any case, I think there is a
lot of support for this idea in the Aldor community.

Regards,
Bill Page.