[Axiom-developer] Vicious circles (was: More AxiomUI)

[Page, Bill]

I think this discussion of Aldor's "post facto extension"
mechanism is directly related to the issues of circular
dependencies and Mutual Recursion in the Axiom libraries
that we discussed some months ago. See for example:

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

On Wednesday, June 22, 2005 1:43 PM Martin Rubey wrote:
> ...
> In fact, this is also a question of future direction, since I
> hope very much that Aldor will become *the* language for Axiom.
> ...
> William Sit writes:
>> 
>> What features of Aldor do you want to add to Axiom?
>
> A clear grammar, dependent types, post-facto extensions, and all
> the splendid algorithms available in the libraries distributed
> with aldor.
> ...
>> a direct coercion between two domains of the same category is
>> by design, I think, not practical. Domains may differ by their
>> mathematical meaning, but even if they do not, they differ by
>> their data structure (and hence implementation). When a domain
>> is constructed, it should not be required to be aware of other
>> domains in the same category (providing coercion would), because
>> for one thing, it may be the first. Thus such a requirement
>> would require constant updating of all older domains that in
>> principle are coercible to other "younger" ones. Note that by
>> the same reasoning, only a younger domain can be CoercibleTo an
>> older domain, not the other way round. (By making CoercibleTo
>> go the other way would make "older" become the "younger").
>
> Part of this problem is solved (in a fine manner) by post-facto
> extensions, described in the Aldor user guide.
>

Reference:

ALDOR Compiler User Guide,
Chapter 10: Post facto extensions

http://www.aldor.org/docs/HTML/chap10.html

------------

In Axiom this "problem" of mutual recursion and circular dependencies
still exists. Axiom has a very large number of algebra domains,
categories and packages (over 1,000) which over time with each new
extension have grown more and more tightly inter-related. The
graph of dependencies between these modules contains more that
30,000 directed edges. As Tim discussed way back in the early
days of the open source Axiom project, this graph contains many
loops and so these modules can not be topologically sorted into
a partial ordering that allows a single execution pass which will
produce consistent compiled code.

As an interim measure Tim designed a "lisp bootstrap" into the
current Axiom build process. A relatively small number domains and
packages (about 30) have been coded in both lisp and in the Spad
language. The set of 30 modules have been chosen so as to break
all of the circular dependencies in the Axiom library. These
modules are initially compiled directly from the low level lisp
code. Then all of the dependent domains and packages are compiled
from the Spad source code in a series of "layers" which do not
contain any cycles. Finally the original 30 bootstrap modules
are also re-compiled from their Spad sources. And the result is
a runnable Axiom system.

Remarkably perhaps, it turns out that this bootstrap procedure
is not sufficient to produce completely consistent code for
all of the Axiom modules. When one compares the intermediate
lisp code that is generated from the first pass of compilation
of the Spad sources to the lisp code generated by a second pass
one discovers that there a small number of modules (about 10)
in which the generated lisp code changes from one iteration to
the next. These changes are not trivial changes such as non
semantic changes in the names of internal symbols, but rather
involve actual changes in the detailed lisp logic generated by
the Spad compiler. It currently takes 3 complete re-build
iterations before the lisp code generated between iterations
reaches a "fixed point".

A preliminary (but incomplete) analysis of these changes was done
by Steve Wilson, Tim Daly and me. Our conclusions was that most
(maybe all?) of changes that we could trace involved additional
optimizations done by the Spad compiler based on the more complete
information on other domains in the various loops that become
available as each re-compilation iteration takes place. So far
we have not found any cases were the detectibly different results
are computed by the code modified (optimized?) but the iterations,
although in some cases bounds on the maximum size of index
variables do change because the compiler makes different choices
regarding data types (for example machine integers instead of
infinite precision integers).

At the present time only the Windows binary versions of Axiom
have been compiled to the "fixed point". The make script for
the Linux versions and for Windows source code version performs
only one iteration of the algebra compiles.

