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.. 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).
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.
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 <avi...@cmu.edu> 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 <axiom...@gmail.com> 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
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
