Re: [Axiom-developer] Axiom in general

[Nicolas Doye]

On Mon, 2005-09-12 at 23:59 -0400, root wrote:
`
> Unfortunately Axiom does not contain a thorough description of the 
> mathematical principles. It does not even contain a good explanation
> of category theory or even of the algorithms that it uses. By design
> this will change in the future provided people lend their expertise
> to the problem. It's clearly a 30 year horizon goal.

I'm a bit rusty on all this, and my knowledge out of date. So caveat
blah-de-blah. For those that don't know remember my mini-intro some time
back, I was one of James Davenport's PhD students charged with finding a
mathematical foundation for coercion in Axiom.

http://worldofnic.org/research/phd.ps

Chapter 2 of my thesis gave some introduction to the mathematical
formulation of Categories in Axiom/Magma/OBJ.

Chapter 3 talks about Category Theory.
Chapter 4 talks about Order Sorted Algebra.
(Both these chapters put these definitions in Axiom terms at the end).

Chapter 9 talks about where I'd like Axiom to go.

Some of my "ideas" in my thesis are wrong and I no longer stand by them.
I was naive. Please ignore 9.7 and any assertions that Axiom should be
written in Axiom. ;-)

In some ways, it is far more useful to not think of Axiom in terms of
Category Theory. Functors etc. are useful sometimes when thinking
abstractly about Axiom, but Axiom's true roots are in Order Sorted
Algebra.

In axiom a Category is an Order Sorted Signature, but the order on the
sorts is never explicitly defined and there are some difficulties in the
definition of the operator symbols.

OBJ _is_ based on Order Sorted Algebra. It's main advantage over Axiom
as I see it, is that it defines Theories. A Theory is an Order Sorted
Signature with (and this is what Axiom misses) a set of equations. This
means that in Axiom we are free to say that MyDomain is in MyCategory,
but certain assertions that we as mathematicians know about all Domains
in MyCategory may not be true in MyDomain. Will literate programming
help? Maybe. Will it enforce? Nope.

Another fantastic advantage of OBJ is a view. In Axiom we can not say
that MyDomain forms a Group over the operator * and the operator +,
because the operator is hard-coded into the Group Category. This
sucks. :-( Changing this behaviour is left as an exercise to the reader
with time to rewrite almost all of Axiom. :-)

nic