Re: A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra

Martin Baker <[email protected]> Fri, 05 Apr 2013 09:51:46 +0100
Newsgroups gmane.comp.mathematics.axiom.user
Organization axiom
Message-ID <[email protected]>
On 05/04/13 01:07, Ralf Hemmecke wrote:
> I don't quite understand. If you assume myOp1 to be commutative, then
> solving equations is quite a different task from when it is
> non-commutative. Where would you store all these axioms?

Yes that's an interesting question. For an Axiom category to correspond 
to a 'category' in category theory or a 'theory' in universal algebra 
then it should define both the function signatures and the axioms. I get 
the impression that Axiom(the program) attempts to include axioms in 
categories to a limited extent by say: inheriting commutative but this 
would not be complete enough to drive a general equation solver? (and, 
of course, it cannot enforce commutative axiom in domain instances). It 
seems a sight irony that Axiom(the program) does not do much about axioms.

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.

> Looks like you aim at a general term rewriting system.

Yes, but again I recognise that there are no resources, so I was 
wondering if it would be possible to start with a very simple domain 
(not a field, something really simple, which is what I was trying to 
indicate in the psudocode in my last message). Then abstract out a rule 
engine. Then gradually build it up over time so that it could cope with 
more complex domains.

This is probably not very practical, but I was just trying to do a 
thought experiment to investigate what would be required to have 
variables that range over domains that are not numbers.

Martin