Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the polytime functions. In: Twenty-fourth Annual ACM Symposium on Theory of Computing (1992)
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)
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)
Leivant, D.: Subrecursion and lambda representation over free algebras. In: Buss, S., Scott, P. (eds.) Feasible Mathematics, Birkhauser, pp. 281–292 (1990)
Bellantoni, S., Niggl, K.H., Schwichtenberg, H.: Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic 104 (2000)
Hofmann, M.: Typed lambda calculi for polynomial-time computation. Habilitation thesis, TU Darmstadt (1998)
Hofmann, M.: Safe recursion with higher types and BCK-algebra. Annals of Pure Applied Logic 104, 113–166 (2000)
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)
Givan, R., McAllester, D.: Polynomial-time computation via local inference relations. ACM Transactions on Computational Logic 3, 521–541 (2002)
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)
Hofmann, M.: Linear types and non-size-increasing polynomial time computation. Information and Computation 183, 57–85 (2003)
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)
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation 1, 497–536 (1991)
Qian, Z.: Unification of higher-order patterns in linear time and space. J. Log. Comput. 6, 315–341 (1996)
Verma, R.M.: General techniques for analyzing recursive algorithms with applications. SIAM Journal of Computing 26, 568–581 (1997)
Caseiro, V.H.: Equations for defining poly-time functions. PhD thesis, University of Oslo (1997)
Harrop, R.: Concerning formulas of the types A → B∨C,A → (Ex)(Bx). Journal of Symbolic Logic 25, 27–32 (1960)
Miller, D.: Hereditary harrop formulas and logic programming. In: Proceedings of the VIII International Congress of Logic, Methodology, and Philosophy of Science, Moscow (1987)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schürmann, C., Shah, J. (2005). Identifying Polynomial-Time Recursive Functions. In: Ong, L. (eds) Computer Science Logic. CSL 2005. Lecture Notes in Computer Science, vol 3634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11538363_36
Download citation
DOI: https://doi.org/10.1007/11538363_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28231-0
Online ISBN: 978-3-540-31897-2
eBook Packages: Computer ScienceComputer Science (R0)