Re: Axiom musings...

[Tim Daly]

Mark,

You're right, of course. The problem is too large.
So what. is the plan to achieve a research result?

There are 3 major restrictions on the effort (so far).

First, the focus is on the GCD in NonNegativeInteger.
Volume 13 is basically a collection of published thoughts
by various authors on the GCD, a background literature
search. Build a limited system with essentially one user
visible function (the NNI GCD) and implement all of the
ideas there. This demonstrates inheritance of axioms,
specification of functions, pre- and post-conditions,
proof integration, provisos, the new compiler, etc.

Second, make the SANE GCD work in the current Axiom
system by generating compatible code. This gives a
stepping-stone approach where things can be grounded.
Obviously none of the new proof ideas will be expected
to work in the current system but it "gives a place to stand".

Third, develop a lattice of functions. The idea is to attack the
functions that  depend on almost nothing, prove them correct,
and use them to prove functions that only depend on the
prior layer. I did this with the category structure when I first
got the system since it was necessary to bootstrap Axiom
without a running system (something that was not possible
with the IBM/NAG version). That effort took several months
so I expect that function-lattice to take about the same time.

This makes the research "incremental" so that a result can
be achieved in one lifetime. Like a PhD thesis, it is initially
intended as a small step forward but still be a valid instance
of "computational mathematics", deeply combining proof and
computer algebra.

Tim