Strong Normalization of STLC
Simply Typed λ-Calculus (STLC) has a nice property called strong normalization, which states that every term in STLC can be normalized to normal form in finite steps. In other words, every program in STLC must terminates.
Theorem (Strong Normalization): If \vdash e : \tau, then \exists v . e \mapsto^{*} v.
If we try to prove the strong normalization theorem by induction on the type derivations, then we will find that for the case of application e_1 ~ e_2, even we have inductive hypothesis on e_1 and e_2, but we don’t have any inductive hypothesis on the value of evaluating e_1, which has form \lambda x . e. In other words, we don’t know anything about the function body e. Therefore the proof cannot be proceeded.
We need to use a proof technique logical relation to show strong normalization.
1 Definition
Using logical relation, the definition of strong normalization for base types and function types can be stated as follows:
Definition (SN): SN_B(e) \text{ iff } \vdash e : B \wedge e \Downarrow \text{, where } B \text{ is some base type}
SN_{\tau_1 \rightarrow \tau_2}(e) \text{ iff } \vdash e : \tau_1 \rightarrow \tau_2 \wedge e \Downarrow \wedge \forall e{}’.SN_{\tau_1} (e{}’) \Rightarrow SN_{\tau_2}(e~e{}’)
We use e \Downarrow to denote \exists v such that e \rightarrow^* v.
2 Proof
The idea of proving strong normalization is to show two things:
\vdash e : T \Rightarrow SN_T(e)
SN_T(e) \Rightarrow e \Downarrow
The first one states that a well-typed term is in the SN relation. The second one states that a term in SN relation can be normalized to some value. Showing (2) can be immediately obtained by the definition of SN. To prove (2), we need firstly establish two lemmas.
Lemma (SN Preserved): If e : T and e \mapsto e{}’, then SN_T(e) if and only if SN_T(e{}’).
Proof: By induction on the type structure of T. □
Lemma (Substitution): If x_1 : T_1,\dots,x_n : T_n \vdash e : T and values v_i have type T_i with SN_{T_i}(v_i), then SN_T(e[x_i \mapsto v_i]).
Proof: By induction on the type derivations of \Gamma \vdash e : T. There are three cases:
\frac {\Gamma(x) = T}{\Gamma \vdash x : T}: Immediately hold.
\frac {\Gamma \vdash e1 : \tau_1 \rightarrow \tau_2 ~~~~ \Gamma \vdash e2 : \tau_1} {\Gamma \vdash e1~e2 : \tau_2} By the inductive hypothesis, we have SN_{\tau_1 \to \tau_2}(e_1 [ x_i \mapsto v_i ]). By the definition of SN_{\tau_1 \to \tau2}, we can instantiate e{}’ with e_2, and obtain SN_{\tau_2}(e_1 ~ e_2).
\frac {\Gamma, x:\tau_1 \vdash e : \tau_2} {\Gamma \vdash \lambda x : \tau_1 . e : \tau_1 \rightarrow \tau_2} Since \lambda x : \tau_1 . e is already a value, so \lambda x : \tau_1 . e [x_i \mapsto v_i] \Downarrow is trivial. Then, we need to show that \forall e{}’ . SN_{\tau_1}(e{}’) \Rightarrow SN_{\tau_2}((\lambda x : \tau_1 . e[x_i \mapsto v_i]) ~ e{}’). Assume that e{}’ is given and SN_{\tau_1}(e{}’). Then by the definition of SN, we know that e{}’ \Downarrow v{}’ where v{}’ is some value. By lemma (SN Preserved), we can conclude that SN_{\tau_1}(v{}’). Now by the inductive hypothesis, after substitution the function body expression is strongly normalized: SN_{\tau_2}(e[x_i \mapsto v_i][x \mapsto v{}’]).
We can also obtain the expression before the substituion: (\lambda x : \tau_1 . e[x_i \mapsto v_i]) ~ e{}’ \mapsto^* e[x_i \mapsto v_i][x \mapsto v{}’]
By using the lemma that SN is preserved when running backward, we can conclude that SN_{\tau_2}((\lambda x : \tau_1 . e[x_i \mapsto v_i]) ~ e{}’). □
Theorem (Strong Normalization): If \vdash e : \tau, then \exists v. e \mapsto^{*} v.
Proof: By lemma (Substitution), we show (1), i.e., SN_{\tau}(e) with some substituions; then by (2), we have e \Downarrow. □