Termination proofs and complexity certification

Abstract

We show that simple structural conditions on proofs of convergence of equational programs, in the intrinsic-theories verification framework of [16], 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.