Weak Normalization of Beta-Reduction on typable lambda-terms

58 Views Asked by At

I have to directly show weak normalization of the β-reduction on typable λ-terms, without showing (a property that entails) strong normalization.

Hint: an idea analogous to that for the cut elimination procedure in the book (First-Order Logic and Automated Theorem Proving, by Melvin Fitting) works, judiciously choosing a β-reduction step among the possible ones and showing that that decreases some measure.