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

[C Y]

--- Bill Page <address@hidden> wrote:

> 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.

Hmm.  That might be worth some consideration when we start thinking
about the Aldor conversion - one of the hardest things for me to do (as
I think the unit discussions in the archives will show) was to actually
define my terms properly (I probably am not all the way there even now)
and it was one of the most important things to do to be able to
communicate effectively.  I think we should try to either use names
that are (at least moderately) common in mathematical and other
research as they are commonly used, or in the worst case clearly define
what we are and are not using the word for in the context of Axiom.  It
will make it FAR easier for researchers to read and use Axiom if they
don't have to re-adjust their understand of common terms (IMHO anyway).
 
> 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".

OK, that makes sense.

> 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.

That would be awesome, and I suspect might appeal to hard core
mathematical researchers.

> 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.

Interesting!  Will do.

> > 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. 

I think that sentence is probably the best summary I have seen or heard
which tells me that Axiom based on category theory is a good idea. 
Axiom would be much more easily understood in whole and part with that
unifying language as a common theme, at least IMHO.

> 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.

Right.  My thinking on the subject was that, beyond the core
implementation of category theory and categories, mathematics done
within that framework (e.g. most of the work) wouldn't need to be
explicitly based on category theory.  It would need to fit within the
framework of course, but one of the main attractions of category theory
as a tool is that it can fit so much within its framework.

> > 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. :)

Actually, I guess the units package is kind of at fault for this train
of thought, not just for the language definition issues but for making
me read up on groups. ;-)

Cheers,
CY

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com