Proving Axiom Correct

Previous Topic Next Topic
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view

Proving Axiom Correct

Tim Daly
* 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

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

Axiom-developer mailing list
[hidden email]