* 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.",