The Curry-Howard Isomorphism has been around since about 1969 https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
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 [1] Burns, Daly: "FXplorer: Exploration of Computed Software Behavior" HICSS 2009 " http://daly.axiom-developer.org/TimothyDaly_files/publications/sei/hicss09.pdf [2] Mili, Daly, Pleszkoch, Prowell HICSS 2006 "A Sematic Recognizer Infrastructure for Computing Loop Behavior" http://daly.axiom-developer.org//TimothyDaly_files/publications/sei/hic.pdf
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
