>Perhaps there are issues around this that will matter? Given that there >are two formulations of each algebra, one like this:
>zero: () -> $ >succ: ($) -> $ >and one like this: >+ ($,$) -> $ >If one form is needed for inductive proofs and the other form for >applied mathematics. Could Axiom hold both forms in a single >category/domain and switch between them as needed? Indeed this is a fundamental question. Holding both forms is not the correct path since it keeps the "mathematical form" separate from the "computational form". The point of this work is to "ground" computational mathematics. So it is necessary to unify these two forms. The approach to this problem relies on the fact that Axiom has proofs not only at the spad layer (using COQ) but also at the lisp layer (using ACL2). After that comes C and then Intel. There is a "proof tower" architecture (I failed to mention): Spad: COQ Lisp; ACL2 C: ? (Frank Pfenning at CMU has OC, a proven subset and there is some LLVM based work I've seen) Intel: I spent 6 years developing the semantics of the Intel Instruction Set as a Lisp program. It goes from binary to Conditional Concurrent Assignments which can be used for reasoning about hardware state: ( http://daly.axiom-developer.org/TimothyDaly_files/publications/sei/intel/intel.pdf ) When you drill down to the spad implementation of equality you find calls to lisp functions. One of the open research questions is how to ground the recursive reasoning usually based on the Peano math on Lisp primitives.Hopefully there is a "firewall" of proven lisp primitives that can be used to support spad recursive proofs, similar to the Peano mechanism. So, in summary, one research question is what it means to ground computational mathematics. That's one of the key questions to answer when creating the "thin thread" from BasicType to NNI. Tim
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer