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

[Christian Aistleitner]

Hello Martin,

I just realized I never replied to this mail. I am sorry.

On Mon, 20 Aug 2007 14:32:14 +0200, Martin Rubey  
<martin.rubey at univie.ac.at> 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.

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

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

But these are just some advantages...

Kind regards,
Christian