diff --git a/books/ProvingAxiomCorrect.pamphlet b/books/ProvingAxiomCorrect.pamphlet index 55192fb..6ef366f 100644 --- a/books/ProvingAxiomCorrect.pamphlet +++ b/books/ProvingAxiomCorrect.pamphlet @@ -1,10 +1,74 @@ \documentclass[dvipdfm]{book} -\newcommand{\VolumeName}{Volume 14: Proving Axiom Correct} +\newcommand{\VolumeName}{Volume 13: Proving Axiom Correct} \input{bookheader.tex} \mainmatter \setcounter{chapter}{0} % Chapter 1 -\chapter{Goals and Background} +\chapter{Here is a problem} +The goal is to prove that Axiom's implementation of +the Euclidean GCD algorithm is correct. +From category EuclideanDomain (EUCDOM) we find the implementation of +the Euclidean GCD algorithm: +\begin{verbatim} + 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 +\end{verbatim} +The unitCanonical function comes from the category IntegralDomain (INTDOM) +where we find: +\begin{verbatim} + unitNormal: % -> Record(unit:%,canonical:%,associate:%) + ++ unitNormal(x) tries to choose a canonical element + ++ from the associate class of x. + ++ The attribute canonicalUnitNormal, if asserted, means that + ++ the "canonical" element is the same across all associates of x + ++ if \spad{unitNormal(x) = [u,c,a]} then + ++ \spad{u*c = x}, \spad{a*u = 1}. + unitCanonical: % -> % + ++ \spad{unitCanonical(x)} returns \spad{unitNormal(x).canonical}. +\end{verbatim} +implemented as +\begin{verbatim} + UCA ==> Record(unit:%,canonical:%,associate:%) + if not (% has Field) then + unitNormal(x) == [1$%,x,1$%]$UCA -- the non-canonical definition + unitCanonical(x) == unitNormal(x).canonical -- always true + recip(x) == if zero? x then "failed" else _exquo(1$%,x) + unit?(x) == (recip x case "failed" => false; true) + if % has canonicalUnitNormal then + associates?(x,y) == + (unitNormal x).canonical = (unitNormal y).canonical + else + associates?(x,y) == + zero? x => zero? y + zero? y => false + x exquo y case "failed" => false + y exquo x case "failed" => false + true +\end{verbatim} + +\section{Approaches} +There are several systems that could be applied to approach the proof. + +I plan to initially look at Coq and ACL2. I suspect, from my initial +understanding of both systems, that both systems are needed. Coq +seems to be applicable at the Spad level. ACL2 seems to be applicable +at the Lisp level. Both levels are necessary for a proper proof. + +\chapter{It is an interesting problem} +\chapter{It is an unsolved problem} +\chapter{Here is my idea} +\chapter{My idea works} +\chapter{Here is how my idea compares to others} \begin{thebibliography}{99} \bibitem[Bertot 04]{Bert04} Bertot, Yves; Cast\'eran, Pierre\\ Interactive Theorem Proving and Program Development''\\ diff --git a/changelog b/changelog index 14365a5..cd4c232 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,5 @@ +20140613 tpd src/axiom-website/patches.html 20140613.02.tpd.patch +20140613 tpd books/ProvingAxiomCorrect state the problem 20140613 tpd src/axiom-website/patches.html 20140613.01.tpd.patch 20140613 tpd books/ProvingAxiomCorrect created 20140612 tpd src/axiom-website/patches.html 20140612.01.tpd.patch diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index a7c2ab1..ec59716 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -4422,6 +4422,8 @@ books/bookvolbib add Le96a books/bookvolbib add Proving Axiom Correct section, Bert04 20140613.01.tpd.patch books/ProvingAxiomCorrect created +20140613.02.tpd.patch +books/ProvingAxiomCorrect state the problem