zbMATH — the first resource for mathematics

Stratified polymorphism and primitive recursion. (English) Zbl 0935.03024
Summary: 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 [D. Leivant, Inf. Comput. 93, No. 1, 93-113 (1991; Zbl 0799.68041)] that when type abstraction in that calculus is stratified into levels, the definable numeric functions are precisely the super-elementary functions (level \({\mathcal E}_4\) in the Grzegorczyk hierarchy). We define here a second-order lambda calculus in which type abstraction is stratified to levels up to \(\omega^\omega\), 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 \(<\omega^\ell\) are precisely Grzegorczyk’s class \({\mathcal E}_{\ell+3}\) \((\ell\geq 1)\). This generalizes Leivant’s result [loc. cit.], where this is proved for \(\ell= 1\). Thus, the numeric functions definable in our calculus are precisely the primitive recursive functions.

03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
03B70 Logic in computer science
03D20 Recursive functions and relations, subrecursive hierarchies
Full Text: DOI