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 _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
