Re: [Axiom-mail] A question about Axiom capabilities

[Martin Baker]

On 05/04/13 12:11, Gabriel Dos Reis wrote:
> Your probably know that OpenAxiom started putting the axioms in AXIOM.
> See for example:
>
> 
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
>
> In fact, a couple of years ago, a student of mine did experiments on
> exploiting these axioms to help code generation and automatic
> parallelization.  The results were very encouraging (see the
> yli-sandbox for example.)
>
> OpenAxiom is very much committed to get the axioms integrated to the
> entire type checking and elaboration process.

Gaby,

Thanks, I find this stuff interesting, Its not that I expect it to 
appear in any flavour of Axiom soon (feel free to correct my 
assumptions), its just that I like to know how things work, what can and 
what can't be done.

AFSICS axioms are currently embedded in the inline documentation for the 
category like this:

snippet from:
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
++ Axioms:
++   \spad{associative("+":(%,%)->%)}\tab{30}\spad{ (x+y)+z = x+(y+z) }
++   \spad{commutative("+":(%,%)->%)}\tab{30}\spad{ x+y = y+x }
AbelianSemiGroup(): Category == SetCategory with

I had a rummage about in the sandbox you mentioned (written by Yueli 
about 3 years ago) and I did not come across any overall tutorial file 
(what I would think of as top level documentation) I may have missed it. 
Did Yueli write any thesis or anything like that?

At first glance it does look encouraging as the code to analyse the code 
does seems to be written in SPAD, which hopefully shows that it can be 
done. When I look at the code (such as snippet below) it looks like the 
axioms are coded differently, that is on a per operator basis?

snippet from:
http://sourceforge.net/apps/trac/open-axiom/browser/yli-sandbox/contrib/redec/operatorcats.spad?rev=2776
)abbrev category ASSOCOP AssociativeOperator
  ++ Axiom: associativity: rule op(a, op(b, c)) == op(op(a,b), c)
  AssociativeOperator(T: SetCategory, op: Mapping(T, T, T)):Category
    == MagmaOperator(T, op)

Any further clues for understanding the code appreciated, thanks,

Martin