|
From: | Tim Daly |
Subject: | Re: [Axiom-developer] [Proving Axiom Correct] Bootstrapping a library |
Date: | Wed, 8 Feb 2017 22:54:34 -0500 |
> with the same name and same arguments but different return types, for example).> by the arguments but also by the return type (so there can be multiple functions> Everything in Spad is strongly typed and function definitions are chosen not only> gcd(y rem x, x)> zero? x => y> gcd(x:NNI,y:NNI):NNI ==> and Axiom's definition is> end.> | S a' => gcd (b mod (S a')) (S a')> | 0 => b> match a with> Coq provides gcd as> Fixpoint gcd a b :=
>
> Every statement in the function is strongly type-checked.
On Wed, Feb 8, 2017 at 9:23 PM, Tim Daly <address@hidden> wrote:The semantics of = is given in the Domain (the current one being defined is called % in Spad)Part of your struggle of understanding what I wrote is that I'm not yet fluent in thelogic language and syntax. I'm learning as fast as I can so please be patient.
======================================================
CATEGORY SIGNATURE vs DOMAIN SEMANTICS
> Presumably you will eventually want to add axioms to the structures that say
> things about what eq and neq donot in the Category (well...you can... sigh)
Each domain that inherits '=' from the Category BasicType needs to specify the meaning
of that function for the Domain you're implementing..In our language, we would say that every instance of the structure has all the necessary data. For example, every group (=instance of the group structure, or element of the type group α) has a unit, a binary operation, and inverse operation, etc.For a Polynomial domain with some
structural data representation you have to define what it means for two polynomial objects
to be =. such as a function to compare coefficients. Part of the game would be to provethat the coefficient-compare function is correct, always returns a Boolean, and terminates.
All a Category like BasicType does is specify that the Domain Polynomial should
implement an = operation with the given signature. That is, you have to implement
poly = poly
which returns a boolean. (Note that there are other = functions in Polynomial such as onethat returns an equation object but that signature is inherited from a different Category).Is there anything that requires that the operation you implement is reflexive, symmetric, and transitive? Putting axioms on the structure specifies that that has to be the case. Without such axioms, you cannot prove anything about implementations in general. You can only prove things about individual implementations.with the same name and same arguments but different return types, for example).by the arguments but also by the return type (so there can be multiple functionsEverything in Spad is strongly typed and function definitions are chosen not onlygcd(y rem x, x)zero? x => ygcd(x:NNI,y:NNI):NNI ==and Axiom's definition isend.| S a' => gcd (b mod (S a')) (S a')| 0 => bmatch a withFixpoint gcd a b :=Coq provides gcd asa function that fulfills the signature ofIt looks like your 'class' syntax implements what I need. I will try this for the otherCategories used in NNI.
======================================================= PROVING TERMINATIONAs I understood from class, for an algorithm like gcd it should be sufficient to construct
gcd(a:NNI,b:NNI):NNI
Every statement in the function is strongly type-checked.That is what I referred to as a shallow embedding -- you are associating to every axiom definition a Coq or Lean definition which has the same behavior.If you do that, you cannot model arbitrary while loops. You have to write functions in Coq or Lean in a way that, from the start, they are guaranteed to terminate. You can do this, for example, by showing the recursive calls are decreasing along a suitable measure, or giving a priori bounds on a while loop. If you want to translate spad functions automatically, you'll have to write the former in such a way that the translations have this property. You can't translate an arbitrary, a priori partial, function and then show after the fact that it terminates for every input.Other approaches are possible. You can, for example, translate spad functions to relations in Coq or Lean, and then prove that the relations give rise to total functions.Best wishes,JeremyThus we are guaranteed that the Spad version of gcd above (in the Domain NNI)can only be called with NNI arguments and is guaranteed to only return NNI results.
The languages are very close in spirit if not in syntax.What Axiom does not do, for example, is prove termination.
Coq, in its version, will figure out that the recursion is on 'a' and that it will terminate.
Part of the game is to provide the same termination analysis on Spad code.
==================================================== ADDITIONAL CONSTRAINTSIt would be ideal to reject code that did not fulfill all of the requirementssuch as specifying at the Category level definition of gcd that it not onlyhas to have the correct signature, it also has to return the 'positive'divisor. For NNI this is trivially fulfilled.The Category definition should say something likegcd(%,%) -> % and gcd >= 1$%where 1$% says to use the unit from the implementing Domain.
So for some domains we have:gcd(x,y) ==x := unitCanonical xy := unitCanonical ywhile not zero? y repeat(x,y) := (y, x rem y)y := unitCanonical yxusing unitCanonical to deal with things like signs. (This also adds the complication
of loops which I mentioned in a previous email.)Not only the signature but the side-conditions would have to be checked.
==================================================== ALTERNATE APPROACHESInstead of a new library organization it might be possible to have a generator functionin Coq that translates Coq code to Spad code. Or a translator from Spad code toCoq code.
Unfortunately Coq and Lean do not seem to use function name overloadingor inheritance (or do they?) which confuses the problem of name translation.Axiom has 42 functions named 'gcd', each living in a different Domain.There is no such thing as a simple job. But this one promises to be interesting.In any case I'll push the implementation forward. Thanks for your help.Tim
On Wed, Feb 8, 2017 at 5:52 PM, Jeremy Avigad <address@hidden> wrote:Dear Tim,I don't understand what you mean. For one thing, theorems in both Lean and Coq are marked as opaque, since you generally don't care about the contents. But even if we replace "theorem" by "definition," I don't know what you imagine going into the "...".I think what you want to do is represent Axiom categories as structures. For example, the declarations below declare a BasicType structure and notation for elements of that structure. You can then prove theorems about arbitrary types α that have a BasicType structure. You can also extend the structure as needed.(Presumably you will eventually want to add axioms to the structures that say things about what eq and neq do. Otherwise, you are just reasoning about a type with two relations.)Best wishes,Jeremyclass BasicType (α : Type) : Type :=(eq : α → α → bool) (neq : α → α → bool)infix `?=?`:50 := BasicType.eqinfix `?~=?`:50 := BasicType.neqsectionvariables (α : Type) [BasicType α]variables a b : αcheck a ?=? bcheck a ?~=? bendOn Wed, Feb 8, 2017 at 9:29 AM, Tim Daly <address@hidden> wrote:Timtheorems by changing external references from = to spad= everywhere.Eventually there should be enough embedded logic to start coding AxiomInitially this would make Axiom depend on the external library structure.the name of Axiom's algebra language).Thus, instead of =, the supporting theorem would be 'spad=' (spad isJeremy Avigad (Lean) made the suggestion to rename these theorems.FoCaL but I suspect it has the same bootstrap problem.that only contains a limited number of theorems. I'm not yet sure aboutremoving the existing libraries and replacing them with a new versionfor the logic system. So BasicType would containdefinitions of = and ~= so we could create a new library structureIn the ideal case we would decorate BasicType with the existing?=?: (%,%) -> Boolean ?~=?: (%,%) -> Booleanis BasicType which contains two signatures:but extract those theorems automatically from Axiom sourcesThe game is to prove GCD in NonNegativeInteger (NNI).We would like to use the 'nat' theorems from the existing libraryat build time.Axiom's NNI inherits from a dozen Category objects, one of whichtheorem = (a, b : Type) : Boolean := .....theorem ~= (a, b : Type) : Boolean := ....These theorems would be imported into NNI when it inherits thesignatures from the BasicType Category. The collection of all ofthe theorems in NNI's Category structure would be used (hopefullyexclusively) to prove GCD. In this way, all of the theorems used toprove Axiom source code would be inheritied from the Categorystructure.Unfortunately it appears the Coq and Lean will not take kindly toAxiom proofs would still depend on the external proof system but onlyfor the correctness engine, not the library structure. This will minimizethe struggle about Axiom's world view (e.g. handling excluded middle).It will also organize the logic library to more closely mirror abstract algebra.Comments, suggestions?
[Prev in Thread] | Current Thread | [Next in Thread] |