On Fri, Apr 5, 2013 at 3:51 AM, Martin Baker <[email protected]> wrote:
> Given that there is no resources (or desire, as far as I can see) to change > the structure of Axiom then I was wondering, just for specific domains where > we want a specific equation solver, could we encode the axioms in a set of > rules in a domain or package? I guess I'm looking for a compromise between > building this into the Lisp code and writing a seperate equation solver in > every domain. 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 _______________________________________________ Axiom-mail mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-mail
