Extracting Feasible Programs

Jean-Yves Marion

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.