[Axiom-developer] Re: ACL2/Axiom recommendations

[root]

Well, the goal is clearly in the "research" category since there is no
clear roadmap for how to proceed in detail. I have been working my way
through the tutorials you suggested. I suspect that will take me a
while. I did use an early version of the Boyer-Moore work while at IBM
Research but that was years ago, on a different project.



The goal is to be able to prove Axiom's mathematical algorithms.
Axiom algorithms, for the most part, are written in a language
called Spad which lives above and apart from lisp. However, the
Spad code compiles directly to lisp code.

Since ACL2 knows nothing about Spad code directly we need to
understand how to span the gap, especially to span the gap in some
categorically useful way. This involves quite a few sub-puzzles, so to
speak. Ideally there is a useful example that does not go beyond what
ACL2 already knows. Thus, building "toy" categories and domains that
compile to specific code to fit the research question would minimize
the gap.



BDD forms are interesting since ACL2 seems to know how to reason about
them.  The exponential form of the BDD diagram is basically just a
fully developed tree structure which is a direct mapping of the domain
of the function to its range. If we ignore the shared version and just
look at the ordered BDD version it appears that there is a
straightforward way to define the "equals" function which would just
be a node-by-node compare of canonical forms. It seems one could prove
that the "equals" function was symmetric, reflexive, and transitive in
an automated way.

The same could be said of any of the "equals" functions in
Axiom, particularly in the tree domains. The caveat is that the
current domains were not developed with the idea of proofs in mind.

If Axiom had the theorems "attached" to the Spad code and ACL2 lived
under Axiom in the lisp layer, we could automate the proof of (small)
blocks of code.

Of course, there is the mundane issue of how to "attach" theorems
to categories and domains in effective ways, both from the ACL2
and Axiom viewpoints. This will likely involve hacking the Spad
compiler and interpreter.




Thinking in the longer term, though, the game is to figure out how to
really integrate ACL2 into an Axiom environment. Axiom is based on
category theory. Ideally we can control the theorems that are "in
scope" by attaching them to the category hierarchy.  That way it
should be possible to handle domains where functions like
multiplication are non-commutative. The hierarchically inherited
theorems for a commutative domain would differ from the hierarchically
inherited theorems for a non-commutative domain.

In Axiom, a domain can override the definition of categorically
defined functions (e.g. equals). It would be interesting to know if we
could prove that the newly created equals function really was an
equivalence relation, based on the categorical theorems inherited by
the domain.



In the really long term (30 year horizon version), the goal is to 
be able to prove the programs correct rather than test them. So 
the way we prove "equals" correct is more important than proving 
"equals" is correct in a particular instance.



Keeping your feedback in mind, there might be a good example of
"equals" already in the hierarchy which is both categorical and
domain defined. Provided the generated code is not too obscure
that could be a good place to start the struggle.


Tim