--- Bill Page <[EMAIL PROTECTED]> wrote:
> I would say that this goal is certainly very disconnected from
> reality. I think comparing computer typesetting (TeX) to computer
> algebra (in general) is rather like comparing arithmetic to
> mathematics (in general). We know pretty well how to do typesetting
> and basic arithmetic by computer. And arguably the technology to do
> these things hasn't changed very much in the last 30 years (not
> withstanding a few significant innovations in numerical algorithms
> and vectorized font systems etc.).
Right. So those abilities and algorithms should be defined once,
reliably, and then used with confidence in the results. As innovations
are found we can implement the new algorithms and call them if we find
they are better.
> But the goals of Principia Mathematica
> (a universal treatment of mathematics) has been shown by
> mathematicians themselves (e.g. Geodel's theorem) not to be
> attainable even in principle.
OK. So then, how DO we work with mathematics? (I don't expect an
answer - but it's still a reasonable question, unless one wants to
throw up one's hands. A universal treatment (whatever that means)
might not be possible, but what is the best solution (or solutions)
that ARE possible?)
> Similarly it seems to me that we just barely have
> a few clues about how to use a computer to do algebra and more
> general mathematics. We don't really know what programming
> languages and systems might or might not be appropriate.
If we design a system that supports (as nearly as possible without
introducing ambiguity) the way mathematicians are expressing themselves
it seems to me we are doing as well as anyone CAN do. Anyway it seems
a reasonable direction to proceed, unless someone has better ideas.
> As interesting as Axiom is as a research project, realistically Axiom
> (nor any other computer algebra system today) is nowhere near
> reaching these goals.
Agreed. We need to get busy ;-).
> If by some miracle we actual had a bunch of energetic
> mathematicians and developers working full time on Axiom right now,
> we would likely still be scrambling just to catch up with other
> systems that have become much more capable while Axiom has slept.
Sure, if you count features. But can any of those systems take an
answer and use their internal routines to guide the creation of an
axiomatic proof of a answer? Something that could be verified by ANY
mechanical proof checker that understand the chosen language, or even a
sufficiently patient human? Without that, how can we trust the results
of any system? Why should scientists depend on a tool they can't know
is without error and have no hope of verifying?
> But like Principia Mathematica, I think there is a very real
> possibility that Axiom's strongly-typed object-oriented approach is
> not capable even in principle of serving as the foundation for
> a "universal" solution to doing mathematics by computer.
I would be curious what branch(es) of mathematics you think Axiom will
be incapable of dealing with, via one form or another of extension? Is
there any possible system you feel would be MORE useful?
> Maybe mathematics is necessarily an
> activity that must be carried out in a less structured way and so
> computer systems would necessarily have to be designed in a manner to
> support this. I just don't know.
Neither do I. But the structured approach to mathematics seems to
yield many useful practical results, even if it cannot be all-inclusive
and remain self consistent. Perhaps we need the ability to select the
structure in which we wish to approach a given problem.
I would like to understand more thoroughly Godel's work - while I am
sure it is true in general I am not sure how much of a problem it
presents for systems like Axiom. Surely it's worth finding out.
> Anyway, research and experimentation is necessary at several
> different levels and if in the end you decide to spend your time
> working towards a goal that seems so far away to me that we can
> only just barely imagine it, who am I to try to suggest you do
> otherwise. ... :-)
If no one works toward those goals, where does the truly new work come
from? I don't suggest I am capable of such work, but I WOULD like to
make it as easy as possible for work to be done towards those distant
goals. Also, I would like to "future proof" work that has already been
done, so that as long as it is useful to the system it can be depended
on to work. Recovering ground previously covered is always a waste.
Dealing with OS related implementation details is a nusiance that
should be minimized as much as possible.
Am I nuts? Probably ;-). I don't know if even Tim shares my views in
this respect. I know I'm not a good fit for FriCAS, perhaps I am not a
good fit for Axiom. But what else can we do in a volunteer project but
pursue our interests? If those are not compatible with the project, I
can work on my own - I have no wish to disrupt anything any further
than it has already been disrupted.
Cheers,
CY
____________________________________________________________________________________
Moody friends. Drama queens. Your life? Nope! - their life, your story. Play
Sims Stories at Yahoo! Games.
http://sims.yahoo.com/
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
