[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]