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

[Christian Aistleitner]

Hello,

On Mon, 20 Aug 2007 13:04:03 +0200, Ralf Hemmecke <ralf at hemmecke.de> wrote:

>>>> It would be nice if there were any better means in Aldor to state
>>>> axioms for functions than just creating a category (like  
>>>> AbelianMonoid).
>>> Axioms seem rather redundant to me.  What's the problem with  
>>> introducing
>>> a category like:
>>>
>>>   define CommutativeTimes: Category == with { *: (%,%) -> % }
>
>> I am not saying that Mathematica is superior to Aldor, but Mathematica  
>> has
>> for example Attributes that can be applied to _functions_:
>> http://reference.wolfram.com/mathematica/tutorial/Attributes.html
>
>> Thereby, you can specify that you expect f( a, b ) to be equivalent to
>> f( b, a ) by attaching the "Orderless" Attribute to "f".
>> Mathematica in turn can exploit this knowledge to speed things up.
>
> But such an attribute is not very much different from Martin's
> CommutativeTimes above. One just has to attach it to "*".

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.

> But all this
> completely fails to do some formal proving about that all. Where would
> be the equation "a*b=b*a" that explains everything?

Within Mathematica.
Mathematica "knows" that the Attribute "Orderless" means a*b=b*a. Hence,  
Mathematica can use this knowledge to restructure the function call.  
"Orderless" is not just a name for Mathematica.

But let me repeat: I do not intend to say that Mathematica is superior  
here. It is just a brief and easy example, of some benefits coming from  
stating axioms differently.

Kind regards,
Christian