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