### arnold beckmann's pages

## Exact bounds for lengths of reductions in typed
λ - calculus

**File:** PDF-File

**Author:** Arnold Beckmann

**Title:** Exact bounds for lengths of reductions in typed
λ - calculus

**Journal:** JSL 2001, **66**(3): 1277-1285

**Stable URL:** http://www.jstor.org/stable/2695106

**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.