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 ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
