RE: [Axiom-developer] Time for another crazy idea...

[Bill Page]

On February 20, 2006 6:39 PM C Y wrote:
> ... 
> My understanding of Axiom's concept of categories and domains is
> that it is similar to and at least somewhat compatible with category
> and/or set theory, but it was not explicitly designed to implement
> and rely these theories as a foundation.

I think a more accurate characterization might be that Axiom was
developed by people who were very much aware of the abstract
foundations of mathematics in which set theory is one of the
main historical pillars. But Axiom was also developed at a time
that a lot of these historical foundations were being re-considered
by category theorists. In the mean time other people have become
interested in formal foundations for computer science and programming
languages and it has turned out that category is also very useful
for here. And in principle category theory is a good match with
computer algebra systems because in most respects category theory
is essential algebraic.

So at the very least, Axiom shares this culture and language but
unfortunately and largely only for historical reasons, Axiom's
terminology is not well matched to category theory. For example,
Axiom's categories are not mathematical categories and Axiom's
objects are not categorical objects. The word functor is used
in some Axiom literature, but it is not formally defined in the
same way as a functor in category theory.

Some researchers have claimed that Axiom can be better formally
described in terms of the implementation of a many-sorted algebra.

Loosely speaking, Axiom's domains are a lot like mathematical
"categories". For example, 'Set' and 'Integer' can both be
described very accurately as mathematical categories. Domain
constructors that take domains as arguments such as 'Complex x'
where 'x' might be 'Integer', are a lot like mathematical
"functors".

I have argued that the concept of 'natural transformation'
is useful in the definition of the semantics of the 'rep' and
'per' construction that is fundamental to the way that Axiom
and Aldor implement domains.

http://wiki.axiom-developer.org/RepAndPer

But with all that said, it is still my opinion that Axiom is
more that just "somewhat compatible with category theory". I
think large parts of Axiom and specifically the semantics of
Axiom's programming language can be formally and accurately
described using category theory.

> If that's true, I was wondering what sort of effort would be
> involved in tuning Axiom's use of categories to be in line with
> category theory mathematics, along the lines of things like
> Categories for the Working Mathematician.  If Axiom is already
> close to this anyway, perhaps the next step could be taken and Axiom
> could relate its category structure directly to research in category
> theory, and turn its own core implementation of mathematical
> fundamentals into a literate document summarizing the research
> in those areas and how it is applied.

I don't think this is a crazy idea. In fact, this was one of
my own motivations for becoming deeply involved in Axiom. Other
people have also expressed similar ideas about Axiom and Aldor.
See for example:

http://physics.bu.edu/~youssef/aldor/aldor.html

and also look for "category theory" mentioned in the axiom-developer
archives.

The Saunders Mac Lane book "Categories for the Working Mathematician"

http://www.amazon.com/gp/product/0387984038

is now a little "dated" in it's approach although still widely
regarded as having established the foundations for the whole
subject. From the point of view of applications of category theory
in computer science, I think there are several better books for
the beginner, e.g.

 Basic Category Theory for Computer Scientists
 by Benjamin C. Pierce
 http://www.amazon.com/gp/product/0262660717

> 
> Is that a) an insane amount of work and I just don't realize it yet

I think completing this programme (of reformulating Axiom on a sound
category theory basis) would be a lot of work. But I think there
are a lot of useful things would can do with category theory in
the context of Axiom without going this far.

> b) a non-practical idea in terms of having an actual working CAS 
> or

I think it is very practical and I would be quite willing to
help in any efforts along this line.

> c) all of the above?  I always thought the best way to lead off
> the Algebra volumes of Axiom was with a discussion of the
> fundamental theories of mathematics encoded in Axiom and the
> research they are based off of, but perhaps that's not a good
> approach for Axiom?

Category theory at least provides a uniform language in which
to express most of the mathematics implemented in Axiom. But
documentation exclusively and formally based on category might
not be to everyone's taste, even though it is widely used in
mathematics and increasingly in computer science. Probably we
need to be more flexible and suit the kind of documentation to
the subject according to current fashion.

> 
> I'm going to finish a unit and dimension implementation before
> I even think about tackling something that crazy, but I figured
> if it's a really Nutty idea I should find out now ;-)
> 

I also look forward to your completion of the work on units and
dimensions in Axiom, but it doesn't hurt to *think* about other
subjects. :)

Regards,
Bill Page.