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

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

[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer