Normalization in the Simply-Typed λ-calculus

Preview

I’ll present the normalization theorem in detail, because that seems to be something we all glanced over when we read TaPL!

Resources

• See Ch. 6 of this book

Summary

Theorem: If ⋅ ⊢ e : τ, then e ↦⋆ v, where v is a value.

This doesn’t go through. We need a stronger induction hypothesis.

Define Rτ(e) by induction on τ:

R_{unit} ⟺ e terminates
R_{τ1→t2} ⟺ ∀e2:τ1, Rτ1(e2) ⟹ Rτ2(e e2)

Then we can use the stronger property to prove normalization!

Theorem: Rτ(e) ⟹ e terminates.

Theorem: If ⋅ ⊢ e : τ, then Rτ(e).

Recap: we made a relation that helped us to express the logical structure of the elimination forms of a type—a lambda is logically an implication, and the Rτ relation in the arrow type case is essentially a form of modus ponens.