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

[Martin Baker]

On 05/04/13 10:20, Ralf Hemmecke wrote:
> On 04/05/2013 10:51 AM, Martin Baker wrote:
> > It seems a sight irony that Axiom(the program) does not do much about
> > axioms.
>
> Of course, AXIOM can deal with axioms, but the SPAD language does not
> include any way to specify axiom (not even Aldor can do this).

I was thinking of something like CASL:
http://www.informatik.uni-bremen.de/cofi/wiki/index.php/CASL
I realise that its purpose is different to a category in Axiom but it 
does at least show how the semantics as well as the syntax of a category 
could be encoded in a well defined language.

Even if it were not possible to use this 'semantic' information for 
enforcing axioms or equation solvers it would be good to have it for 
documentation and automatically generating test scripts.

> > > 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
>
> For a term rewriting system you basically have to start with the
> implementation of a term algebra. The signature would basically tell,
> what symbols are allowed. Since LISP is so fitting for a representation
> of such a term algebra, it is no surprise that quite a lot of computer
> algebra systems were written in LISP.
>
> Then you can add equations (axioms) and a mechanism to reduce a given
> term modulo such equations. But there is no general algorithm to
> transform a given term modulo such equation into a canonical form. A
> "canonical form" does not even exist for every given term rewriting
> system. The non-existence of the "eierlegende Wollmilchsau"
> (http://de.wikipedia.org/wiki/Eierlegende_Wollmilchsau
> http://en.wiktionary.org/wiki/eierlegende_Wollmilchsau) is the reason
> why people work on specialized solvers and use special representations
> of the respective term algebra to make things fast.

So are you saying that, for practical purposes, it is not even worth 
trying to write an equation solver for a given category/domain in SPAD, 
even for a very simple category?

I realise there is no general algorithm to do this, but I was hoping 
there might have been the possibility of a common 'toolkit' so at least 
every category/domain writer was not totally on their own.

Martin