[Axiom-developer] [axiom] Axiom Development

[root]

>In a nutshell, I'm interested in many aspects of the AXIOM project but
>my immediate problem is funding.  I noticed you mention a number of
>potential sources of funding on your TODO page.  I'm wondering if you
>have any advice on how I could proceed.

So far there have been no positive replies about funding Axiom.
All of the funding involved comes from my own pocket except for
the server services from the free software foundation. One of
these days I should send them a donation. It would be nice to
be able to work on Axiom full time but that won't happen again
in my lifetime.

>My background is in pure math.  I received my PhD under Raoul Bott at
>Harvard.  My mathematical research centers on the interplay between
>polyhedral geometry and algebraic geometry.  However, for about the
>past year I've been working in the CS department at the University of
>Utah.  Unfortunately, I recently learned that my support here will end
>in 3 months, so I am looking at various possibilities for employment
>or funding after that point.

I know a tiny bit about algebraic topology but nothing about 
algebraic geometry. If you can recommend a textbook I'll look
at it and suggest a possible connection to Axiom. Or you could
check with Jon McCammond at UC Santa Barbara. He's been doing
work in Geometric Group Theory. (address@hidden).
Also see www.math.ucsb.edu/~jon.mccammond/geogrouptheory/people.html

>In my more recent involvement in computer science, I've focused on
>computer language design and formal methods.  (By the way, I'm okay
>with Common Lisp, but I prefer languages like Haskell and OCaml for
>internals.  I'm also good with Java, which is well suited to some
>kinds of cross platform user interface work.)

Heathen! :-) Sorry, that one got away. Common Lisp is a useful
implementation language because the source text and the data
structures use the same syntax, a feature we use quite often.
There is nothing sacred about it, however, as the Aldor compiler
is implemented in C (Aldor is Axiom's standalone compiler).

>One of my ideas is to work on computer algebra.  I am drawn to this
>for several different, partly incompatible, reasons, having to do with
>my mathematical research, my interest in computer programming
>languages, and my experiences teaching mathematics.

>First, there's the open source issue, about which I'm sure you need no
>convincing.  For commercial systems like Maple, and especially
>Mathematica, cost is exorbitant, open documentation is lacking,
>precise semantics are lacking, source code is not freely available,
>etc.  This is a big negative for both teaching and research.  It's
>long been one of my dreams to have a high quality open source symbolic
>mathematics system.

Actually, a large portion of the computational math community has the
same issue. Almost everyone I've spoken to wants open source so they
can do various things (not the least of which is to fix broken code).

>My second reason has to do with my experiences using symbolic
>computation in my research.  I've used general purpose programming
>languages for this, general purpose CA systems, and domain specific
>systems.  I've had mixed success with all three breeds.  My chief
>complaint has nothing to do with efficiency or fast algorithms.  I'm
>more interested in reliability, usability, and especially
>expressiveness.  General programming languages don't have the
>facilities, systems like Mathematica are inadequate in abstract
>domains like algebraic geometry, and domain specific systems lack
>flexibility and constantly reinvent the wheel in ad hoc and limiting
>ways.  I find the difficulty of expressing mathematics in programming
>languages a fascinating problem.

According to Daly's Hasty Generalization Theorem (TM) there are 3
kinds of computer algebra system. 

Type 1 is the library approach. The insight begins with the fact 
that their favorite language has a type system and there is a nice
mapping from types to abstract algebra. A large library gets built
which no-one can use except the developers because it is complex.
An interpreter is usually placed over the library to make it more
useable but the library is the key.

Type 2 is the engineering approach. Do whatever is necessary to make
it work. The key symptom is that you can subtract two types, say
matrices, and get a 0 (integer). Note the loss of type information
because a 0 is a 0 is a 0, right? These systems are easy to use at
first but they have trouble scaling because the coercions that make
it work also turn out to be the source of bugs in more complex situations.

Type 3 is the theory approach. The symptom is that a language is
defined that is close to the mathematics you want to express. This
makes the algorithms clearer and, therefore, easier to get right.
The problem with these systems is that they have very steep learning
curves making them hard to learn initially. However, they scale
better because they have good theoretical models and you can strongly
argue for the correctness of the results.

Axiom is a type 3 system. It is harder to learn but, once learned,
it becomes easier to write correct algorithms.

>My third reason has to do with my more recent involvement in computer
>science where I've gained some knowledge of programming language
>design.  I'm particularly interested in advanced type systems, module
>systems, and other devices that balance expressiveness with structure
>and safety.  From this point of view, systems like Mathematica are
>rather undisciplined.  Simply carrying state of the art language
>design to the CA world seems a worthy undertaking, but this is just a
>first step.  An even bigger ambition is to reverse the process -- to
>explore the deep and rich domain of mathematics as a vehicle for
>research in programming language design itself.

The Aldor (external compiler)/Spad (internal compiler) language
IS state of the art. Very few languages have dependent types,
parameterized types and types as first-class objects. Stephen
Watt and his team have done some very impressive work in this
area (www.aldor.org). Also check out references to Manuel Bronstein
(Sumit) and Nicolas Mannhart (Piit). Having been directly involved
in defining and implementing 4 commercial programming languages
I'm kinda burned out in this area.

>These three reasons cover a huge amount of ground, a good deal of
>which overlaps with the goals of the AXIOM project.  Like I said,
>there are also some incompatibilities; experimental research in design
>is somewhat at odds with the goal of producing a polished system
>targeted at teachers, students, and ordinary users.

Half the teachers in France want to use Axiom for teaching in a
much more polished form so there is a lot of support there. Send
mail to the address@hidden mailing list and see what support you
find (they may even have a job opening). Gilbert Baumslag at 
CCNY wants to converge the Magnus user interface with Axiom.
Magnus has a "zero learning curve" philosophy and a completely
different direction than any other computer algebra system.
(see www.grouptheory.org for Magnus)

>So where in this expanse of possibilities would it make sense for me
>to work?  That has everything to do with funding.  Like I said, my
>current funding runs out in 3 months.  I can bear a lapse for a few
>more months after that, but I can't work indefinitely without support.

Unfortunately I'm recently re-hired myself (I was one of the chosen
17000 Worldcom layoffs). The people page listed above could give you
a list of places to apply, I guess.

>Keep in mind that getting funded in computer science is tricky for me
>because I have no formal background in that field.  I have to lean on
>my math background and the credentials of my collaborators.  Here are
>some rough ideas for specific kinds of project proposals I have in
>mind:
>
>1.  General user interface, usability, accessibility, development for
>AXIOM.  The tools and libraries needed to make top quality end-to-end
>usability and packaging feasible are just now coming together in the
>open source world.  This would be pitched as a means of growing the
>AXIOM community and improving AXIOM as a tool for education and 
>research.

I would recommend taking a look at TeXmacs as a possible place to
start. Joris van der Hoeven is the author and has exactly the same
goals (address@hidden). Andrey Grozin is another contact
(address@hidden).

>2.  AXIOM in education.  I've taught most of the undergraduate courses
>in math at the U. of Utah, where we've generally used Maple.  I'd
>propose working with the math department on integrating AXIOM into some
>of these courses, and using the experience to improve AXIOM as a
>teaching tool.

Memory fails me for the best contact but check with Paul Zimmermann
(address@hidden). He can put you in touch with people
who share your interest in this.

>3.  Integrating AXIOM with theorem proving.  I'm right now working
>with one of the principal developers of the HOL theorem proving system
>(who happens to be in the Utah CS department).  I don't speak for him,
>but he and I have discussed integrating HOL with computer algebra and
>I think he'd be interested if we could get funded to do the work.

The best contacts here are either at UTexas (ACL2, contact
Michael Bogomolny <address@hidden>) or Cornell (MetaPRL,
contact Sergey Artimov)

>4.  Programming language research in the context of symbolic algebra.
>I've discussed this idea with one of the computer languages people in
>the CS department.  He's an expert in component and module systems and
>the principal developer of PLT Scheme and the Dr. Scheme development
>environment.  (By the way, Dr. Scheme's design is very flexible and it
>can be easily modified to provide a development environment for a
>computer algebra system.)  Again, I don't speak for him, but he seems
>enthusiastic about the idea.

I'm unfamiliar with PLT Scheme or Dr. Scheme, though I've used scheme
in the past. Axiom requires some low-level mods to most lisps to
support things like sockets and dynamic loading of native code.
Plus we plan to push Axiom into parallel programming so there would
have to be some support for MPI. I have set up a beowulf so I'm
interested in reflecting this parallelism into the type hierarchy
and the data structures. 

Hope this helps.

Tim