Finitely stratified polymorphism
journal contributionposted on 01.11.1996, 00:00 by Daniel Leivant
Abstract: "We consider predicative type-abstraction disciplines based on type quantification with finitely stratified levels. The main technical result is that the functions representable in the finitely stratified polymorphic [lambda]-calculus are precisely the super-elementary functions, i.e. the class E in Grzegorczyk's subrecursive hierarchy. This implies that there is no super-elementary bound on the length of optimal normalization sequences, and that the equality problem for finitely stratified polymorphic [lambda]-expressions is not super-elementary. We also observe that finitely stratified polmorphism augmented with type recursion admits functional algorithms that are not typable in the full second order [lambda]-calculus."