[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)
Subject: Re: [Axiom-developer] RE: dependency visualization with VCG
From: Bill Page <address@hidden>
To: address@hidden
Cc: address@hidden, address@hidden
In-Reply-To: <address@hidden>
Content-Type: text/plain
Organization: 
Date: 30 Aug 2003 04:09:01 -0400
X-UIDL: K2p!!X=&#!mI`!!KU1"!

Tim, William;

I think an accurate algebra dependency di-graph has more than
just a curiosity value.

William, I think the analysis and formalism in your previous
message is relevant, however the problem is somewhat simplier
than you suggest. The vertices of the di-graph are just the
*.spad files themselves. These are a subset of the files
contained in the int/algebra and are derived (many to one)
from the *.spad.pamphlet files in src/algebra. The directed
edges between vertices represent pre-conditions for compilation.
Specifically, an edge directed from vertex A to vertex B states
that file B.spad contains some element (function) that is
needed in the compilation of A.spad. (Of course the opposite
convention for the orientation of the edges is also possible.)

Although I admit that you do correctly point out that my
current method of finding these dependencies is deficient in
some respects. I agree with you and Tim that the most accurate
way to obtain this dependency di-graph would be to analyze
the output of the compilation process itself. Now that we
have a full compilation of Axiom that runs to completion,
this is easily achievable.

It is one of the unusual properties of Axiom that the algebra
dependency di-graph may contain cycles. This means that it
is not possible to compile Axiom in the way that most complex
computer systems are compiled. The presence of cycles means that
no linear order of compilation exists. Instead, one must find a
way to *solve* (satisfy) the set of cyclically dependent vertices,
separately from those that follow in a linear manner. We call
a cycle "satisfied" if all of the spad files in the cycle can
be compiled in a self-consistent manner, that is, in such a
way that all the dependencies in the cycle are satisfied.
Operationally, this means that given such a solution for a
cycle, we could repeatedly compile each spad file in turn going
around the cycle with no change in the internal code that is
produced. In other words, the solution is a "fixed-point" for
the cycle.

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

The solution algorthm that Tim has employed in the new open
source version of Axiom starts with a choice of "bootstrap"
vertices. The compiled code for these vertices is given "out
of the blue", that is through some external process (in this
case it is derived from the intermediate LISP code of a previous
version of Axiom). The dependency di-graph is *cut* by
temporarily ignoring all the outward directed edges of these
vertices. The choice of bootstrap vertices is made in such
a way as to produce an acyclic di-graph (lattice) that covers
the orginal dependency di-graph.

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. 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.

I say "in principle" because in actual fact, change in the
bootstrap code with each iteration may not be that significant.
On the other hand, it is not clear to me what are the pre-
onditions on the initial bootstrap code might have to be in
order to guarrantee the existence of a fixed point solution
by iteration. It is also not clear that such a solution is
necessarily unique. So perhaps it is not really possible to
completely eliminate the dependence of Axiom on the initial
choice of bootstrap code.

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
program is designed to perform a "lazy evaluation" on a lattice
of such specific dependencies. If I make a change to coding in
one spad file (by editing a spad.pamphlet file), I want the
make program to use the information in the Makefile to re-compile
only those spad files which are affected (both directly and
indirectly) by my change. This would (usually) be a very short
process compared to recompiling the whole set of well over
1000 files.

The second problem to which Tim has referred, namely attempting
to find an optimal set of bootstrap files also deserves some
attention. Presumably a smaller set of bootstrap files will
converge to a fixed point more quickly that a larger set. And
it is also desirable to have a smaller set in order to reduce
the effort reguired to evaluate the correctness of the initial
bootstrap code.

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

Cheers,
Bill Page.


On Sat, 2003-08-30 at 00:33, root wrote:
> Bill Sit,
> 
> The linear order exists and is documented in the file 
> src/algebra/Lattice.pamphlet. The compiler will tell
> you all of the dependencies at compile time. The subtle
> part is to find the bootstrap set since, in the beginning,
> nothing will compile. That's part of what took so long.
> The other part is that computing the correct location in
> the lattice for all 1100 categories, domains, and packages
> was tedious and time consuming. But it's done.
> 
> I believe the lattice can be further optimized but that's
> just an academic exercise. The reason the lattice has to
> exist in any form is that you need to compile from scratch.
> Once that happens the lattice is worthless.
> 
> I'd like to see it graphed just so I can stare at the beast
> that ate 8 months of my life.
> 
> Tim
> address@hidden
> address@hidden
> 
> 
------- End of forwarded message -------