Abstract
We restrict recursion in finite types so as to characterize the polynomial time computable functions. The restrictions are obtained by enriching the type structure with the formation of types ρ → σ and terms λ
ρ r as well as
and λx ρ r. Here we use two sorts of typed variables: complete ones
ρ and incomplete ones x ρ.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Stephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97–110, 1992.
Stephen Bellantoni and Martin Hofmann. A New “Feasible” Arithmetic Journal of Symbolic Logic, to appear.
Stephen Bellantoni, Karl-Heinz Niggl, and Helmut Schwichtenberg. Higher type recursion,ramification and polynomial time. Annals of Pure and Applied Logic, 104:17–30, 2000.
Stephen A. Cook. Computability and complexity of higher type functions. In Y.N. Moschovakis, editor, Logic from Computer Science, Proceedings of a Workshop held November 13-17, 1989, number 21 in MSRI Publications, pages 51–72. Springer Verlag, Berlin, Heidelberg, New York, 1992.
Stephen A. Cook and Bruce M. Kapron. Characterizations of the basic feasible functionals of finite type. In S. Buss and P. Scott, editors, Feasible Mathematics, pages 71–96. Birkhäuser, 1990.
Jean-Yves Girard. Light linear logic. Information and Computation, 143, 1998.
Jean-Yves Girard, Andre Scedrov, and Philipp J. Scott. Bounded linear logic. In S.R. Buss and Ph.J. Scott, editors, Feasible Mathematics, pages 195–209. Birkhäuser, Boston, 1990.
Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunkts. Dialectica, 12:280–287, 1958.
David Hilbert. Über das Unendliche. Mathematische Annalen, 95:161–190, 1925.
Martin Hofmann. Typed lambda calculi for polynomial-time computation. Habilitation thesis, Mathematisches Institut, TU Darmstadt, Germany. Available under www.dcs.ed.ac.uk/home/mxh/habil.ps.gz, 1998.
Daniel Leivant. Intrinsic theories and computational complexity. In Logic and Computational Complexity, International Workshop LCC ’94, Indianapolis D. Leivant, ed., Springer LNCS 960, 1995, p. 177–194.
Daniel Leivant. Predicative recurrence in finite type. In A. Nerode and Y.V. Matiyasevich, editors, Logical Foundations of Computer Science, volume 813 of LNCS, pages 227–239, 1994.
Daniel Leivant and Jean-Yves Marion. Ramified recurrence and computational complexity IV: Predicative functionals and poly-space. To appear: Information and Computation.
Daniel Leivant and Jean-Yves Marion. Lambda calculus characterization of poly-time. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, pages 274–288. LNCS Vol. 664, 1993.
Harold Simmons. The realm of primitive recursion. Archive for Mathematical Logic, 27:177–188, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Schwichtenberg, H., Bellantoni, S.J. (2002). Feasible Computation with Higher Types. In: Schwichtenberg, H., Steinbrüggen, R. (eds) Proof and System-Reliability. NATO Science Series, vol 62. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-0413-8_13
Download citation
DOI: https://doi.org/10.1007/978-94-010-0413-8_13
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-0608-1
Online ISBN: 978-94-010-0413-8
eBook Packages: Springer Book Archive