Extracting Feasible Programs

Logic-Based Program Synthesis: State of the Art and Future Trends

Volume

Papers from the 2002 AAAI Spring Symposium

Contents

This work in progress paper presents a methodology for reasoning about the computational complexity of functional programs, which are extracted from proofs. We suggest a first order arithmetic AT0 which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which is provably total in AT0, is exactly the set of polynomial time functions. This result has been accepted at Conference of the European Association for Computer Science Logic (CSL), 2002. Compared to others feasible arithmetics, $StrictTa$ is surprisingly simpler. The main feature of AT0 concerns the treatment of the quantification. The range of quantifiers is restricted to the set of actual terms which is the set of constructor terms with variables. The second feature concerns a restriction of the inductive formulas. Although this paper addresses some theoretical aspects of program extractions, it is relevant for practical issue, in the long term, because certifying the computational resource consumed by a program is a challenging issue.