Termination Proofs and Complexity Certification

  • Daniel Leivant
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


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.


Classical Logic Recursive Function Atomic Formula Intuitionistic Logic Functional Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Arnold Beckmann and Andreas Weiermann. Characterizing the elementary recursive functions by a fragment of Gödel’s system t. Archive of Math. Logic, 39:475–491, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Stephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the poly-time functions. Computational Complexity, 1992.Google Scholar
  3. 3.
    Samuel Buss. Bounded Arithmetic. Bibliopolis, Naples, 1986.Google Scholar
  4. 4.
    Kurt Gödel. Uber eine bisher noch nicht benutzte erweiterung des finiten standpunktes. Dialectica, 12:280–287, 1958.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Petr Hájek and Pavel Pudlák. Metamathematics of First-Order Arithmetic. Springer, Berlin, 1993.zbMATHGoogle Scholar
  6. 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. 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
  8. 8.
    N. Jones. Computability and Complexity from a Programming Perspective. MIT Press, Cambridge, MA, 1997.zbMATHGoogle Scholar
  9. 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. 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. 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. 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. 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. Scholar
  14. 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
  15. 15.
    Daniel Leivant. Applicative control and computational complexity. In J. Flum and M. Rodriguez-Artalejo, editors, Computer Science Logic (Proceedings of the Thirteenth CSL Conference, pages 82–95, Berlin, 1999. Springer Verlag (LNCS 1683). Scholar
  16. 16.
    Daniel Leivant. Intrinsic reasoning about functional programs I: first order theories. Annals of Pure and Applied Logic, 2001.
  17. 17.
    Daniel Leivant. Substructural proofs and feasibility., 2001.
  18. 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
  19. 19.
    D. Prawitz. Natural Deduction. Almqvist and Wiksell, Uppsala, 1965.zbMATHGoogle Scholar
  20. 20.
    H.E. Rose. Subrecursion. Clarendon Press (Oxford University Press), Oxford, 1984.zbMATHGoogle Scholar
  21. 21.
    M. Schonfinkel. Uber die Bausteine der mathematischen Logik. Mathematische Annalen, 92:305–316, 1924. English translation: On the building blocks of mathematical logic, in [6], 355-366.CrossRefMathSciNetGoogle Scholar
  22. 22.
    Harold Simmons. The realm of primitive recursion. Archive for Mathematical Logic, 27:177–188, 1988.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    S. Simpson. Subsystems of Second-Order Arithmetic. Springer-Verlag, Berlin, 1999.zbMATHGoogle Scholar
  24. 24.
    A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, Cambridge, 1996, 2000.zbMATHGoogle Scholar
  25. 25.
    Kai F. Wehmeier. Fragments of HA based on Σ 1-induction. Archive for Mathematical Logic, 37:37–49, 1997.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Daniel Leivant
    • 1
  1. 1.Computer Science DepartmentIndiana UniversityBloomington

Personalised recommendations