[Axiom-developer] Embedding Axiom

[Tim Daly]

This is a request for design discussion for those who are interested.

I am rewriting Axiom into literate form. This involves understanding
Axiom in a very deep way. One of the insights of my current understanding
is that Axiom needs to be restructured internally.

I have to say that if you are not a lisp programmer most of this will
not make sense. If you are a lisp programmer it should be obvious.

For the non-lispers, a few comments are in order. As pointed out in
Structure and Interpretation of Computer Programs, a properly formed
lisp program "embeds" in lisp. When carefully designed, a lisp
program is not "on top of lisp", but the result is "just lisp".
That is, the new code is layered so that Spad becomes something like
a domain-specific language. If this does not seem like a deep
philosophical design issue then I highly recommend "On Lisp" by
Paul Graham.

The current state of Axiom internals is more like a history museum
than a robust layered design. There are code fragments dating back
to the late 60s along with clever research algorithms (for the time)
about zipper-parsing and CLU-capsules. There are maxima and vmlisp
concepts left over from prior ports. There are non-standard interfaces
to networks, C, and Fortran. There is a broken attempt at a python-like
syntax. Axiom was a research project of many interests and it shows.

Those who have been following Axiom releases know that I've been rewriting
the lisp code and so I've been spending some time rethinking the whole
of the internals.

I believe that there needs to be clearly defined layers of abstraction
that build up to full support of the algebra library. I have several
motives for this, including native support for literate documents and
a more robust platform for my proviso research.

Some primary design goals are:
 * the algebra and interpreter semantics should be identical, as far as 
possible.
  
 * the embedded design should target the lisp compiler as "the compiler",
   that is, the existing algebra code should just be a layered-syntax 
on the
   embedded lisp implementation. This would allow further layering of the
   system since a Spad "integrate(sin(x),x)" is really just a lisp-form
   "(integrate (sin x) x)". Note, however, that this is NOT the boot-code
   cheeseball idea of "pretty piles". Rather this would be isomorphic
   mappings between Spad and Lisp so all of the concepts of one are in
   the other.

 * the system structure should be designed to allow a "different direction"
   for the algebra since another research goal is to provide a way to
   "prove" (philosophical caveats here) that the algorithms are correct.
   Ideally this would just amount to more surface syntax layered on the
   underlying structures that a reasoning engine like COQ or ACL2 could 
use.

 * the layering should be "natural enough" so that it can be explained in
   literate text. A long term goal of the Axiom project is to make the 
whole
   system into a literate document that can be taught to the next 
generation.


All of the computer algebra systems I've seen are really just "stuck onto"
their underlying systems. You can see the struggle to marry the algebra to
the platform aka "algebra by accretion".

Instead I want to see the Axiom category/domain/package hierarchy be a 
natural
embedding on a prior layer that is prepared to "express the concepts" in the
hierarchy in natural ways. That layer embeds on a prior layer, which 
embeds on
a prior layer.... it is turtles all the way down. (Since it is an embedding,
"down" is the wrong concept but...)

I have some plans on how to get "from here to there" in a slow, incremental
fashion. These plans involve things like finding the basis-set of the 
algebra
in terms of lisp functions and then trying to find a closure of this 
basis set
so that the algebra embeds cleanly in this set. The compiler should compile
that basis set into an embedding in the prior layer. Lisp can support this
by defining domain-specific languages for each layer and macros from one 
layer
to another.

I have no idea what the final form will be. I do know that you should be 
able to
look at any layer of code and know immediately what it means in terms of the
next layer down. The compiler and interpreter should be able to walk the 
same
layers and generate the code that supports the understanding.

When it is done in this properly embedded fashion you should be able to
(mapcar #'(lambda (f) (integrate f x)) '((sin x) (cos x) ...
or use the Spad surface syntax to generate the same results.

At which point we can climb upward to a category-theoretic form...

And perform computational-mathematical proofs of algorithms...

And re-express the whole of the algebra in program transformations,
like transforming generalized grassmann expressions into efficient
linear algebra forms when the compiler knows the provisos...

And computational mathematics that involve simple classroom exercises
using the intermediate languages from their literate textbooks...

And have the open-source research supported by NSF funding...

oops...that last one is pure fantasy :-)

Tim