----------

In any case, the reason that I reviewed all this here is because
I think it relates to the problem discussed by Martin and William
above. It seems likely that the mechanism of post facto extension
in Aldor was conceived partly in response to the designer's
experience with the complex dependency structure of the Axiom
algebra library.

The issue of object-oriented programming and type inheritance
has recently been re-consider by


who seem to reach similar conclusions to those of the original
Axiom developers: the conventional type inheritance rules of
(most) modern hierarchical object oriented programming languages
is not really adequate for programming mathematical algorithms.
See for example:

"Approaching Inheritance from a "Natural" Mathematical Perspective
and from a Java Driven Viewpoint" by Marc Conrad, Tim French,
Carsten Maple, and Sandra Pott

http://page.axiom-developer.org/zope/Plone/refs/articles/McTfCmSp-axiom.pdf/
view


"Mathematical Use Cases lead naturally to non-standard Inheritance
Relationships" by Marc Conrada, Tim French, Carsten Maple and
Sandra Pott

http://page.axiom-developer.org/zope/Plone/refs/articles/m_conrad-axiom.pdf/
view

--------

In fact I think Axiom already implements this same sort of post facto
extension of domains, al beit in a less well-structured way by
exploiting mutual recursion and circular dependencies. The bootstrap
mechanism developed by Tim seems to provide just enough "pre-facto"
information in the Axiom bootstrap so that the post-facto extension
is (probably?) is not needed.

It may come as a surprise to some people that it is possible at all,
in principle, to compile consistent computer code from what amounts
to essentially circular definitions. This might be especially worrisome
in the context of a *mathematical* software system such as Axiom
since it seems to suggest that Axiom's implementation of the mathematics
might somehow be fundamentally flawed and could be at least formally
not well-founded. It seems however that some mathematicians have
had some new ideas bout this sort of circular dependency and non-
well foundedness just in time for possible application to Axiom.

The book "Vicious circles: on the mathematics of non-well-founded
phenomena" by Jon Barwise and Lawrence Moss, Publisher: Center for
the Study of Language and Inf. (August 4, 2004).

"Circular analyses of philosophical, linguistic, or computational
phenomena have been attacked on the assumption that they conflict
with mathematical rigor. Barwise and Moss have undertaken to prove
this assumption false. This volume is concerned with extending the
modelling capabilities of set theory to provide a uniform treatment
of circular phenomena. As a means of guiding the reader through
the concrete examples of the theory, the authors have included many
exercises and solutions: these exercises range in difficulty and
ultimately stimulate the reader to come up with new results. Vicious
Circles is intended for use by researchers who want to use hypersets;
although some experience in mathematics is necessary, the book is
accessible to people with widely differing backgrounds and interests.

The following partial table of contents shows that it deals with
many issues that are potentially applicable to Axiom's algebra
library and computer algebra in general.

2. Background on set theory
3. Circularity in computer science
4. Circularity in philosophy
5. Circularity and paradox
6. The solution dilemma
7. Bisimulation
8. Graphs
9. Modal logic
10. Streams
11. Games
12. Modeling the semantic paradoxes
13. Greatest fixed points
14. Uniform operators
15. Corecursion 

---------

While I have to agree that the Aldor probably represents a significant
technical advance in terms of compiler design over the older library
compiler that is built-in to Axiom, I am not yet completely satisfied
that Aldor necessarily provides a complete solution to problems of
dealing with the complex circular dependencies in the Axiom algebra
library. The flexibility that is inherent in the current less
structured approach to building Axiom's library code might very well
be one factor that has contributed to the remarkable breadth of
mathematical knowledge that is captured in this computer code. If
we move to a more rigorous and formally structured library compiler
language such as Aldor, will we be giving up some important features
of Axiom's design (accidental or not as it may or may not be) just
because we do not quite understand yet how to formalize it?

Regards,
Bill Page.