23.5 Basic Properties

---

23.5 Basic Properties

The fundamental properties of System F are very similar to those of the simply typed lambda-calculus. In particular, the proofs of type preservation and progress are straightforward extensions of the ones we saw in Chapter 9.

23.5.1 Theorem [Preservation]

If Г ⊢ t : T and t → t′, then Г ⊢ t′ : T.

Proof: EXERCISE [RECOMMENDED, ⋆⋆⋆].

23.5.2 Theorem [Progress]

If t is a closed, well-typed term, then either t is a value or else there is some t′ with t → t′.

Proof: EXERCISE [RECOMMENDED, ⋆⋆⋆].

System F also shares with λ_→ the property of normalization-the fact that the evaluation of every well-typed program terminates.^[3] Unlike the type safety theorems above, normalization is quite diffcult to prove (indeed, it is somewhat astonishing that it holds at all, considering that we can code things like sorting functions in the pure language, as we did in Exercise 23.4.12, without resorting to fix). This proof, based on a generalization of the method presented in Chapter 12, was a major achievement of Girard's doctoral thesis (1972; also see Girard, Lafont, and Taylor, 1989). Since then, his proof technique has been analyzed and reworked by many others; see Gallier (1990).

23.5.3 Theorem [Normalization]

Well-typed System F terms are normalizing.

^[3]Indeed, presentations of System F with more permissive operational semantics based on full beta-reduction have the strong normalization property: every reduction path starting from a well-typed term is guaranteed to terminate.

---