[Axiom-developer] The Axiom Library and Category Theory (was: Defining piece-wise functions and drawing, integrating, ...)

[Bill Page]

Topic drift is a wonderful thing ... :-)

On June 4, 2007 6:36 PM Ralf Hemmecke wrote:
> Bill Page wrote: 
> > I would agree to replace "Set" with something more algebraic,
> > e.g. a topos.
> > 
> > http://en.wikipedia.org/wiki/Topos
> 
> Cool. ;-) How many people know topoi in contrast to the number
> of people who grew up with sets?

Well, I do hope that the number of people in mathematics and
computer science who have grown up with category theory is
increasing at the same or greater rate than the number of people
retiring from these professions who still think that set theory
is the proper foundation of all mathematics ... ;)

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

> 
> > The short answer to why everything must be algebraic is:
> > category theory. You can ask why try to base the Axiom
> > library on category theory, but that is an argument at a
> > very different level.
> 
> Oh, I have no problem with basing a library on category
> theory. But maybe at some point we should drop the "the"
> in "the Axiom library".

I am not convinced. Do you think it makes sense to drop "the"
in reference to "the Internet"? In the same way I would hope
that the mathematics implemented in Axiom is somehow
"universal" and not merely just one of several ways of doing
things. Removing "the" from the "the Axiom library" seems to
reduce Axiom to just another (albeit rather sophisticated)
programming language.

So I think that we should at least try to define "the Axiom
library" even though this may prove impossible except perhaps
in the very long term.

> 
> In fact, I would love to see a system that allows different
> views. As mathematics can be based on set theory or category
> theory. 

Maybe it is just where I live but I think most mathematicians
since about 1975 or so have agreed that one should not try to
base mathematics on set theory.

> 
> > In fact I think it is quite wrong that Axiom's library
> > places SetCategory so near to the top of the algebra
> > hierarchy. It would be better to start with something more
> > primitive like the concept of a Cartesian close category.
> 
> I already hear people saying ... but hey, "sets" are much 
> simpler than ccc's.

I think perhaps these people simply do not know what a "set"
is.

> 
> There are just different views and Axiom should support both
> of them and even more.

Right now I do not agree. I do not want Axiom to be so "relative".
Such a point of view might be alright for a programming language
like Aldor that is trying to be many things for many different
people. But (in my view) mathematics is not like that and neither
should Axiom be.

> 
> >> Actually, you could probably turn an ExpressionTree
> >> into some form of universal algebra (just leave the set
> >> of operations empty).
> > 
> > That would not make me nearly as happy as category theory.
> > :-(
> 
> OK, you are responsible to start a library that builds on 
> category theory.
> 

Well I have been thinking about and writing about on this email
list for a few years now... I would very much like to "get my
head above water" long enough to concentrate on issues like
these. Unfortunately we are still trying to decide things like
what source code management system we should be using... :-(

> >> Oh, maybe SExpression is near to what I want. But is
> >> somehow sounds to LISPish for me. ;-) Anyway, I think it
> >> would be a good thing to have a very general expression
> >> domain (maybe like SExpression) and yet others that only
> >> allow certain expression trees that correspond to a
> >> grammar.
> 
> > Yes. I think Gaby had some ideas along that line. We
> > discussed some aspects of that here:
> 
> > http://wiki.axiom-developer.org/SandBoxInductiveType
> > 
> > and on this list.
> 
> I don't think that this would allow me to transform the
> program (= inductive type) at runtime as I could do with
> expression trees.
> 

Well I am not so sure exactly what we need to be able to do
at "run time". Certainly one of the points of Aldor is to
define a *static* type system that is strong enough to express
abstract mathematics but which can still be resolved entirely
by the compiler. Among other things this means that we have
higher-order functions and dependent types.

I do think that part of the point of the Axiom "all things
algebraic" philosophy is that things such as transforming
expression trees should not be viewed as fundamental to do
doing mathematics by computer. In other words there is a
distinction between symbolic computation and computer algebra
that I have mentioned several times before and that I think
Stephen Watt has described so well.

Regards,
Bill Page.