The finitely generated types of the λ-calculus

Abstract

We answer a question raised by Richard Statman (cf. [8]) concerning the simply typed λ-calculus (having o as only ground type): Is it possible to generate from a finite set of combinators all the closed terms of a given type ? (By combinators we mean closed λ-terms of any types). Let us call complexity of a λ-term t the least number of distinct variables required for its writing up to α-equivalence. We prove here that a type T can be generated from a finite set of combinators iff there is a constant bounding the complexity of every closed normal λ-term of type T. The types of rank ≤ 2 and the types A1→(A2→: : : (A n→o)) such that for all i = 1; : : : ; n: Ai = o, Ai = o→o or Ai = (o→(o→: : : (o→o))) →o, are thus the only inhabited finitely generated types. © Springer-Verlag Berlin Heidelberg 2001.