Abstract
We present a version of Gödel’s system T in which the types are ramified in the style of Leivant and a system of dependent typing is introduced. The dependent typing allows the definition of recursively defined types, where the recursion is controlled by ramification; these recursively defined types in turn allow the definition of functions by repeated iteration. We then analyze a subsystem of the full system and show that it defines exactly the primitive recursive functions. This result supports the view that when data use is regulated (for example, by ramification), standard function constructions are intimately connected with standard type-theoretic constructions.
The author would like to thank Daniel Leivant and the referees for several helpful suggestions. The type derivations are typeset with Makoto Tatsuta’s proof.sty package, version 3.0. The author was partially supported by National Science Foundation grant number DMS-9983726.
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
J. Avigad. Predicative functionals and an interpretation of \( \widehat{ID}_{ < \omega } \) . Ann. Pure Appl. Logic, 92(1):1–34, 1998.
J. Avigad and S. Feferman. Gödel’s functional (“Dialectica”) interpretation. In S. Buss, editor, Handbook of Proof Theory, pages 337–405. North-Holland, Amsterdam, 1998.
H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Vol. 2, pages 117–309. Oxford University Press, Oxford, 1992.
S. Bellantoni. Predicative recursion and the polytime hierarchy. In Feasible Mathematics II (Ithaca, NY, 1992), pages 15–29. Birkhäuser Boston, Boston, MA, 1995.
S. Bellantoni and S. Cook. A new recursion-theoretic characterization of the polytime functions. Comput. Complexity, 2(2):97–110, 1992.
S. Bellantoni, K.-H. Niggl, and H. Schwichtenberg. Higher type recursion, ramification and polynomial time. Ann. Pure Appl. Logic, 104(1–3):17–30, 2000.
E. Covino, G. Pani, and S. Caporaso. Extending the implicit computational complexity approach to the sub-elementary time-space classes. In Algorithms and Complexity (Rome, 2000), pages 239–252. Springer, Berlin, 2000.
N. Danner and C. Pollett. Minimization and the class NPMV. In preparation.
K. Gödel. über eine bisher noch nicht benützte Erweiterung des niten Standpunktes. Dialectica, 12:280–287, 1958.
M. Hofmann. A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. In Computer Science Logic (Aarhus, 1997), pages 275–294. Springer, Berlin, 1998.
M. Hofmann. Safe recursion with higher types and BCK-algebra. Ann. Pure Appl. Logic, 104(1–3):113–166, 2000.
D. Leivant. Ramified recurrence and computational complexity I: Word recurrence and poly-time. In Feasible Mathematics II (Ithaca, NY, 1992), pages 320–343. Birkhäuser Boston, Boston, MA, 1995.
D. Leivant. Ramified recurrence and computational complexity III: Higher type recurrence and elementary complexity. Ann. Pure Appl. Logic, 96(1–3):209–229, 1999. Festschrift on the occasion of Professor Rohit Parikh’s 60th birthday.
D. Leivant and J.-Y. Marion. Ramified recurrence and computational complexity II: Substitution and poly-space. In Computer Science Logic (Kazimierz, 1994), pages 486–500. Springer, Berlin, 1995.
N. Nelson. Primitive recursive functionals with dependent types. In Mathematical Foundations of Programming Semantics (Pittsburgh, PA, 1991), pages 125–143. Springer, Berlin, 1992.
H. E. Rose. Subrecursion: functions and hierarchies. Number 9 in Oxford Logic Guides. Oxford University Press, Oxford, 1984.
A. L. Selman. Much ado about functions. In Eleventh IEEE Conference on Computational Complexity, pages 198–212. 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danner, N. (2001). Ramied Recurrence with Dependent Types. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_11
Download citation
DOI: https://doi.org/10.1007/3-540-45413-6_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41960-0
Online ISBN: 978-3-540-45413-7
eBook Packages: Springer Book Archive