I first heard of it in 2003 working with Gilbert Baumslag at CCNY.

It seemed "interesting" but I didn't understand how important it is.

The field of proof theory has grown beyond belief in the past decade

and the systems are much more powerful than the Nthqm system I

used at IBM. It seems that these systems are now capable of providing

a solid basis for implementing proofs in/of Axiom.

The essential idea (for Axiom) is that a proof is a first-class object with

a well-defined type. The "type of a proof" is the statement of the theorem.

In Axiom, that would be contained in the Category.

The "implementation of the type" is the proof itself. In Axiom. that would

be contained in the Domain, just like one would implement any other operation.

So, in Axiom terms, it is possible to give signatures in Axiom Categories,

such as "Commutative":

Commutative : Category ==

TH ==> Theorem

PR ==> Proof

commutative : TH -> PR

== add

Inheriting Commutative is no longer an empty promise. It requires a domain

to provide an implementation (aka a proof) of commutativity.

Similar towers of Theorem/Proof requirements can be built up using the

existing Category structure. For example, Group could inherit a tower of

theorems that need to be proven by a Domain that is a Group.

For example (using Lean syntax

http://leanprover.github.io/ ):

class semigroup (α : Type u) extends has_mul α := |

(mul_assoc : ∀ a b c : α, a * b * c = a * (b * c)) |

class comm_semigroup (α : Type u) extends semigroup α := |

(mul_comm : ∀ a b : α, a * b = b * a) |

class left_cancel_semigroup (α : Type u) extends semigroup α := |

(mul_left_cancel : ∀ a b c : α, a * b = a * c → b = c) |

class right_cancel_semigroup (α : Type u) extends semigroup α := |

(mul_right_cancel : ∀ a b c : α, a * b = c * b → a = c) |

class monoid (α : Type u) extends semigroup α, has_one α := |

(one_mul : ∀ a : α, 1 * a = a) (mul_one : ∀ a : α, a * 1 = a) |

class comm_monoid (α : Type u) extends monoid α, comm_semigroup α |

class group (α : Type u) extends monoid α, has_inv α := |

(mul_left_inv :

∀ a : α, a

⁻¹ * a

= 1)

Each of these theorems needs to be proven by a Domain which claims to

be a Group. The theorems themselves are essentially 'types' and the

proofs are essentially 'programs'. So, in Axiom-speak, a Domain which is

a Group has to "provide an implementation for the theorem signatures" by

creating a proof for each inherited signature, similar to the requirements

for other signatures, using operations from the Domain.

This use of "existing empty Categories" (like Commutative) seems to be

a reasonable place to insert theorem/proofs into Axiom's type tower.

At the moment, these are simply unproven declarations.

There are design questions of how to handle the 'forall', 'implies', and other

syntax/semantics. Axiom's compiler needs extensions. Systems like Lean,

mentioned above, provide a server API which might be used to provide the

actual proof service to the Axiom compiler.

There are further questions which this does not address. For example, the

proof systems like to use Peano posulates for "natural numbers" whereas

Axiom uses Lisp integers for "NonNegativeIntegers". So there needs to be

some path to provide "ground truth" to proofs, all the way down to the hardware.

The current path is a "tower of provers" extending from Spad to the hardware:

Spad <-> COQ

Lisp <-> ACL2

C <-> Intel (using C0 from Pfenning at CMU?; GCL compiles to C)

Intel <-> (my prior Intel instruction semantics work on Conditional-Concurrent

Assignments [1][2])

In the "upward" direction there needs to be some connection between the

theorems/proofs in a paper (e.g. integration, groebner, etc) and the Axiom

Spad implementations. I'm collecting references and decorating the algorithms

where I can find a connection. But that is only some groundwork. I have no

insight into this question yet. In the future there ought to be a stronger formal

connection between the published theory and its implementation in Axiom.

Comments? Suggestions?

Tim

[2] Mili, Daly, Pleszkoch, Prowell HICSS 2006

"A Sematic Recognizer Infrastructure for Computing Loop Behavior"

_______________________________________________

Axiom-developer mailing list

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