* 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.", _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |