Proving Axiom Correct, "state of the art" report

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Proving Axiom Correct, "state of the art" report

Tim Daly
I've spent a lot of time talking to professors at CMU about
Type Theory and the Curry-Howard correspondence. There
are excellent lectures online, taught every summer in Oregon.
https://www.cs.uoregon.edu/research/summerschool/summer16/curriculum.php

Type theory has advanced considerably in recent years. It appears
that there is a correspondence between Axiom's world and the formal
theory world.

Axiom has "Categories", which correspond the "Typeclasses".
Axiom had "Domains", which correspond to "Instances".

However, I've adusted the "Typeclasses" and "Instances" ideas
a bit to better match Axiom's construction.

Typeclasses have 3 parts:
   carrier -- the representation data structure
   signatures -- the functions
   propositions -- the logical type requirements

In Axiom we currently only have signatures in Categories.
We put the "carrier" in the Domain as the Rep.

Consider the Axiom Domain NonNegativeInteger. NNI roughly
corresponds to the Type theory "Nat" construction. They differ
in that Axiom uses Lisp Integers whereas Type theory uses
Peano arithmetic (a zero and a successor function) but for
our purposes this does not matter at the moment.

NNI inherits a requirement for an "=" signature from the BasicType
Category. Type theory expects that "=" should satisfy three
propositions,
  reflexive:  x = x
  symmetric: x = y iff y = x
  transitive: x = y and y = z implies x = z

But these propositions are "types", per Curry-Howard. That means
that we can state these "types" in BasicType. They are no
different from the signatures we currently use.

  reflexive: x:% = x:%
  symmetric: x:% = y:% <-> y:% = x:%
  transitive: x:% = y:% /\ y:% = z:% -> x:% = z:%


But that implies that when we create an Axiom Domain we need
to do three things:
1) we need to define the "carrier" (Axiom's Rep) which we already do
2) we need to implement the function signature (we already do)
3) we need to provide proofs for each proposition and since the
    inherited propositions are type signatures that means we need
    to prove each one using operations and elements from the
    Domain we are creating.

We currently do not write Category propositions, nor do we yet have
a proof language for the Domain proofs.

However it appears that some systems (e.g. Lean)
https://github.com/leanprover
can operate in "server mode".

Which means that it might be possible to include the Category level
propositions as comments and the Domain level proofs as comments.
The compiler can pass these comments to the proof server and get
back a verification that the proof is correct. This is a short term
solution which is not "first class".

At present Axiom extracts these during the build and calls the
proof checker (COQ) to show that the proofs are correct. I am
trying to get a "thin thread" all the way through the system in
order to prove propositions about the NNI GCD function.

In the ideal case Axiom implements a trusted kernel in Lisp and
the propositions and proofs are native to the compiler/interpreter.
I'm currently studying the "trusted kernel" source code of various
systems to see what it would take to implement this.

A secondary effort involves coercions and conversions. Type theory
doesn't seem to say a lot about these operations. Fortenbacher
wrote a short paper years ago. Coercions are orthogonal to Types.
We really need a strong theory of coercions, most notably to
formalize their role in the interpreter.

Anyway, that's the current "state of the art" with respect to Axiom.

Tim


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct, "state of the art" report

Martin Baker-3
On 31/03/17 05:34, Tim Daly wrote:
> Consider the Axiom Domain NonNegativeInteger. NNI roughly
> corresponds to the Type theory "Nat" construction. They differ
> in that Axiom uses Lisp Integers whereas Type theory uses
> Peano arithmetic (a zero and a successor function) but for
> our purposes this does not matter at the moment.

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?

Martin

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