Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-08T15:06:01.682Z Has data issue: false hasContentIssue false

Stratified polymorphism and primitive recursion

Published online by Cambridge University Press:  01 August 1999

NORMAN DANNER
Affiliation:
Indiana University, Bloomington, IN 47405, U.S.A. Email: ndanner@member.ams.org
DANIEL LEIVANT
Affiliation:
Indiana University, Bloomington, IN 47405, U.S.A. Email: leivant@cs.indiana.edu
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Natural restrictions on the syntax of the second-order (i.e., polymorphic) lambda calculus are of interest for programming language theory. One of the authors showed in Leivant (1991) that when type abstraction in that calculus is stratified into levels, the definable numeric functions are precisely the super-elementary functions (level [Escr]4 in the Grzegorczyk Hierarchy). We define here a second-order lambda calculus in which type abstraction is stratified to levels up to ωω, an ordinal that permits highly uniform (and finite) type inference rules. Referring to this system, we show that the numeric functions definable in the calculus using ranks < ω[lscr] are precisely Grzegorczyk's class [Escr][lscr]+3 ([lscr] [ges ] 1).This generalizes Leivant (1991), where this is proved for [lscr] = 1. Thus, the numeric functions definable in our calculus are precisely the primitive recursive functions.

Information

Type
Research Article
Copyright
© 1999 Cambridge University Press