[Axiom-math] address@hidden: Re: [Axiom-developer] RE: dependency visualization with VCG]

[root]

------- Start of forwarded message -------
X-Original-To: address@hidden
X-MessageWall-Score: 0 (mail-gw.bsdwebsolutions.com)
X-MessageWall-Score: 0 (spam-filter-less.bsdwebsolutions.com)
Date: Sat, 30 Aug 2003 10:12:11 -0400
From: root <address@hidden>
To: address@hidden
Cc: address@hidden, address@hidden, address@hidden
In-reply-to: <address@hidden> (message from Bill Page on 30
        Aug 2003 04:09:01 -0400)
Subject: Re: [Axiom-developer] RE: dependency visualization with VCG
Reply-To: address@hidden
X-UIDL: !6#!!UH`"!5H5"!mM-"!

> In this respect the Axiom code is not strictly "imperative" but
> rather it is a specification of a system that may or may not
> have a solution. And if a solution exists, it may not be unique.
> 
> Bertfried Fauser has pointed out that there is good reason to
> suppose that this sort of cyclical dependency is inherent in
> the underlying mathematics that Axiom attempts to represent. I
> think this has a rather large importance in the philosophy of
> mathematics. But that is subject that is beyond the scope of
> the current discussion

I've added a new mailing list, address@hidden, because
such discussions of math theory and philosophy of Axiom's math
are important and need a proper forum. It should be available
today and I'll announce it to the lists once it exists. Once it
exists lets move the discussion over there.

Philosophically speaking, I'm beginning to think that computational
mathematics (as opposed to pencil mathematics) will begin to uncover
new "axioms" that further refine the mathematical theory. So, for
instance, we might discover that the category division of RNG and RING
exists because there is a logical requirement that has never been
formally stated. The Axiom book contains an algebra hierarchy on the
front flyleaf. Somebody needs to write the corresponding axioms that
underlie each domain. It would be very interesting to see the RNG vs
RING axioms.

(On a side note: I once saw a Venn diagram that showed the relationship
between groups, rings, integral domains, fields, etc. in a book. I'm
unable to find that again. If anyone ever sees it please send me the
name of the book. I want to use that diagram to explain the algebra
hierarchy and I can't find it again.)


> Tim is right that *any* viable selection (quite possiblity
> sub-optimal) of "bootstrap" vertices together with a linear
> ordering is sufficient to build a working version of Axiom -
> and this is hard enough. But really we are not done when we
> have just produced a runnable program. We really need to
> complete the bootstrap cycles and compile each of the
> previously choosen bootstrap spad files as well.             

Actually, if you look at the <<order>> chunk in the makefile you'll
see that a chunk exists after all of the levels. This chunk recompiles
the bootstrap layer code using the compiler. 

This should cover the case where the bootstrap lisp code is not
semantically the same. This will not work in general as significant
changes to the files containing the bootstrap code (e.g. deleting
functions) will break everything.  However, the pamphlet files for the
bootstrap code contain warnings that you have to regenerate and
re-embed the lisp code if you change the algebra.

>                                                  Then we will
> compare the newly generated internal code (LISP) for each
> bootstrap file to the bootstrap code with which that we
> started. If there is a semantic difference between the orginal
> and the new bootstrap code, then we need to repeat the build
> process again, using the new bootstrap code. In principle we
> have to iterate until we reach the desired fixed point for
> all of the bootstrap vertices. Achieving this fixed point
> means that our internal code for Axiom no longer depends on
> the particular starting bootstrap code and it does not
> depend on how many times we have repeated the iterations
> after the fixed point is achieved.

The recompile hack mentioned above will recover from "small" errors
but does not cover the "fixed point" case you mention. However if
the fixed point is not achieved within the one iteration within the
makefile I'd consider the build badly broken.

> But in preparing the algebra makefile for Axiom, I think we
> should be even more ambitious. I think it is very desirable to
> design a makefile script that directly incorporates the specific
> dependencies and not just a viable linear ordering. The make

I originally agreed with you on this and, if you look in the previous
Makefile.pamphlet you'll see that the layer0 files were being added to
each file they depended on. That is, if foo.spad depended on int.spad
I wrote:

foo.NRLIB: int.o foo.spad

This is very fragile as modifications to the lattice had to be propagated
into all of the rule stanzas. So the next "hack" was to generalize the
dependence to the layer thus:

foo.NRLIB: ${LAYER0} foo.spad

Thus any change in the layer 0 files would cause foo to be rebuilt.
This is more robust but causes a HUGE increase in the number of 
recompiles. 

Axiom's algebra is reasonably stable in the face of changes. I don't
expect that people will be making many changes to the "standard library"
that is shipped with Axiom. Code that IS changed or added will have to
be reviewed. In particular the "standard library" code will have to 
build from scratch anyway so changes that break the algebra will show
up (well, mumble, mumble, mutter, mumble) in the build.

> I hope I have not taken us too far afield in this discussion.

It's very relevant discussion but perhaps not of interest to all of
the developers. The lattice solution has caused me to "circle the coffee
table" quite a few times as it was not clear how to solve the bootstrap
problem. Discussions like this would have helped.

There are still more problems that need this kind of discussion such as:

generalization of simplification, 
making simplification "domain controlled",
adding provisos (e.g. saying 1/x provided x != 0), 
proving the algorithms correct, 
adding ACL2 or MetaPRL style computation to the standard library, 
mathematically justifying the computational mathematics (e.g. why RNG and RING?)
taxonomiically ordering the algebra by subject,
...

Indeed, each of these topics and more should eventually become Axiom Journal
articles. Once we figure out the correct way to represent the lattice we
should consider writing up a paper for submission to the Axiom Journal.
Then we can argue over what the "rules" for submission are (e.g. what
is required in a "literate paper", who reviews these things, how to
get such a Journal recognized by ACM or Springer, etc).

In any case, sometime this afternoon there will be an "axiom-math" 
mailing list. I'll forward these mailings to it. Lets continue the 
discussion there. I'm very interested in the result.

Tim
address@hidden
address@hidden
------- End of forwarded message -------