axiom-developer
[Top][All Lists]

## Re: [Axiom-developer] Proving Axiom Correct

 From: Tim Daly Subject: Re: [Axiom-developer] Proving Axiom Correct Date: Fri, 31 Mar 2017 12:34:16 -0400

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

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