[Aldor-l] Re: Specifying properties of functions

[Ralf Hemmecke]

Hello Manuel,

> As for your suggestion on CommutativeRing, while it is mathematically
> purer, it might make it more difficult to test that category later on
> in code. For example, many types over a ring R have in their category
> 'if R has CommutativeRing then ... '  Such tests might become harder
> to write.

Of course, I would keep the category CommutativeRing exactly for that 
purpose you describe above and CommutativeRing is a category in the 
mathematical sense.

I made the code only as an example. Of course it is better to test
   if R has MyCommutativeRing ...
than
   if R has Commutative(R, *) ...

 > There have been projects to mix axiom and aldor with theorem
> provers so that one could indeed write axioms satisfied by the operations
> in the categories themselves (ie x*y=y*x for all x,y in CommutativeRing).
> They required compiler changes, and while they were mathematically elegant,
> it is unclear that there was a gain in expressiveness for the programmers.

I also don't see yet, how such axioms could help the _programmer_ much.
The point is that in Aldor the properties are given through the 
documentation (like for CommutativeRing) but not by a formal 
description. And yes, you guessed rightly that the final goal should be 
to put Aldor also into the frame of automated theorem proving. But maybe 
that is a very long term goal...

Can you give some references to these axiom/aldor/theorem prover projects.

Ralf