[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] Re: The Axiom Library and Category Theory
From: |
Ralf Hemmecke |
Subject: |
[Axiom-developer] Re: The Axiom Library and Category Theory |
Date: |
Tue, 05 Jun 2007 08:02:31 +0200 |
User-agent: |
Thunderbird 2.0.0.0 (X11/20070326) |
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
- [Axiom-developer] RE: Defining piece-wise functions and drawing, integrating, ..., Bill Page, 2007/06/03
- [Axiom-developer] Re: Defining piece-wise functions and drawing, integrating, ..., Ralf Hemmecke, 2007/06/03
- RE: [Axiom-developer] Re: Defining piece-wise functions and drawing, integrating, ..., Bill Page, 2007/06/03
- Re: [Axiom-developer] Re: Defining piece-wise functions and drawing, integrating, ..., Ralf Hemmecke, 2007/06/04
- RE: [Axiom-developer] Re: Defining piece-wise functions and drawing, integrating, ..., Bill Page, 2007/06/04
- Re: [Axiom-developer] Re: Defining piece-wise functions and drawing, integrating, ..., Ralf Hemmecke, 2007/06/04
- [Axiom-developer] The Axiom Library and Category Theory (was: Defining piece-wise functions and drawing, integrating, ...), Bill Page, 2007/06/05
- [Axiom-developer] Re: The Axiom Library and Category Theory,
Ralf Hemmecke <=
- Re: [Axiom-developer] The Axiom Library and Category Theory, C Y, 2007/06/05
- Re: [Axiom-developer] The Axiom Library and Category Theory, Gabriel Dos Reis, 2007/06/05