Abstract

We present a new proof for the standardization theorem in $\lambda$-calculus, which is largely built upon a structural induction on $\lambda$-terms. We then extract some bounds for the number of $\beta$-reduction steps in the standard $\beta$-reduction sequence obtained from transforming a given $\beta$-reduction sequence, sharpening the standardization theorem. As an application, we establish a super exponential bound for the lengths of $\beta$-reduction sequences from any given simply typed $\lambda$-terms.