Identifying Polynomial-Time Recursive Functions

  • Carsten Schürmann
  • Jatin Shah
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


We present a sound and sufficient criterion for identifying polynomial-time recursive functions over higher-order data structures generalizing the seminal results by Bellantoni and Cook [1] and Leivant [2] to complex structural data-types. The criterion, presented as a deductive system, always terminates with a response that is either yes or don’t know. The criterion is complete in the sense that every polynomial-time recursive function over binary strings has at least one implementation that is identified by our criterion; whether this is also true for arbitrary higher-order data structures remains an open problem. Logic programming serves as the underlying model of computation and our results apply to the Horn fragment as well to the fragment of hereditary Harrop formulas.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the polytime functions. In: Twenty-fourth Annual ACM Symposium on Theory of Computing (1992)Google Scholar
  2. 2.
    Leivant, D.: A foundational delineation of computational feasibility. In: Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 2–11. IEEE, Los Alamitos (1991)CrossRefGoogle Scholar
  3. 3.
    Cobham, A.: The intrinsic computational complexity of functions. In: Bar-Hellel, Y. (ed.) Proceedings of the 1964 International Congress for Logic, Methodology, and the Philosophy of Science, pp. 24–30 (1965)Google Scholar
  4. 4.
    Leivant, D.: Subrecursion and lambda representation over free algebras. In: Buss, S., Scott, P. (eds.) Feasible Mathematics, Birkhauser, pp. 281–292 (1990)Google Scholar
  5. 5.
    Bellantoni, S., Niggl, K.H., Schwichtenberg, H.: Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic 104 (2000)Google Scholar
  6. 6.
    Hofmann, M.: Typed lambda calculi for polynomial-time computation. Habilitation thesis, TU Darmstadt (1998)Google Scholar
  7. 7.
    Hofmann, M.: Safe recursion with higher types and BCK-algebra. Annals of Pure Applied Logic 104, 113–166 (2000)zbMATHCrossRefGoogle Scholar
  8. 8.
    Ganzinger, H., McAllester, D.: A new meta-complexity theorem for bottom-up logic programs. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 5114–5128. Springer, Heidelberg (2001)Google Scholar
  9. 9.
    Givan, R., McAllester, D.: Polynomial-time computation via local inference relations. ACM Transactions on Computational Logic 3, 521–541 (2002)CrossRefMathSciNetGoogle Scholar
  10. 10.
    Aehlig, K., Schwichtenberg, H.: A syntactical analysis of non-size-increasing polynomial time computation. In: Fifteenth Annual IEEE Symposium on Logic in Computer Science (2000)Google Scholar
  11. 11.
    Hofmann, M.: Linear types and non-size-increasing polynomial time computation. Information and Computation 183, 57–85 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Rohwedder, E., Pfenning, F.: Mode and termination checking for higher-order logic programs. In: Nielson, H.R. (ed.) Proceedings of the European Symposium on Programming, Linköping, Sweden, pp. 296–310. Springer, Heidelberg (1996)Google Scholar
  13. 13.
    Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation 1, 497–536 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Qian, Z.: Unification of higher-order patterns in linear time and space. J. Log. Comput. 6, 315–341 (1996)zbMATHCrossRefGoogle Scholar
  15. 15.
    Verma, R.M.: General techniques for analyzing recursive algorithms with applications. SIAM Journal of Computing 26, 568–581 (1997)zbMATHCrossRefGoogle Scholar
  16. 16.
    Caseiro, V.H.: Equations for defining poly-time functions. PhD thesis, University of Oslo (1997)Google Scholar
  17. 17.
    Harrop, R.: Concerning formulas of the types A → B∨C,A → (Ex)(Bx). Journal of Symbolic Logic 25, 27–32 (1960)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Miller, D.: Hereditary harrop formulas and logic programming. In: Proceedings of the VIII International Congress of Logic, Methodology, and Philosophy of Science, Moscow (1987)Google Scholar
  19. 19.
    Schürmann, C., Shah, J.: Representing reductions of NP-complete problems in logical frameworks: A case study. In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN, ACM, New York (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Carsten Schürmann
    • 1
  • Jatin Shah
    • 1
  1. 1.Department of Computer ScienceYale UniversityNew HavenUSA

Personalised recommendations