Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-22T14:38:08.375Z Has data issue: false hasContentIssue false
  • English
  • Français

Tiering as a Recursion Technique

Published online by Cambridge University Press:  15 January 2014

Harold Simmons
Harold Simmons*
Affiliation:
Mathematical Foundations Group, The University of Manchester, Oxford Road, Manchester M13 9PL, England. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

I survey the syntactic technique of tiering which can be used to restrict the power of a recursion scheme. I show how various results can be obtained entirely proof theoretically without the use of a model of computation.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 11 , Issue 3 , September 2005 , pp. 321 - 350
Copyright
Copyright © Association for Symbolic Logic 2005

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Beckmann, A. and Weiermann, A., Characterizing the elementary recursive functions by a fragment of Gödel's T, Archive for Mathematical Logic, vol. 39 (2000), pp. 475–491.Google Scholar
[2] Bellantoni, S., Predicative recursion and computational complexity, Ph.D. thesis, University of Toronto, 1992.Google Scholar
[3] Bellantoni, S., Predicative recursion and the polytime hierarchy, In Clote and Remmel [6], pp. 15–29.Google Scholar
[4] Bellantoni, S. and Cook, S., A new recursion-theoretic characterization of the poly-time functions, Computational complexity, vol. 2 (1992), pp. 97–110.Google Scholar
[5] Bellantoni, S. J. and Hofmann, M., A new ‘feasible’ arithmetic, The Journal of Symbolic Logic, vol. 67 (2002), pp. 104–116.Google Scholar
[6] Clote, P. and Remmel, J. (editors), Feasible mathematics II, Perspectives in Computer Science, Birkäuser, Boston, New York, 1995.Google Scholar
[7] Hofmann, M., A mixed modal/linear lambda calculus with application to Bellantoni-Cook safe recursion, CSL 97, Lecture Notes in Computer Science, vol. 1414, Springer-Verlag, pp. 275–295.Google Scholar
[8] Hofmann, M., Linear types and non-size-increasing polynomial time computation, Proceedings of the Symposium of the 14th LICS, CS Press, 1999.Google Scholar
[9] Hofmann, M., Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol. 104 (2000), pp. 113–166.CrossRefGoogle Scholar
[10] Leivant, D., Finitely stratified polymorphism, Information and Computation, vol. 93 (1991), pp. 93–113.Google Scholar
[11] Leivant, D., Ramified recurrence and computational complexity I: Word recurrence and poly-time, In Clote and Remmel [6], pp. 320–343.Google Scholar
[12] Leivant, D., Ramified recurrence and computational complexity III: Higher type recurrence and elementary complexity, Annals of Pure and Applied Logic, vol. 96 (1999), pp. 209–229.CrossRefGoogle Scholar
[13] Leivant, D. and Marion, J. Y., A λ-calculus characterization of poly-time, Typedlambda calculi and applications (Bezem, M. and Groote, J. F., editors), Lecture Notes in Computer Science, vol. 664, Springer-Verlag, 1993, pp. 274–288.Google Scholar
[14] Leivant, D. and Marion, J. Y., Lambda calculus characterization of poly-time, Fundamenta Informatica, vol. 19 (1993), pp. 167–184.Google Scholar
[15] Murawski, A. S. and Ong, C.-H. L., Can safe recursion be interpreted in light linear logic?, paper presented at ICC '00, 2000.Google Scholar
[16] Schwichtenberg, H., Definierbare Funktionen im Lambda-Kalkül mit Typen, Archiv für Logik und die Grundlagen der Mathematik, vol. 17 (1976), pp. 113–114.Google Scholar
[17] Simmons, H., The realm ofprimitive recursion, Archive for Mathematical Logic, vol. 27 (1988), pp. 177–188.Google Scholar
[18] Simmons, H., Fiering for natural number systems, http://www.cs.man.ac.uk/~hsimmons/DOCUMENTS/papersandnotes.html.Google Scholar