Martin,
There is a distinction to be made between mathematical AXIOMS for
the category (e.g. associative) and SIGNATURES for the functions
in a category (domain, package).
Interesting questions arise for functions like coerce, convert,
and retract about how they preserve AXIOMs across domains.
A look at the definition of gcd in catdef.spad shows that the tricky
bit is how to deal with imperative constructs like while ... repeat etc.
In Coq's standard libraries we find gcd in Coq.ZArith.Znumtheory [1]
and in Coq.ZArith.Zgcd_alt [2], whereby the latter (earlier version) is
based on
I'm taking Pierce's online course at the moment (Software Foundations
in Coq).
and in Coq.ZArith.Zgcd_alt [2], whereby the latter (earlier version) is
based on Euclid's algorithm which is more suitable for our purposes.
It is becoming clear that between an implmentation of an algorithm and
its
On 25/07/15 12:38, d...@axiom-developer.org wrote:
Axiom has moved into a new phase. The goal is to prove Axiom correct.
Tim,
Why not do the easy bit first and just mark up the operators, in
domains, with the following common Axioms/Identities?
Only for functions with signature:
