Exact bounds for lengths of reductions in typed λ-calculus
Arnold Beckmann · Journal of Symbolic Logic · 2001
Abstract 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.