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. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
