# [Proving Axiom Correct] Bootstrapping a library

 Classic List Threaded
11 messages
Reply | Threaded
Open this post in threaded view
|

## [Proving Axiom Correct] Bootstrapping a library

 The game is to prove GCD in NonNegativeInteger (NNI).We would like to use the 'nat' theorems from the existing librarybut extract those theorems automatically from Axiom sourcesat build time. Axiom's NNI inherits from a dozen Category objects, one of whichis BasicType which contains two signatures: ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> BooleanIn the ideal case we would decorate BasicType with the existingdefinitions of = and ~= so we could create a new library structurefor the logic system. So BasicType would containtheorem = (a, b : Type) : Boolean := .....theorem ~= (a, b : Type) : Boolean := ....These theorems would be imported into NNI when it inherits the signatures 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 toremoving the existing libraries and replacing them with a new versionthat only contains a limited number of theorems. I'm not yet sure aboutFoCaL but I suspect it has the same bootstrap problem.Jeremy Avigad (Lean) made the suggestion to rename these theorems.Thus, instead of =, the supporting theorem would be 'spad=' (spad isthe name of Axiom's algebra language).Initially this would make Axiom depend on the external library structure.Eventually there should be enough embedded logic to start coding Axiomtheorems by changing external references from = to spad= everywhere.Axiom 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?Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 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.neqsection  variables (α : Type) [BasicType α]  variables a b : α   check a ?=? b  check a ?~=? bendOn Wed, Feb 8, 2017 at 9:29 AM, Tim Daly wrote:The game is to prove GCD in NonNegativeInteger (NNI).We would like to use the 'nat' theorems from the existing librarybut extract those theorems automatically from Axiom sourcesat build time. Axiom's NNI inherits from a dozen Category objects, one of whichis BasicType which contains two signatures: ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> BooleanIn the ideal case we would decorate BasicType with the existingdefinitions of = and ~= so we could create a new library structurefor the logic system. So BasicType would containtheorem = (a, b : Type) : Boolean := .....theorem ~= (a, b : Type) : Boolean := ....These theorems would be imported into NNI when it inherits the signatures 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 toremoving the existing libraries and replacing them with a new versionthat only contains a limited number of theorems. I'm not yet sure aboutFoCaL but I suspect it has the same bootstrap problem.Jeremy Avigad (Lean) made the suggestion to rename these theorems.Thus, instead of =, the supporting theorem would be 'spad=' (spad isthe name of Axiom's algebra language).Initially this would make Axiom depend on the external library structure.Eventually there should be enough embedded logic to start coding Axiomtheorems by changing external references from = to spad= everywhere.Axiom 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?Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 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 doThe semantics of = is given in the Domain (the current one being defined is called % in Spad)not in the Category (well...you can... sigh)Each domain that inherits '=' from the Category BasicType needs to specify the meaningof that function for the Domain you're implementing.. 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).It 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 constructa function that fulfills the signature of   gcd(a:NNI,b:NNI):NNICoq provides gcd as  Fixpoint gcd a b :=    match a with      | 0 => b      | S a' => gcd (b mod (S a')) (S a')    end.and Axiom's definition is  gcd(x:NNI,y:NNI):NNI ==    zero? x => y    gcd(y rem x, x)Everything in Spad is strongly typed and function definitions are chosen not onlyby the arguments but also by the return type (so there can be multiple functionswith the same name and same arguments but different return types, for example). Every statement in the function is strongly type-checked.Thus 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 like   gcd(%,%) -> %  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 x    y := unitCanonical y    while not zero? y repeat      (x,y) := (y, x rem y)      y := unitCanonical y    xusing 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.TimOn Wed, Feb 8, 2017 at 5:52 PM, Jeremy Avigad 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.neqsection  variables (α : Type) [BasicType α]  variables a b : α   check a ?=? b  check a ?~=? bendOn Wed, Feb 8, 2017 at 9:29 AM, Tim Daly wrote:The game is to prove GCD in NonNegativeInteger (NNI).We would like to use the 'nat' theorems from the existing librarybut extract those theorems automatically from Axiom sourcesat build time. Axiom's NNI inherits from a dozen Category objects, one of whichis BasicType which contains two signatures: ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> BooleanIn the ideal case we would decorate BasicType with the existingdefinitions of = and ~= so we could create a new library structurefor the logic system. So BasicType would containtheorem = (a, b : Type) : Boolean := .....theorem ~= (a, b : Type) : Boolean := ....These theorems would be imported into NNI when it inherits the signatures 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 toremoving the existing libraries and replacing them with a new versionthat only contains a limited number of theorems. I'm not yet sure aboutFoCaL but I suspect it has the same bootstrap problem.Jeremy Avigad (Lean) made the suggestion to rename these theorems.Thus, instead of =, the supporting theorem would be 'spad=' (spad isthe name of Axiom's algebra language).Initially this would make Axiom depend on the external library structure.Eventually there should be enough embedded logic to start coding Axiomtheorems by changing external references from = to spad= everywhere.Axiom 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?Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 In reply to this post by Tim Daly Am 08.02.2017 um 15:29 schrieb Tim Daly: > The game is to prove GCD in NonNegativeInteger (NNI). We encounter numerous problems when trying to prove gcd from EuclideanDomain: --- gcd(x, y) ==   --Euclidean Algorithm   x := unitCanonical x   y := unitCanonical y   while not zero? y repeat     (x, y) := (y, x rem y)     y := unitCanonical y     -- this doesn't affect the                              -- correctness of Euclid's algorithm,                              -- but                              -- a) may improve performance                              -- b) ensures gcd(x, y)=gcd(y, x)                              --    if canonicalUnitNormal   x --- 1. Define type EuclideanDomain (tower of hierarchies) 2. Define unitCanonical (depends on canonicalUnitNormal etc.) 3. Imperative elements in spad 4. Trust interpreter/compiler and lisp While (1,2) seems not so difficult, (3) might be delicate and (4) seems to be out of scope for the moment (that is let's trust it, as an axiom so to speak ). Basically, I see two methods: a) Implement spad language, e.g. like the "Imp" example: https://www.seas.upenn.edu/~cis500/current/sf/Imp.htmland prove the statements. b) Prove the math (by reusing existing [abundant] math libraries) and extract the functions (Definitions in Coq) as spad code. This would actually mean to replace parts of current code by new one (purely functional). Clearly, both methods will require a definition of spad's key functions/operators. I believe that (a) is more laborious than (b). Moreover, Coq's notation mechanism (Notation) has it's limits (e.g. conflicts with built-in keywords)(**). Moreover, method (b) is admittedly not what we really want: namely proving existing Axiom code correct. (**) a parser might be a better solution https://www.seas.upenn.edu/~cis500/current/sf/ImpParser.html> > We would like to use the 'nat' theorems from the existing library > but extract those theorems automatically from Axiom sources > at build time. > > Axiom's NNI inherits from a dozen Category objects, one of which > is BasicType which contains two signatures: > >  ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> Boolean > > In the ideal case we would decorate BasicType with the existing > definitions of = and ~= so we could create a new library structure > for the logic system. So BasicType would contain > > theorem = (a, b : Type) : Boolean := ..... > theorem ~= (a, b : Type) : Boolean := .... > > These theorems would be imported into NNI when it inherits the > signatures from the BasicType Category. The collection of all of > the theorems in NNI's Category structure would be used (hopefully > exclusively) to prove GCD. In this way, all of the theorems used to > prove Axiom source code would be inheritied from the Category > structure. Parameter BasicType:Type. Parameter eq: BasicType -> BasicType -> bool. Parameter neq: BasicType -> BasicType -> bool. Infix "=" := eq. Parameter x y z:BasicType. Check (x=y). There are several better choices of course: Module Type or type classes, whereas I'm not very used to the latter. > > Unfortunately it appears the Coq and Lean will not take kindly to > removing the existing libraries and replacing them with a new version > that only contains a limited number of theorems. I'm not yet sure about > FoCaL but I suspect it has the same bootstrap problem. I think you can overwrite anything and even do a \$ coqtop -noinit so that even "nat" is unknown. Coq < Check nat. Toplevel input, characters 6-9: > Check nat. >       ^^^ Error: The reference nat was not found in the current environment. > > Jeremy Avigad (Lean) made the suggestion to rename these theorems. > Thus, instead of =, the supporting theorem would be 'spad=' (spad is > the name of Axiom's algebra language). > > Initially this would make Axiom depend on the external library structure. > Eventually there should be enough embedded logic to start coding Axiom > theorems by changing external references from = to spad= everywhere. > > Axiom proofs would still depend on the external proof system but only > for the correctness engine, not the library structure. This will minimize > the struggle about Axiom's world view (e.g. handling excluded middle). > It will also organize the logic library to more closely mirror abstract algebra. Indeed, this is an important point when dealing with dependent types. Type classes (http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf) presumably could serve best to map the spad categories while reasoning in CoC (whilst "exlcuded middle" may be introduced as needed). > > Comments, suggestions? I believe that some more research will be necessary to find the most suitable approach before building a prototype. I should dig into the "type classes" subject before making any suggestions. BTW I have recently written "field_mpl.v" (attached) for a talk about MPL where you can see how tedious it can be to prove simple facts from scratch, whereas the last prop (P1) goes with ease owing to solid preparations (it's educational only of course). > > Tim > > > > > _______________________________________________ > Axiom-developer mailing list > [hidden email] > https://lists.nongnu.org/mailman/listinfo/axiom-developer> _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer field_mpl.v (7K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 In reply to this post by Tim Daly On Wed, Feb 8, 2017 at 9:23 PM, Tim Daly wrote: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 doThe semantics of = is given in the Domain (the current one being defined is called % in Spad)not in the Category (well...you can... sigh)Each domain that inherits '=' from the Category BasicType needs to specify the meaningof 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.It 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 constructa function that fulfills the signature of   gcd(a:NNI,b:NNI):NNICoq provides gcd as  Fixpoint gcd a b :=    match a with      | 0 => b      | S a' => gcd (b mod (S a')) (S a')    end.and Axiom's definition is  gcd(x:NNI,y:NNI):NNI ==    zero? x => y    gcd(y rem x, x)Everything in Spad is strongly typed and function definitions are chosen not onlyby the arguments but also by the return type (so there can be multiple functionswith the same name and same arguments but different return types, for example). 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,Jeremy Thus 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 like   gcd(%,%) -> %  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 x    y := unitCanonical y    while not zero? y repeat      (x,y) := (y, x rem y)      y := unitCanonical y    xusing 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.TimOn Wed, Feb 8, 2017 at 5:52 PM, Jeremy Avigad 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.neqsection  variables (α : Type) [BasicType α]  variables a b : α   check a ?=? b  check a ?~=? bendOn Wed, Feb 8, 2017 at 9:29 AM, Tim Daly wrote:The game is to prove GCD in NonNegativeInteger (NNI).We would like to use the 'nat' theorems from the existing librarybut extract those theorems automatically from Axiom sourcesat build time. Axiom's NNI inherits from a dozen Category objects, one of whichis BasicType which contains two signatures: ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> BooleanIn the ideal case we would decorate BasicType with the existingdefinitions of = and ~= so we could create a new library structurefor the logic system. So BasicType would containtheorem = (a, b : Type) : Boolean := .....theorem ~= (a, b : Type) : Boolean := ....These theorems would be imported into NNI when it inherits the signatures 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 toremoving the existing libraries and replacing them with a new versionthat only contains a limited number of theorems. I'm not yet sure aboutFoCaL but I suspect it has the same bootstrap problem.Jeremy Avigad (Lean) made the suggestion to rename these theorems.Thus, instead of =, the supporting theorem would be 'spad=' (spad isthe name of Axiom's algebra language).Initially this would make Axiom depend on the external library structure.Eventually there should be enough embedded logic to start coding Axiomtheorems by changing external references from = to spad= everywhere.Axiom 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?Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 >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.Yes. Such properties are required by the Category hierarchy. There is,for example, Group and AbelianGroup and there are Categoriesconstraints on properties like reflexive, etc. which can affect thesignatures that get inherited.On Wed, Feb 8, 2017 at 9:44 PM, Jeremy Avigad wrote:On Wed, Feb 8, 2017 at 9:23 PM, Tim Daly wrote: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 doThe semantics of = is given in the Domain (the current one being defined is called % in Spad)not in the Category (well...you can... sigh)Each domain that inherits '=' from the Category BasicType needs to specify the meaningof 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.It 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 constructa function that fulfills the signature of   gcd(a:NNI,b:NNI):NNICoq provides gcd as  Fixpoint gcd a b :=    match a with      | 0 => b      | S a' => gcd (b mod (S a')) (S a')    end.and Axiom's definition is  gcd(x:NNI,y:NNI):NNI ==    zero? x => y    gcd(y rem x, x)Everything in Spad is strongly typed and function definitions are chosen not onlyby the arguments but also by the return type (so there can be multiple functionswith the same name and same arguments but different return types, for example). 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,Jeremy Thus 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 like   gcd(%,%) -> %  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 x    y := unitCanonical y    while not zero? y repeat      (x,y) := (y, x rem y)      y := unitCanonical y    xusing 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.TimOn Wed, Feb 8, 2017 at 5:52 PM, Jeremy Avigad 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.neqsection  variables (α : Type) [BasicType α]  variables a b : α   check a ?=? b  check a ?~=? bendOn Wed, Feb 8, 2017 at 9:29 AM, Tim Daly wrote:The game is to prove GCD in NonNegativeInteger (NNI).We would like to use the 'nat' theorems from the existing librarybut extract those theorems automatically from Axiom sourcesat build time. Axiom's NNI inherits from a dozen Category objects, one of whichis BasicType which contains two signatures: ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> BooleanIn the ideal case we would decorate BasicType with the existingdefinitions of = and ~= so we could create a new library structurefor the logic system. So BasicType would containtheorem = (a, b : Type) : Boolean := .....theorem ~= (a, b : Type) : Boolean := ....These theorems would be imported into NNI when it inherits the signatures 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 toremoving the existing libraries and replacing them with a new versionthat only contains a limited number of theorems. I'm not yet sure aboutFoCaL but I suspect it has the same bootstrap problem.Jeremy Avigad (Lean) made the suggestion to rename these theorems.Thus, instead of =, the supporting theorem would be 'spad=' (spad isthe name of Axiom's algebra language).Initially this would make Axiom depend on the external library structure.Eventually there should be enough embedded logic to start coding Axiomtheorems by changing external references from = to spad= everywhere.Axiom 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?Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 In reply to this post by Jeremy Avigad > Coq provides gcd as> >  Fixpoint gcd a b :=>    match a with>      | 0 => b>      | S a' => gcd (b mod (S a')) (S a')>    end.> and Axiom's definition is>  gcd(x:NNI,y:NNI):NNI ==>    zero? x => y>    gcd(y rem x, x)> Everything in Spad is strongly typed and function definitions are chosen not only> by the arguments but also by the return type (so there can be multiple functions> with the same name and same arguments but different return types, for example). > 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.This is not intended to be a shallow embedding. In order to prove Spad's gcdwe have to prove zero? and rem and have those available. The idea is to initially create the definitions so that Spad code is reducible to code that theproof engine can process directly. This involves defining the Spad 'words' like'zero?' so they properly type check.What can't be directly proven will have to be restructured/rewritten.As we discussed on Tuesday, a lot of Spad code uses loops. I'm looking atthe Isabelle/HOL book you recommended for some advice on Hoare triples.That's queued behind getting up to speed on FoCaL, as mentioned by Renaud.Eventually I'd like to see the proof engine embedded directly into Axiomrather than called at compile time so that it is also available in the interpreter.Where are grad students when you need them? :-)TimOn Wed, Feb 8, 2017 at 9:44 PM, Jeremy Avigad wrote:On Wed, Feb 8, 2017 at 9:23 PM, Tim Daly wrote: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 doThe semantics of = is given in the Domain (the current one being defined is called % in Spad)not in the Category (well...you can... sigh)Each domain that inherits '=' from the Category BasicType needs to specify the meaningof 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.It 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 constructa function that fulfills the signature of   gcd(a:NNI,b:NNI):NNICoq provides gcd as  Fixpoint gcd a b :=    match a with      | 0 => b      | S a' => gcd (b mod (S a')) (S a')    end.and Axiom's definition is  gcd(x:NNI,y:NNI):NNI ==    zero? x => y    gcd(y rem x, x)Everything in Spad is strongly typed and function definitions are chosen not onlyby the arguments but also by the return type (so there can be multiple functionswith the same name and same arguments but different return types, for example). 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,Jeremy Thus 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 like   gcd(%,%) -> %  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 x    y := unitCanonical y    while not zero? y repeat      (x,y) := (y, x rem y)      y := unitCanonical y    xusing 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.TimOn Wed, Feb 8, 2017 at 5:52 PM, Jeremy Avigad 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.neqsection  variables (α : Type) [BasicType α]  variables a b : α   check a ?=? b  check a ?~=? bendOn Wed, Feb 8, 2017 at 9:29 AM, Tim Daly wrote:The game is to prove GCD in NonNegativeInteger (NNI).We would like to use the 'nat' theorems from the existing librarybut extract those theorems automatically from Axiom sourcesat build time. Axiom's NNI inherits from a dozen Category objects, one of whichis BasicType which contains two signatures: ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> BooleanIn the ideal case we would decorate BasicType with the existingdefinitions of = and ~= so we could create a new library structurefor the logic system. So BasicType would containtheorem = (a, b : Type) : Boolean := .....theorem ~= (a, b : Type) : Boolean := ....These theorems would be imported into NNI when it inherits the signatures 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 toremoving the existing libraries and replacing them with a new versionthat only contains a limited number of theorems. I'm not yet sure aboutFoCaL but I suspect it has the same bootstrap problem.Jeremy Avigad (Lean) made the suggestion to rename these theorems.Thus, instead of =, the supporting theorem would be 'spad=' (spad isthe name of Axiom's algebra language).Initially this would make Axiom depend on the external library structure.Eventually there should be enough embedded logic to start coding Axiomtheorems by changing external references from = to spad= everywhere.Axiom 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?Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 Termination is clearly an issue for provers like Coq. There are solutions to define function partially but they have some cost in term of proof effo.  Maybe we could benefit how the people of Focal deals with loops. -- Laurent On 02/09/2017 04:54 AM, Tim Daly wrote: >     > Coq provides gcd as >     > >     >  Fixpoint gcd a b := >     >    match a with >     >      | 0 => b >     >      | S a' => gcd (b mod (S a')) (S a') >     >    end. > >     > and Axiom's definition is > >     >  gcd(x:NNI,y:NNI):NNI == >     >    zero? x => y >     >    gcd(y rem x, x) > >     > Everything in Spad is strongly typed and function definitions are chosen not only >     > by the arguments but also by the return type (so there can be multiple functions >     > with the same name and same arguments but different return types, for example). >     > 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. > > This is not intended to be a shallow embedding. In order to prove Spad's gcd > we have to prove zero? and rem and have those available. The idea is to > initially create the definitions so that Spad code is reducible to code > that the > proof engine can process directly. This involves defining the Spad > 'words' like > 'zero?' so they properly type check. > > What can't be directly proven will have to be restructured/rewritten. > > As we discussed on Tuesday, a lot of Spad code uses loops. I'm looking at > the Isabelle/HOL book you recommended for some advice on Hoare triples. > > That's queued behind getting up to speed on FoCaL, as mentioned by Renaud. > > Eventually I'd like to see the proof engine embedded directly into Axiom > rather than called at compile time so that it is also available in the > interpreter. > > Where are grad students when you need them? :-) > > Tim > > > On Wed, Feb 8, 2017 at 9:44 PM, Jeremy Avigad <[hidden email] > > wrote: > > > >     On Wed, Feb 8, 2017 at 9:23 PM, Tim Daly <[hidden email] >     > wrote: > >         Part of your struggle of understanding what I wrote is that I'm >         not yet fluent in the >         logic 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 do > >         The semantics of = is given in the Domain (the current one being >         defined is called % in Spad) >         not 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 prove >         that 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 one >         that 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. > > >         It looks like your 'class' syntax implements what I need. I will >         try this for the other >         Categories used in NNI. > > > > >         ======================================================= >         PROVING TERMINATION > >         As I understood from class, for an algorithm like gcd it should >         be sufficient to construct >         a function that fulfills the signature of > >            gcd(a:NNI,b:NNI):NNI > >         Coq provides gcd as > >           Fixpoint gcd a b := >             match a with >               | 0 => b >               | S a' => gcd (b mod (S a')) (S a') >             end. > >         and Axiom's definition is > >           gcd(x:NNI,y:NNI):NNI == >             zero? x => y >             gcd(y rem x, x) > >         Everything in Spad is strongly typed and function definitions >         are chosen not only >         by the arguments but also by the return type (so there can be >         multiple functions >         with the same name and same arguments but different return >         types, for example). >         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, > >     Jeremy > > > > >         Thus 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 CONSTRAINTS > >         It would be ideal to reject code that did not fulfill all of the >         requirements >         such as specifying at the Category level definition of gcd that >         it not only >         has 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 like > >            gcd(%,%) -> %  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 x >             y := unitCanonical y >             while not zero? y repeat >               (x,y) := (y, x rem y) >               y := unitCanonical y >             x > >         using 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 APPROACHES > >         Instead of a new library organization it might be possible to >         have a generator function >         in Coq that translates Coq code to Spad code. Or a translator >         from Spad code to >         Coq code. > >         Unfortunately Coq and Lean do not seem to use function name >         overloading >         or 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 <[hidden email] >         > 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, > >             Jeremy > >             class BasicType (α : Type) : Type := >             (eq : α → α → bool) (neq : α → α → bool) > >             infix `?=?`:50  := BasicType.eq >             infix `?~=?`:50 := BasicType.neq > >             section >               variables (α : Type) [BasicType α] >               variables a b : α > >               check a ?=? b >               check a ?~=? b >             end > > > > >             On Wed, Feb 8, 2017 at 9:29 AM, Tim Daly <[hidden email] >             > wrote: > >                 The game is to prove GCD in NonNegativeInteger (NNI). > >                 We would like to use the 'nat' theorems from the >                 existing library >                 but extract those theorems automatically from Axiom sources >                 at build time. > >                 Axiom's NNI inherits from a dozen Category objects, one >                 of which >                 is BasicType which contains two signatures: > >                  ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> Boolean > >                 In the ideal case we would decorate BasicType with the >                 existing >                 definitions of = and ~= so we could create a new library >                 structure >                 for the logic system. So BasicType would contain > >                 theorem = (a, b : Type) : Boolean := ..... >                 theorem ~= (a, b : Type) : Boolean := .... > >                 These theorems would be imported into NNI when it >                 inherits the >                 signatures from the BasicType Category. The collection >                 of all of >                 the theorems in NNI's Category structure would be used >                 (hopefully >                 exclusively) to prove GCD. In this way, all of the >                 theorems used to >                 prove Axiom source code would be inheritied from the >                 Category >                 structure. > >                 Unfortunately it appears the Coq and Lean will not take >                 kindly to >                 removing the existing libraries and replacing them with >                 a new version >                 that only contains a limited number of theorems. I'm not >                 yet sure about >                 FoCaL but I suspect it has the same bootstrap problem. > >                 Jeremy Avigad (Lean) made the suggestion to rename these >                 theorems. >                 Thus, instead of =, the supporting theorem would be >                 'spad=' (spad is >                 the name of Axiom's algebra language). > >                 Initially this would make Axiom depend on the external >                 library structure. >                 Eventually there should be enough embedded logic to >                 start coding Axiom >                 theorems by changing external references from = to spad= >                 everywhere. > >                 Axiom proofs would still depend on the external proof >                 system but only >                 for the correctness engine, not the library structure. >                 This will minimize >                 the 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? > >                 Tim > > > > > > _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 In reply to this post by Tim Daly Dear Axiom gurus, > Axiom's NNI inherits from a dozen Category objects, one of which > is BasicType which contains two signatures: > >  ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> Boolean > > In the ideal case we would decorate BasicType with the existing > definitions of = and ~= so we could create a new library structure > for the logic system. So BasicType would contain > > theorem = (a, b : Type) : Boolean := ..... > theorem ~= (a, b : Type) : Boolean := .... Since BasicType is not an implementation you need to write a specification for equal and different. These specifictions should be inherited and proved at the domain level. You can see the standard library of FoCaLiZe for details. In practice you need a language for writing logical statements and a language to prove these statements. Again see the FoCaLiZe library (for instance lattices) to see how a statement can be used in a proof. > Unfortunately it appears the Coq and Lean will not take kindly to > removing the existing libraries and replacing them with a new version > that only contains a limited number of theorems. I'm not yet sure about > FoCaL but I suspect it has the same bootstrap problem. Inheritance is managed by the FoCaLiZe compiler together with dependencies which enables to have statements and proofs in a coherent way. -- Renaud Rioboo _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 Renaud,I'm just getting around to the FoCal information. Obviously you've done a lot ofwork on this subject already. I have the papers and the reference manual nearthe top of the reading stack. I'm certain to have questions.Yes, BasicType requires properties for = such as symmetry which would haveto be proven at the Domain level for each implementation. Of course, = is notactually implemented directly in NNI but somewhere up the inheritance chain.For example, the domain ANY has  x = y ==    (x.dm = y.dm) and EQUAL(x.ob, y.ob)\$Lispwhere dm is a field in the Record implementation of ANY   Rep := Record(dm: SExpression, ob: None)which depends on the Lisp definition of EQUAL and SExpressionis one of String, Symbol, Integer, DoubleFloat, OutputFormWhereas the domain IndexedList implements  x = y ==    Qeq(x,y) => true    while not Qnull x and not Qnull y repeat      Qfirst x ^=\$S Qfirst y => return fase      x := Qrest x      y := Qrest y    Qnull x and Qnull ywhere   Qeq   ==> EQ\$Lisp  Qnull ==> NULL\$Lisp  Qfirst ==> QCAR\$Lisp  Qrest ==> QCDR\$Lispand   S : Type is a dependent argument type. Sigh.The proofs of = in each domain will involve an appeal to the Lispdefinition of a small number of functions. I'm using ACL2 for Lisp.This is where the ACL2 and Coq proofs meet.There is no such thing as a simple job.TimOn Fri, Feb 10, 2017 at 5:13 AM, Renaud Rioboo wrote:Dear Axiom gurus, Axiom's NNI inherits from a dozen Category objects, one of which is BasicType which contains two signatures:  ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> Boolean In the ideal case we would decorate BasicType with the existing definitions of = and ~= so we could create a new library structure for the logic system. So BasicType would contain theorem = (a, b : Type) : Boolean := ..... theorem ~= (a, b : Type) : Boolean := .... Since BasicType is not an implementation you need to write a specification for equal and different. These specifictions should be inherited and proved at the domain level. You can see the standard library of FoCaLiZe for details. In practice you need a language for writing logical statements and a language to prove these statements. Again see the FoCaLiZe library (for instance lattices) to see how a statement can be used in a proof. Unfortunately it appears the Coq and Lean will not take kindly to removing the existing libraries and replacing them with a new version that only contains a limited number of theorems. I'm not yet sure about FoCaL but I suspect it has the same bootstrap problem. Inheritance is managed by the FoCaLiZe compiler together with dependencies which enables to have statements and proofs in a coherent way. -- Renaud Rioboo _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

## Re: [Proving Axiom Correct] Bootstrapping a library

 Renaud,I've been looking at FoCal and, in particular, the Zenon programhttp://zenon.inria.fr/zenlpar07.pdfZenon appears to be able to output OCAML code from proofs.In your opinion is it reasonable to consider modifying the back endto output Spad code?TimOn Fri, Feb 10, 2017 at 8:39 AM, Tim Daly wrote:Renaud,I'm just getting around to the FoCal information. Obviously you've done a lot ofwork on this subject already. I have the papers and the reference manual nearthe top of the reading stack. I'm certain to have questions.Yes, BasicType requires properties for = such as symmetry which would haveto be proven at the Domain level for each implementation. Of course, = is notactually implemented directly in NNI but somewhere up the inheritance chain.For example, the domain ANY has  x = y ==    (x.dm = y.dm) and EQUAL(x.ob, y.ob)\$Lispwhere dm is a field in the Record implementation of ANY   Rep := Record(dm: SExpression, ob: None)which depends on the Lisp definition of EQUAL and SExpressionis one of String, Symbol, Integer, DoubleFloat, OutputFormWhereas the domain IndexedList implements  x = y ==    Qeq(x,y) => true    while not Qnull x and not Qnull y repeat      Qfirst x ^=\$S Qfirst y => return fase      x := Qrest x      y := Qrest y    Qnull x and Qnull ywhere   Qeq   ==> EQ\$Lisp  Qnull ==> NULL\$Lisp  Qfirst ==> QCAR\$Lisp  Qrest ==> QCDR\$Lispand   S : Type is a dependent argument type. Sigh.The proofs of = in each domain will involve an appeal to the Lispdefinition of a small number of functions. I'm using ACL2 for Lisp.This is where the ACL2 and Coq proofs meet.There is no such thing as a simple job.TimOn Fri, Feb 10, 2017 at 5:13 AM, Renaud Rioboo wrote:Dear Axiom gurus, Axiom's NNI inherits from a dozen Category objects, one of which is BasicType which contains two signatures:  ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> Boolean In the ideal case we would decorate BasicType with the existing definitions of = and ~= so we could create a new library structure for the logic system. So BasicType would contain theorem = (a, b : Type) : Boolean := ..... theorem ~= (a, b : Type) : Boolean := .... Since BasicType is not an implementation you need to write a specification for equal and different. These specifictions should be inherited and proved at the domain level. You can see the standard library of FoCaLiZe for details. In practice you need a language for writing logical statements and a language to prove these statements. Again see the FoCaLiZe library (for instance lattices) to see how a statement can be used in a proof. Unfortunately it appears the Coq and Lean will not take kindly to removing the existing libraries and replacing them with a new version that only contains a limited number of theorems. I'm not yet sure about FoCaL but I suspect it has the same bootstrap problem. Inheritance is managed by the FoCaLiZe compiler together with dependencies which enables to have statements and proofs in a coherent way. -- Renaud Rioboo _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer