Arnold Beckmann
The Journal of Symbolic Logic Vol. 66, No. 3, pp. 1277-1285
Publication year: 2001

We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ – calculus with β -, ξ – and η – conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.