I've spent a lot of time talking to professors at CMU about Type Theory and the Curry-Howard correspondence. Therehttps://www.cs.uoregon.edu/research/summerschool/summer16/curriculum.php 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. 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 |
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 |
Free forum by Nabble | Edit this page |