Polynomial-time Algorithms from Ineffective Proofs

10 years 1 days ago
Polynomial-time Algorithms from Ineffective Proofs
We present a constructive procedure for extracting polynomial-time realizers from ineffective proofs of Π0 2theorems in feasible analysis. By ineffective proof we mean a proof which involves the non-computational principle weak K¨onig’s lemma WKL, and by feasible analysis we mean Cook and Urquhart’s system CPVω plus quantifierfree choice QF-AC. We shall also discuss the relation between the system CPVω +QF-AC and Ferreira’s base theory for feasible analysis BTFA, for which Π0 2-conservation of WKL has been non-constructively proven. This paper treats the case of weak K¨onig’s lemma for trees defined by Π0 1formulas. Illustrating the applicability of CPVω + QF-AC extended with this form of weak K¨onig’s lemma, we indicate how to formalize the proof of the Heine/Borel covering lemma in this system. The main techniques used in the paper are G¨odel’s functional interpretation and a novel form of binary bar recursion.
Paulo Oliva
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where LICS
Authors Paulo Oliva
Comments (0)