Termination Proofs and Complexity Certification
We show that simple structural conditions on proofs of convergence of equational programs, in the intrinsic-theories verification framework of , correspond to resource bounds on program execution. These conditions may be construed as reflecting finitistic-predicative reasoning. The results provide a user-transparent method for certifying the computational complexity of functional programs. In particular, we define natural notions of data-positive formulas and of data-predicative derivations, and show that restricting induction to data-positive formulas captures precisely the primitive recursive functions, data-predicative derivations characterize the Kalmar-elementary functions, and the combination of both yields the poly-time functions.
KeywordsClassical Logic Recursive Function Atomic Formula Intuitionistic Logic Functional Program
Unable to display preview. Download preview PDF.
- 2.Stephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the poly-time functions. Computational Complexity, 1992.Google Scholar
- 3.Samuel Buss. Bounded Arithmetic. Bibliopolis, Naples, 1986.Google Scholar
- 6.J. van Heijenoort. From Frege to Godel, A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, Cambridge, MA, 1967.Google Scholar
- 7.W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, New York, 1980. Preliminary manuscript: 1969.Google Scholar
- 9.Daniel Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In Proceedings of the Twenty Fourth Annual Symposium on the Foundations of Computer Science, pages 460–469, Washington, 1983. IEEE Computer Society.Google Scholar
- 10.Daniel Leivant. Contracting proofs to programs. In P. Odifreddi, editor, Logic and Computer Science, pages 279–327. Academic Press, London, 1990.Google Scholar
- 11.Daniel Leivant. Subrecursion and lambda representation over free algebras. In Samuel Buss and Philip Scott, editors, Feasible Mathematics, Perspectives in Computer Science, pages 281–291. Birkhauser-Boston, New York, 1990.Google Scholar
- 12.Daniel Leivant. A foundational delineation of poly-time. Information and Computation, 110:391–420, 1994. (Special issue of selected papers from LICS’91, edited by G. Kahn). Preminary report: A foundational delineation of computational feasibility, in Proceedings of the Sixth IEEE Conference on Logic in Computer Science, IEEE Computer Society Press, 1991.Google Scholar
- 13.Daniel Leivant. Ramified recurrence and computational complexity I: Word recurrence and poly-time. In Peter Clote and Jeffrey Remmel, editors, Feasible Mathematics II, Perspectives in Computer Science, pages 320–343. Birkhauser-Boston, New York, 1994. http://www.cs.indiana.edu/?leivant/papers.Google Scholar
- 14.Daniel Leivant. Intrinsic theories and computational complexity. In D. Leivant, editor, Logic and Computational Complexity, LNCS, pages 177–194, Berlin, 1995. Springer-Verlag.Google Scholar
- 16.Daniel Leivant. Intrinsic reasoning about functional programs I: first order theories. Annals of Pure and Applied Logic, 2001. http://www.cs.indiana.edu/?leivant/papers.
- 17.Daniel Leivant. Substructural proofs and feasibility. http://www.cs.indiana.edu/~leivant/papers, 2001.
- 18.Charles Parsons. On a number-theoretic choice schema and its relation to induction. In A. Kino, J. Myhill, and R. Vesley, editors, Intuitionism and Proof Theory, pages 459–473. North-Holland, Amsterdam, 1970.Google Scholar