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