From be2a82fe51d49a52d26692ba38bba49ad6979787 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 29 Jul 2015 08:41:22 -0400
Subject: [PATCH] books/bookvol13 Add mathematics for GCD proof
Goal: Prove Axiom correct
Buchberger presents a proof of the GCD algorithm.
---
books/bookvol13.pamphlet | 56 +++++++++++++++++++
books/bookvolbib.pamphlet | 118 +++++++++++++++++++++++++++++++++++++---
changelog | 3 +
patch | 5 +-
src/axiom-website/patches.html | 2 +
5 files changed, 174 insertions(+), 10 deletions(-)
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 735419c..ae81603 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -149,6 +149,62 @@ implemented as
true
\end{verbatim}
+\section{Mathematics}
+
+From Buchberger\cite{Buch97},
+
+Define ``divides''
+\[ t\vert a \Longleftrightarrow \exists u (t \cdot u = a)\]
+
+Define ``greatest common divisor''
+\[ {\rm GCD}(a,b) = \forall t\ max(t\vert a \land t\vert b)\]
+
+Theorem:
+\[ (t\vert a \land t\vert b) \Longleftrightarrow t\vert (a-b) \land t\vert b\]
+
+Euclids' Algorithm
+\[ a > b \Rightarrow {\rm GCD}(a,b) = {\rm GCD}(a-b,b)\]
+
+By the definition of GCD we need to show that
+\[\forall t\ max(t\vert a \land t\vert b) =
+ \forall t\ max(t\vert (a-b) \land t\vert b)\]
+
+Thus we need to show that
+\[(t\vert a \land t\vert b) \Longleftrightarrow (t\vert (a-b) \land t\vert b)\]
+
+Let $t$ be arbitrary but fixed and assume
+\begin{equation}\label{eq1}(t\vert a \land t\vert b)\end{equation}
+
+We have to show
+\begin{equation}\label{eq2}t\vert (a-b)\end{equation}
+
+and
+\begin{equation}\label{eq3}t\vert b\end{equation}
+
+Equation \ref{eq3} follows propositionally. For equation \ref{eq2},
+by definition of ``divides'', we have to find a $w$ such that
+\begin{equation}\label{eq4}t \cdot w = a-b\end{equation}
+
+From \ref{eq1}, by definition of ``divides'', we know that for certain
+$u$ and $v$
+\[t \cdot u = a\]
+
+and
+\[t \cdot v - b\]
+
+Hence,
+\[ a-b = t \cdot u - t \cdot v\]
+
+But
+\[t \cdot u - t \cdot v = t \cdot (u - v)\]
+
+So we need to find
+\[w = u - v\]
+
+and
+\[\textrm{Find w such that }t \cdot u - t \cdot v = t \cdot w\]
+
+
\section{Approaches}
There are several systems that could be applied to approach the proof.
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 89e2671..39bfe77 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2404,6 +2404,20 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Buchberger, Bruno}
+\begin{chunk}{axiom.bib}
+@article{Buch97,
+ author = "Buchberger, Bruno",
+ title = "Mathematica: doing mathematics by computer?",
+ journal = "Advances in the design of symbolic computation systems",
+ year = "1997",
+ publisher = "Springer-Verlag",
+ pages = "2-20",
+ isbn = "978-3-211-82844-1",
+}
+
+\end{chunk}
+
\index{Bressoud, David}
\begin{chunk}{axiom.bib}
@article{Bres93,
@@ -2418,14 +2432,55 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Geuvers, Herman}
+\index{Pollack, Randy}
+\index{Wiedijk, Freek}
+\index{Zwanenburg, Jan}
+\begin{chunk}{axiom.bib}
+@article{Geuv02,
+ author = "Geuvers, Herman and Pollack, Randy and Wiedijk, Freek and
+ Zwanenburg, Jan",
+ title = "A Constructive Algebraic Hierarchy in Coq",
+ year = "2002",
+ journal = "Journal of Symbolic Computation",
+ paper = "Geuv02.pdf",
+ keywords = "axiomref",
+ abstract =
+ "We describe a framework of algebraic structures in the proof assistant
+ Coq. We have developed this framework as part of the FTA project in
+ Nijmegen, in which a constructive proof of the Fundamental Theorem of
+ Algebra has been formalized in Coq.
+
+ The algebraic hierarchy that is described here is both abstract and
+ structured. Structures like groups and rings are port of it in an
+ abstract way, defining e.g. a ring as a tuple consisting of a group, a
+ binary operation and a constant that together satisfy the properties
+ of a ring. In this way, a ring automatically inherits the group
+ properties of the additive subgroup. The algebraic hierarchy is
+ formalized in Coq by applying a combination of labeled record types
+ and coercions. In the labeled record types of Coq, one can use
+ {\sl dependent types}: the type of one label may depend on another
+ label. This allows to give a type to a dependent-typed tuple like
+ $\langle A, f, a \rangle$, where $A$ is a set, $f$ an operation on $A$
+ and $a$ an element of $A$. Coercions are functions that are used
+ implicitly (they are inferred by the type checker) and allow, for
+ example, to use the structure $\mathcal{A} := \langle A, f, a \rangle$
+ as a synonym or the carrier set $A$, as is often done in mathematical
+ practice. Apart rom the inheritance and reuse of properties, the
+ algebraic hierarchy has proven very useful for reusing notations."
+
+}
+
+\end{chunk}
+
\index{Medina-Bulo, I.}
\index{Palomo-Lozano, F.}
\index{Alonso-Jim\'enez, J.A.}
\index{Ruiz-Reina, J.L.}
\begin{chunk}{axiom.bib}
@article{Bulo04,
- author = "Medina-Bulo, I. and Palomo-Lozano, F. and Alonso-Jim\'enez, J.A.
- and Ruiz-Reina, J.L.",
+ author = {Medina-Bulo, I. and Palomo-Lozano, F. and Alonso-Jim\'enez, J.A.
+ and Ruiz-Reina, J.L.},
title = "Verified Computer Algebra in ACL2",
journal = "ASIC 2004, LNAI 3249",
year = "2004",
@@ -8610,14 +8665,15 @@ IBM Research Report, RC3062 Sept
\index{Boulanger, Jean-Louis}
\begin{chunk}{ignore}
-\bibitem[Boulanger 91]{Bou91}
+@misc{Boul91,
author = "Boulanger, Jean-Louis",
title = "Etude de la compilation de scratchpad 2",
year = "1991",
month = "September",
-Rapport de DEA Universite dl lille 1
+ publisher = "Rapport de DEA Universite dl lille 1",
keywords = "axiomref",
+}
\end{chunk}
\index{Boulanger, Jean-Louis}
@@ -8655,15 +8711,15 @@ Rapport de DEA Universite dl lille 1
\end{chunk}
\index{Boulanger, Jean-Louis}
-\begin{chunk}{ignore}
-\bibitem[Boulanger 94]{Bou94}
+\begin{chunk}{axiom.bib}
+@misc{Boul95,
author = "Boulanger, J.L.",
title = "Object Oriented Method for Axiom",
year = "1995",
month = "February",
pages = "33-41",
paper = "Bou94.pdf",
-ACM SIGPLAN Notices, 30(2) CODEN SINODQ ISSN 0362-1340
+ publisher = "ACM SIGPLAN Notices, 30(2) CODEN SINODQ ISSN 0362-1340",
keywords = "axiomref",
abstract = "
Axiom is a very powerful computer algebra system which combines two
@@ -16371,6 +16427,54 @@ Math. Tables Aids Comput. 10 91--96. (1956)
\end{chunk}
+\index{Thiery, Nicolas M.}
+\begin{chunk}{axiom.bib}
+@misc{Thie15,
+ author = "Thiery, Nicolas M.",
+ title = "Open Digital Research Environment Toolkit for the Advancement of Mathematics",
+ year = "2015",
+ url = "http://opendreamkit.org",
+ paper = "Thie15.pdf",
+ abstract =
+ "OpenDreamKit will deliver a flexible toolkit enabling research groups
+ to set up Virtual Research Environments, customised to meet the varied
+ needs of research projects in pure mathematics and applications, and
+ supporting the full research life-cycle from exploration, through
+ proof and publication, to archival and sharing of data and code.
+
+ OpenDreamKit will be built out of a sustainable ecosystem of
+ community-developed open software, databases, and ser- vices,
+ including popular tools such as LINBOX, MPIR, SAGE (sagemath.org),
+ GAP, PARI/GP, LMFDB, and SINGULAR. We will extend the JUPYTER Notebook
+ environment to provide a flexible user interface. By improving and
+ unifying existing build- ing blocks, OpenDreamKit will maximise both
+ sustainability and impact, with beneficiaries extending to scientific
+ computing, physics, chemistry, biology and more, and including
+ researchers, teachers, and industrial practitioners.
+
+ We will define a novel component-based VRE architecture and adapt
+ existing mathematical software, databases, and user interface
+ components to work well within it on varied platforms. Interfaces to
+ standard HPC and grid services will be built in. Our architecture will
+ be informed by recent research into the sociology of mathematical
+ collaboration, so as to properly support actual research practice. The
+ ease of set up, adaptability and global impact will be demonstrated in
+ a variety of demonstrator VREs.
+
+ We will ourselves study the social challenges associated with
+ large-scale open source code development and publications based on
+ executable documents, to ensure sustainability.
+
+ OpenDreamKit will be conducted by a Europe-wide steered by demand
+ collaboration, including leading mathematicians, computational
+ researchers, and software developers with a long track record of
+ delivering innovative open source software solutions for their
+ respective communities. All produced code and tools will be open
+ source."
+}
+
+\end{chunk}
+
\eject
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Bibliography}
diff --git a/changelog b/changelog
index bb44775..03cfc64 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20150729 tpd src/axiom-website/patches.html 20150729.01.tpd.patch
+20150729 tpd books/bookvolbib add Buch97 reference for GCD proof
+20150729 tpd books/bookvol13 Add mathematics for GCD proof
20150718 tpd src/axiom-website/patches.html 20150718.01.tpd.patch
20150718 tpd books/bookvol13 Add program proof papers
20150718 tpd books/bookvolbib Add program proof papers
diff --git a/patch b/patch
index 82321d3..ed25f26 100644
--- a/patch
+++ b/patch
@@ -1,6 +1,5 @@
-books/bookvolbib: Add program proof papers
+books/bookvol13 Add mathematics for GCD proof
Goal: Prove Axiom correct
-Several papers related to proving algorithms (Buchberger's, GCD,
-and Cylindrical Algebraic Decomposition) were added.
+Buchberger presents a proof of the GCD algorithm.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 0701609..a8e4722 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5108,6 +5108,8 @@ Makefile: extract and run proof code automatically

Makefile: extract and run proof code automatically

20150718.01.tpd.patch
books/bookvolbib Add program proof papers

+20150729.01.tpd.patch
+books/bookvol13 Add mathematics for GCD proof

--
1.7.5.4