Re: [Axiom-developer] Proving Axiom Correct

[Tim Daly]

I got the tongue-in-cheek aspect but Axiom's formal logic basis is important.

In the 1980s Expert Systems were going to take over the world. We tried to prove our version

correct using the Boyer-Moore theorem proving technology. We failed miserably, partly

because the technology was not up to the task but mostly because we were not up to the

task. Proving programs correct, at the time, was pretty much based on reasoning about

pre- and -post-conditions. That's the "assembly language" of proof techniques these days.

There was a complete mismatch with the rule-based expert systems technology.

Because Axiom is so close to the math and Coq is so close to Axiom it seems there

is hope that this effort will make a lot more progress.

Coq is astonishingly good at proving things. It has a very small trusted kernel based on

logic. But it has things like a 'tactics' language that enables automation of proof steps

to the point where a proof might be just a single tactic, a 1-line statement. This really
simplifies what is usually a hair-tearing struggle. Lean (a Microsoft/CMU) system is
the basis of a course I'm taking at CMU and it seems even more user-affectionate.

Even better, Coq has dependent types so it is possible to state, for instance, the size

of a matrix. Since types can be user-defined we can create Axiom-specific types in Coq
that mirror the Category structure.Even sweeter is that the syntax is very close to Spad.

For example, Spad

   gcd(x:NNI,y:NNI):NNI ==

      zero? x => y

      gcd(y rem x, x)

and Coq

   Fixpoint gcd x y :=

      match x with

      | O => y

      | S x' => gcd (y mod (S x')) (S 'x)

where S is the Peano Successor function. Coq can prove this directly and

automatically infer that the type signature is

  gcd(x:nat,y:nat):nat

Coq proofs are now integrated into the build. The next commit will likely include complete

automation of the proof, calling Coq during the build process with GCD as the first case.

Once that happens the game seems to be creating the Axiom type tower in Coq.

Axiom's NNI becomes Coq's 'nat' type. This enables writing Axiom types directly

in Coq proofs.

The ideal case would be to modify Axiom's compiler to accept the Coq/ML syntax

but that's a large effort.

Another, more likely effort, would be to implement Coq's trusted kernel in Axiom.

That would permit the compiler and interpreter to prove running code.

It is time to formalize computational mathematics and put computer algebra on

a firm mathematical basis. The technolgy is here (although the funding is not).

On Wed, Jan 25, 2017 at 3:18 AM, Gabriel Dos Reis <address@hidden> wrote:

I was largely poking, tongue in cheek, at the earlier syllogism:

>> The point is that Lisp has a formal logic basis and, as Spad is really

>> just a domain specific language implemented in Lisp then Spad shares

>> the formal logic basis.

-- Gaby

On Thu, Jan 12, 2017 at 10:35 PM, Tim Daly <address@hidden> wrote:

> There were implementations of C in Lisp. So C shares that formal logic basis, or that it was discovered?

According to Wadler, C is an "invented" language, not a "discovered" language.

Wadler (https://www.youtube.com/watch?v=aeRVdYN6fE8)  at around 40 minutes

shows the logician's view versus the computer science view of various theories.

He makes a distinction betwen invented and discovered langauges.

(begin quote of Wadler)

Every interesting logic has a corresponding language feature:

Natural Deduction (Gentzen) <==> Typed Lambda Calculus (Church)
Type Schemes (Hindley) <==> ML Type System (Milner)
System F (Girard) <==> Polymorphic Lambda Calculus (Reynolds)
Modal Logic (Lewis) <==> Monads (state, exceptions) (Kleisli, Moggi)
Classical-Intuitionistic Embedding (Godel) <==> Continuation Passing (Reynolds)
Linear Logic (Girard) <==> Session Types (Honda)

Languages which were "discovered" (based on theory):

Lisp (McCarthy)
Iswim (Landin)
Scheme (Steele and Sussman)
ML (Milner, Gordon, Wadsworth)
Haskell (Hudak, Hughes, Peyton Jones, Wadler)
O'Caml (Leroy)
Erlang (Armstrong, Virding, Williams)
Scala (Odersky)
F# (Syme)
Clojure (Hickey)
Elm (Czaplicki)

At about minute 43 we hear:

"Not all of these languages are based on lambda calculus ...
but there is a core that is "discovered". Now most of you work
in languages like Java, C++, or Python and those languages I will
claim are not discovered; they are "invented". Looking at them
you can tell they are invented. So this is my invitation to you
to work in languages that are "discovered".

Somebody asked before about "dependent types". It turns out that
when you extend into dependent types you now get languages that
have "for all" and "there exists" that corresponds to a feature
called "dependent types". So this means that you can encode very
sophisticated proofs, pretty much everything you can name as a
program. And so the standard way to get a computer to check a
proof for you and to help you with that proof is to represent that
as a program in typed lambda calculus.

All of these systems are based on a greater or lesser extent on
that idea:

Automath (de Bruijn)
Type Theory (Martin Lof)
Mizar (Trybulec)
ML/LCF (Milner, Gordon, Wadsworth)
NuPrl (COnstable)
HOL (Gordon, Melham)
Coq (Huet, Coquand)
Isabelle (Paulson)
Epigram (McBride, McKinna)
Agda (Norell)

(end quote)

Axiom is using Coq for its proof platform because Axiom needs
dependent types (e.g. specifying matrix sizes by parameters).

In addition, Coq is capable of generating a program from a
proof and the plan is to reshape the Spad solution to more
closely mirror the proof-generated code. Also, of course, we need

to remove any errors in the Spad code found during proofs.

It seems there must be an isomorphism between Coq and Spad.

At the moment it seems that Coq's 'nat' matches Axiom's
NonNegativeInteger. Coq also has a 'Group' type which needs
to be matched with the Axiom type. The idea is to find many
isomorphisms of primitive types which will generate lemmas
that can be used to prove more complex code.

Given that Axiom has an abstract algebra scaffold it seems likely

that a reasonable subset can be proven (modulo the fact that there

are arguable differences from the abstract algebra type hierarchy).

Currently Coq is run during the Axiom build to check any proofs
of Spad code that are included. ACL2 is also run during the build
to check any proofs of Lisp code that are included.

I'm taking a course at Carnegie-Mellon this semester using Lean
(a Coq offshoot) in order to try to make some working examples
of proving Spad code correct.

On Thu, Jan 12, 2017 at 10:14 PM, Gabriel Dos Reis <address@hidden> wrote:

There were implementations of C in Lisp. So C shares that formal logic basis, or that it was discovered?

On Wed, Jan 11, 2017 at 8:17 PM, Tim Daly <address@hidden> wrote:

I'm making progress on proving Axiom correct both at the Spad level and

the Lisp level. One interesting talk by Phillip Wadler on "Propositions as

Types", a very entertaining talk, is here:
https://www.youtube.com/watch?v=IOiZatlZtGU

He makes the interesting point late in the talk that some languages are

"discovered" based on fundamental logic principles (e.g.Lisp) and others

are "invented" with no formal basis (e.g. C). As he says, "you can tell

whether your language is discovered or invented".

The point is that Lisp has a formal logic basis and, as Spad is really

just a domain specific language implemented in Lisp then Spad shares

the formal logic basis.

_______________________________________________
Axiom-developer mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/axiom-developer