> 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 <address@hidden
<mailto:address@hidden>> wrote:
On Wed, Feb 8, 2017 at 9:23 PM, Tim Daly <address@hidden
<mailto:address@hidden>> 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 <address@hidden
<mailto: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,
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 <address@hidden
<mailto:address@hidden>> 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