RE: [Axiom-developer] [MutualRecursion] (new)

[Page, Bill]

On Tuesday, January 18, 2005 3:50 PM Peter Broadbery wrote:
> ...
> > > 
> > > I wonder how the Aldor compiler handles such mutual
> > > recursive structures. Perhaps Peter Broadbery knows.
> > 
> > I would also like to know.
> 
> [Disclaimer: I'm not an expert on the type checking bit -
> and if you want info, it is nicer to ask]
>

It's great to find out that there is someone here to ask!
Thank you very much for taking the time to explain. In the
future I will try to ask in a more polite manner. :)

> ... 
> If you have a situation with mutually referencing domains
> in separate files, then you have to use the extend keyword,
> and build the defn. up in steps - there may well be an
> example or two of this in the aldor library sources shipped
> with the compiler.

The point of this discussion (for me at least) is to understand
the problem of attempting to build the Axiom library from spad
code alone. Apparently in the previous century Axiom had always
been built using a running system. (So says Tim Daly.) So it
seems that the Axiom algebra evolved incrementally over time,
gradually building one layer on top of another and (for the
most part) discarding the information about the path that
lead to the then current state of the library. Each port of
the system to a new environment was built with the resources
of the old and as a whole over time the library became more
tightly integrated and highly structured. This seems like a
remarkable thing to study from a historical perspective since
it seems to run counter to the evolution of most software.

Anyway, the short story is that at the present time we do
not "build the defn. up in steps". Instead we use a bootstrap
based on lisp code that maintains a tenuous but essential
historical link with the past that goes beyond the spad code
itself. This leave me with the concern that what Axiom is now
may be at least in part determined by the path that got it
where it is today (about which almost no detailed information
is available). Or viewed another way, some essential aspects
of Axiom may be hidden in the "low level" previously generated
bootstrap lisp code and not apparent in the current "high level"
spad code.

But with more than 1,000 strongly interdependent algebra domains,
categories and packages, building up the current algebra
incrementally by successive extensions of the kind supported
by Aldor seems like it would be a very time consuming and
largely uninteresting task. From what I have seen so far, only
a small part of the Axiom algebra has so far been implemented
in Aldor.

So instead of using a series of incremental extensions, my
current proposal is that we can define the compilation of the
Axiom algebra library as a particular type of fixed point,
namely that point in the iterated re-compilation of the entire
library where the compiler generated lisp code does not change
from one iteration to the next. All the lisp code (and of
course the object code compiled from the lisp code) is then
determined only by the spad code itself and not from the any
remnant of the bootstrap lisp code.

There is the formal problem of the uniqueness of the particular
"solution", i.e. for example is it a "least" fixed point?
Perhaps starting with a somewhat different set of bootstrap
lisp code could yield a different fixed point solution? But
in practice I think that having at least one self-consistent
compilation of the mutually recursive mathematical definitions
in the Axiom library will be adequate for most purposes.
Ultimately the kind of things that I can imagine would be to
support the proof of the formal correctness of substantial
parts of Axiom's library.

Given the "flexibility" of the Axiom compiler (some might call
it a weakness), perhaps there is some practical half-way point
where some parts of the Axiom library are defined by a fixed
point iteration and other parts by the Aldor-like method of
formal extensions. I think that the little experiment at

http://page.axiom-developer.org/zope/mathaction/MutualRecursion

shows that this is possible in principle.

> 
> The problem then shifts to the category level, which can't
> be extended.

Are you speaking about the Aldor language or about some formal
limitation? Is it true that there are no circular definitions
(cyclic dependencies) among the Axiom categories?

> 
> > > 
> > > Maybe this example is easy, because both domains are in the
> > > same file. Do you know a good example where it makes sense
> > > to put the domains much more away from each other?
> > 
> > I can not give a simple example right now but I suspect that
> > this happens very frequently in Axiom's algebra.
> > 
> 
> All over - try OutputForm as an example.
> 

So then it is remarkable is it not, that it is possible at all
to compile this whole tangled mess of code into a (mostly)
consistent computer algebra system?

Regards,
Bill Page.