Re: [Axiom-developer] The Axiom Library and Category Theory

[Gabriel Dos Reis]

C Y <address@hidden> writes:

| --- Bill Page <address@hidden> wrote:
| 
| > The point of category theory as a foundation for mathematics
| > is that a lot of mathematics can and should be done long before
| > it becomes necessary to define what is meant by "set".
| 
| I have seen a few comments to the fact that it should be possible, in
| theory, to describe virtually all of mathematics within the framework
| of category theory.  If this is true, to me that makes it not only the
| obvious foundational choice for The Axiom Library but the essential
| one.

I've been trying to stay out of this debate...

In computational mathematics, we have computation which brings in
computer science.  Basing math implementation on set theory is, in
both conceptual and practical points of view, like using OO design in
the sense that everything derives from a universal Object type.  That
has been tried many times with failure -- but that won't stop people from
trying again.

On the other hand, Category Theory (or the Theory of Empty Set), does
not require set -- you can do things with small and large categories.
It only cares about *forms and structures*.  From an implementation
point of view, it means that you don't need to require all
computational objects to derive from a single universal base.  That
gives flexibility for composition -- something much harder and clumsy
with OO paradigms (all incarnations that have been tried so fart).

You can failures of OO thinking in the current library in forms of the
curious Abelian Monoids that are not Monoids.  No undergrade in math will
get away with that.  But, Axiom apparently does :-(

So from my perspective (*Computational Math*), the question is not on
what Math is based, but on what computation is based and which
framework allows for easy of composition and extension.


-- Gaby