Warning: There is some unfortunate notational overloading here. I'll try to use a capitalised 'Axiom' for the program (any flavour) and lower case 'axiom' for the mathematical concept. I'll try to make the word 'category' clear by the context.

## Motivation

There are various ways to divide up mathematics. The Axiom program (here I mean pan-Axiom) generally aligns with these, but there is a slight mismatch. An Axiom category has little definition of its axioms. Of course a domain must respect its axioms but they are not yet explicitly and automatically policed or available to SPAD or external code. |

I guess we can roughly characterise what is required in a category as

- the function signatures (syntax)
- the axioms (semantics)

It seems to me that It would be very useful to have axioms defined within categories, for many reasons, including such things as:

- Automatically checking of the axioms in domains (if not in real time then at least in test suite).
- As an input to writing compiler-like code in SPAD.
- Support for general equation solver in non-numeric variables.
- Input to a general term rewriting system.
- As a basis for modeling Axiom structures in formal specification tools.
- As an input to theorem provers (either written in SPAD or formal tools)

Gabriel Dos Reis and Yue Li have done a lot of work on specifying axioms in a category and it is starting to appear in OpenAxiom. Three years ago Yue Li used an early version of this for:

- Code generation
- Automatic parallelization

His code is here and there is some information here.

I would like to help and encourage, in my own small way, putting axiom information in OpenAxiom categories and it seems to me that there is a need to fill the documentation/tutorial holes. I would also like to make information about this available to the Axiom and FriCAS projects in the hope that they might join in.

## 'assume' Syntax

OpenAxiom and the sandbox code written by Yue Li has gone through some changes and it is not yet completely in its final final form. So its probably best if I try and write down where it is headed but, just to explain existing code, these are roughly the stages:

Stage 1 - axioms in inline comments in existing categories. | snippet from here ++ 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 |

Stage 2 - Operator categories added so that axioms can be defined on a per operator basis | snippet from here )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) |

Stage 3 - 'assume' syntax (still on a per operator basis) . | Snippets from here SemiGroupOperatorCategory(T: BasicType): Category == BinaryOperatorCategory T with assume associativity == forall(f: %, x: T, y:T, z: T) . f(f(x,y),z) = f(x,f(y,z)) and MonoidOperatorCategory(T: BasicType): Category == SemiGroupOperatorCategory T with neutralValue: % -> T ++ \spad{neutralValue f} returns the neutral value of the ++ monoid operation \spad{f}. assume neutrality == forall(f: %, x: T) . f(x, neutralValue f) = x f(neutralValue f, x) = x |

So extra syntax has been added in to encode the axioms, it would help to have a more precise definition of this extra syntax, here is my first try to reverse engineer the openAxiom syntax (in a semi-formal syntax - not quite the full EBNF to try to make it more readable):

where:

- single quotes means keyword
- '{' means indent (push pile)
- '}' means previous indent (pull pile)
- type is either '%' or type parameter from category parameters.

## Using axioms from within SPAD

SPAD does already have a mechanism for specifying rewrite rules (described on the page here. Could this be extended to allow, for instance, identities to be specified as part of each category and domain and to be inherited in the same way that the function signatures are.

It would be useful for:

- A domain to be able to introspect its own axioms.
- Compiler-like SPAD code to be able to read axioms from other categories.

## Category Structure

I think there is a need for a way that humans can absorb the complex interrelationship of these structures. Axiom already has diagrams like this It would be good (and I hope useful) to try to extend this to incorporate the axiom information.

In order to explore the possibilities I am starting by using a simple graphical editor (Inkscape) which makes it easier to try out various layouts. The downside, compared to automated methods, is that it it time consuming to maintain and errors can, probably already have, get in.

The first problem is to find the right level of detail. For me, just including the category and domain names does not give enough information to human users about what domains they should use. However too much information makes the diagram cluttered and unusable. I think it will take some experimenting to get the balance right.

Here is a very small sub-diagram (based on catdef.spad.pamphlet) to experiment with layouts and level-of-detail issues: