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

[Ralf Hemmecke]

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

You may be right. But what foundation you use for mathematics is in the 
end a very vague thing. Let's say we base mathematics on category 
theory. Then you have to explain and define a category without using 
mathematics. You have to have a lot of people agreeing on these "common 
sense". Once that is done. The rest is "easy".

I guess, you more easily get people to agree what a set is. It's not 
necessary at first to start with classes.

Anyway, what I want to say is, that mathematics can be based on category 
theory and on set theory. There is no "must" for either of them. You can 
also use higher order logic to start mathematics.

You like different views in LEO. Why do you think different views on the 
foundations of mathematics are bad. (OK, actually, you never said that, 
you just have preferences for category theory.)

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

OK, if Axiom becomes as universal as "the" mathematics, we can leave 
"the Axiom library". ;-)

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

Yes, but it should not force people to just have only *one* view on 
mathematics.

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

Do they also say "it cannot be based 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.

As I said above. The other people actually do handwaiving when trying to 
explain what one should understand by a "category".

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

Right now I don't see how one could implement different views 
consistently. And it certainly costs a lot of effort. But let me have my 
dreams.

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

Maybe I should read "A new kind of science" to understand what Stephen 
Wolfram thinks about what mathematics is.

[snip]

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

In Aldor-Combinat we just are at a point where Aldor seems to be too 
weak to express the idea of multi-sorted species in a natural and 
somehow typesafe manner. Remember my wish.

http://lists.nongnu.org/archive/html/axiom-developer/2007-03/msg00151.html

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

Oh, I mentioned Expression(Grammar) in my last mail. If I allow only 
transformations of expression trees that respect the Grammar, isn't that 
in some way "algebraic".

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

Yes, it agree with the essence of that distinction and that also means 
(at least for me) that Axiom be strong in computer algebra, but allow 
experiments using symbolic computation (which will be hopefully turned 
into proper computer algebra programs later).

Ralf