From b812580d096975d8df8dbe18a02c4c6ce29bd666 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 4 Mar 2018 04:01:03 -0500
Subject: [PATCH] proposal
Goal: Proving Axiom Correct
---
changelog | 2 +
patch | 91 ++++++++++++++++++++++++-
proposal | 148 +++++++++++++++++++++++++++++++++++++++++
src/axiom-website/patches.html | 2 +
4 files changed, 241 insertions(+), 2 deletions(-)
create mode 100644 proposal
diff --git a/changelog b/changelog
index da9904c..439a0c1 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20180304 tpd src/axiom-website/patches.html 20180304.01.tpd.patch
+20180304 tpd proposal
20180227 tpd src/axiom-website/patches.html 20180227.03.tpd.patch
20180227 tpd books/bookvol10.1 add new chapter
20180227 tpd src/axiom-website/patches.html 20180227.02.tpd.patch
diff --git a/patch b/patch
index c59bcb8..d413c96 100644
--- a/patch
+++ b/patch
@@ -1,3 +1,90 @@
-books/bookvol10.1 add new chapter
+books/bookvolbib add references
-Goal: Axiom Literate Documentation
\ No newline at end of file
+Goal: Proving Axiom Correct
+
+\index{Harper, Robert}
+\begin{chunk}{axiom.bib}
+@phdthesis{Harp85,
+ author = "Harper, Robert",
+ title = {{Aspects of the Implementation of Type Theory}},
+ school = "Cornell University",
+ year = "1985",
+ comment = "TR 85-675",
+ abstract =
+ "This thesis is about building an automated programming logic. For our
+ purposes an automated programming logic consists of
+ \begin{itemize}
+ \item A formal system for reasoning about programs
+ \item A proof development environment which includes, at least, an
+ editor for the construction of proofs in the logic
+ \item Mechanized decision methods to assist in the proof development
+ process
+ \item A library mechanism for managing collections of theorems
+ \end{itemize}",
+ paper = "Harp85.pdf"
+}
+
+\end{chunk}
+
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@phdthesis{Fill99,
+ author = "Filliatre, Jean-Christophe",
+ title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
+ school = {{Universit\'e Paris Sud}},
+ year = "1999"
+}
+
+\end{chunk}
+
+\index{Blanqui, Frederic}
+\index{jouannaud, Jean-Pierre}
+\index{Okada, Mitsuhiro}
+\begin{chunk}{axiom.bib}
+@inproceedings{Blan99,
+ author = "Blanqui, Frederic and jouannaud, Jean-Pierre and Okada, Mitsuhiro",
+ title = {{The Calculus of Algebraic Constructions}},
+ booktitle = "Rewriting Techniques and Applications RTA-99",
+ year = "1999",
+ publisher = "LNCS 1631",
+ link = "\url{https://hal.inria.fr/inria-00105545v1/document}",
+ abstract =
+ "This paper is concerned with the foundations of the Calculus of
+ Algebraic Constructions (CAC), an extension of the Calculus of
+ Constructions by inductive data types. CAC generalizes inductive
+ types equipped with higher-order primitive recursion, by providing
+ definition s of functions by pattern-matching which capture recursor
+ definitions for arbitrary non-dependent and non-polymorphic inductive
+ types satisfying a strictly positivity condition. CAC also
+ generalizes the first-order framework of abstract data types by
+ providing dependent types and higher-order rewrite rules.",
+ paper = "Blan99.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Blanqui, Frederic}
+\begin{chunk}{axiom.bib}
+@article{Blan05,
+ author = "Blanqui, Frederic",
+ title = {{Inductivev Types in the Calculus of Algebraic Constructions}},
+ journal = "Fundamenta Informaticae",
+ volume = "65",
+ number = "1-2",
+ pages = "61-86",
+ year = "2005",
+ abstract =
+ "In a previous work, we proved that an important part of the Calculus
+ of Inductive Constructions (CIC), the basis of the Coq proof
+ assistant, can be seen as a Calculus of Algebraic Constructions
+ (CAC), an extension of the Calculus of Constructions with functions
+ and predicates defined by higher-order rewrite rules. In this
+ paper, we prove that almost all CIC can be seen as a CAC, and that it
+ can be further extended with non-strictly positive types and
+ inductive-recursive types together with non-free constructors and
+ pattern-matching on defined symbols.",
+ paper = "Blan05.pdf"
+}
+
+\end{chunk}
diff --git a/proposal b/proposal
new file mode 100644
index 0000000..31a9c80
--- /dev/null
+++ b/proposal
@@ -0,0 +1,148 @@
+* Proving Axiom Correct is the overall research goal.
+
+ Axiom is a very large, strongly typed, general purpose computer
+ algebra system. It has several thousand functions which implement
+ known, standard mathematical functions and known, standard computer
+ science algorithms.
+
+ As a result, the specification of the behavior of a function written
+ in the Spad language is externally defined. However, the external
+ function specifications need to be formalized before they can be used
+ in a formal type system.
+
+ Because Axiom is strongly typed it is an ideal candidate for
+ assistance of proofs by a formal system like Coq.
+
+* Uniqueness of the research
+
+ An extensive survey [0] from 1968 to the present shows that there has
+ been no equivalent effort to prove a computer algebra system correct.
+ Indeed, there has been little overlap between the computer algebra
+ and proof system efforts. In these prior efforts the computer algebra
+ systems have been a distant, UNTRUSTED oracle.
+
+ Our research attacks the fundamental issue of trust. By proving
+ Axiom's algorithms correct we plan to show that the results are
+ trusted. As a required side-effect, Axiom needs to integrate proof
+ constructs into the structure of the system, allowing direct checking
+ of proofs.
+
+* Impact of the research
+
+ There is a rich tradition of computational mathematics in computer
+ algebra systems. There is a rich tradition of computational reasoning
+ in proof systems. These two systems currently have nearly disjoint
+ sets of researchers. At most, proof systems have attempted to prove
+ computational algorithms (e.g. Groebner basis). However, there are
+ hundreds of person-years of work in a system like Axiom, costing over
+ 40 million dollars to develop. It is unlikely that this work will be
+ recreated from scratch so we need to rely on existing algorithms.
+
+ Successful creation of a (prototype) merger of these two fields
+ has the potential impact on both. Existing algorithms have a
+ platform for integrated proofs and proof systems have a rich
+ source of computational mathematics.
+
+* Prior work related to the feasibility of the research goal
+
+ Spad programs which implement mathematical functions (e.g. GCD) are
+ strongly typed and written in an imperative style. Two issues need to
+ be explored in detail. The first issue is handling imperative programs
+ in Coq. The second issue is handling algebraic constructs in Coq.
+
+ Filliatre [1] researched the verification of non-functional
+ programs using interpretations in type theory. He defines a logical
+ interpretation of an annotated program as a partial proof of its
+ specification. To do this he provides partial proof terms as "proof
+ obligations", terms left open for the user to prove. Validity of these
+ proof obligations implies the total correctness of the program. We
+ believe that this research, and its Coq implementation, provides a
+ basis for handling Spad imperative constructs.
+
+ Blanqui et al. [2][3] provides an extension of the CIC basis of Coq with
+ the Calulus of Algebraic Constructions (CAC) which is an extension of
+ CIC by inductive data types. This work provides a more algebraic basis
+ for Coq programs by providing dependent types and higher-order rewrite
+ rules. This provides a basis for handling Axiom's algebraic constructs
+ in a formal system.
+
+* Plan for near-term research
+
+ The plan is to focus on the GCD algorithm as implemented in Axiom.
+ There are 22 different GCD algorithms exported by various domains
+ (e.g. polynomials).
+
+ In order to prove the algorithm, Axiom needs to know various
+ propositions about groups, rings, etc. which are inherited by each
+ of the domains. It also needs to have a way of collecting these
+ propositions as they apply to each individual domain. This work is
+ necessary and generic to the project goal and lays the groundwork
+ for future proofs. A large part of the near-term effort will
+ involve "decorating" Axiom's type hierarchy with propositions
+ related to both group theory and computer science algorithms.
+
+ The expected result will be a Coq-based proof of the GCD algorithm
+ using the collected propostions and the specification of the GCD.
+
+ There is also a need to study an extension of Filliatre's research to
+ handle dependent types. A result in this area would be of interest
+ beyond the Axiom community. This is a longer term, necessary, and
+ interesting effort expected as a side-effect of this work.
+
+[0] Daly, Timothy (in preparation)
+
+[1] Filliatre, Jean-Christophe, "{Verification of Non-Functional Programs
+using Interpretations in Type Theory", J. Functional Programming 13(4),
+709-745, 2003,
+ "We study the problem of certifying programs combining imperative
+ and functional features within the general framework of type
+ theory.
+
+ Type theory is a powerful specification language, which is
+ naturally suited for the proof of purely functional programs. To
+ deal with imperative programs, we propose a logical interpretation
+ of an annotated program as a partial proof of its
+ specification. The construction of the corresponding partial proof
+ term is based on a static analysis of the effects of the program
+ which excludes aliases. The missing subterms in the partial proof
+ term are seen as proof obligations, whose actual proofs are left
+ to the user. We show that the validity of those proof obligations
+ implies the total correctness of the program.
+
+ This work has been implemented in the Coq proof assistant. It
+ appears as a tactic taking an annotated program as argument and
+ generating a set of proof obligations. Several nontrivial
+ algorithms have been certified using this tactic.",
+
+[2] Blanqui, Frederic, jouannaud, Jean-Pierre, and Okada, Mitsuhiro
+"The Calculus of Algebraic Constructions",
+Rewriting Techniques and Applications RTA-99, 1999
+ "This paper is concerned with the foundations of the Calculus of
+ Algebraic Constructions (CAC), an extension of the Calculus of
+ Constructions by inductive data types. CAC generalizes inductive
+ types equipped with higher-order primitive recursion, by providing
+ definition s of functions by pattern-matching which capture recursor
+ definitions for arbitrary non-dependent and non-polymorphic inductive
+ types satisfying a strictly positivity condition. CAC also
+ generalizes the first-order framework of abstract data types by
+ providing dependent types and higher-order rewrite rules."
+
+[3] Blanqui, Frederic "Inductivev Types in the Calculus of Algebraic
+Constructions", Fundamenta Informaticae, 65(1-2), 61-86, 2005
+ "In a previous work, we proved that an important part of the Calculus
+ of Inductive Constructions (CIC), the basis of the Coq proof
+ assistant, can be seen as a Calculus of Algebraic Constructions
+ (CAC), an extension of the Calculus of Constructions with functions
+ and predicates defined by higher-order rewrite rules. In this
+ paper, we prove that almost all CIC can be seen as a CAC, and that it
+ can be further extended with non-strictly positive types and
+ inductive-recursive types together with non-free constructors and
+ pattern-matching on defined symbols.",
+
+
+
+
+
+
+
+
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 32f6299..a9183bf 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5914,6 +5914,8 @@ books/bookvolbib add references

books/bookvolbug bug 7335: type resolution failure

20180227.03.tpd.patch
books/bookvol10.1 add new chapter

+20180304.01.tpd.patch
+proposal

--
1.9.1