Notes on Strong Normalization of STLC

Simply Typed $\lambda$-Calculus (STLC) has a nice property called strong normalization which states that every term in STLC can be normalized in finite steps.

$ Theorem (Strong~Normalization): \text{if }\vdash e : \tau, \text{ then } \exists v. e \mapsto^{*} v$

If someone tries to prove it by induction on type derivations, then he will find that for the case function applications like (e1 e2), even we have induction hypothesis on e1 and e2, but we don’t have any induction hypothesis on the value of e1 which has form λx.e. In other words, we don’t know anything about e (the function body of e1). Therefore the proof fails.

A proof technique Logical Relations is introduced to solve this problem. The rest of this post is a brief note on prooving strong normalization of call-by-value STLC.


The definition of strong normalization (in the way of logical relations) is stated as follows:

$$ 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’) $$

Note on notation: $e \Downarrow$ is defined as $\exists v . e \rightarrow^* v$.


The proof idea is to show two things:

(1) $ \vdash e : T \Rightarrow SN_T(e) $

(2) $ 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 (1) we firstly establish two lemmas.

$ Lemma (SN~Preserved):
\text{if } e : T,\text{ and }e \mapsto e’, \text{ then }SN_T(e) \text{ iff } SN_T(e’) $
$Proof:$ By induction on type structure of $T$. $\square$

In this lemma, we claim that the if $e$ is a well-typed term and can be reduced one step to $e’$ then SN property is preserved on two directions: $SN_T(e)$ implies $SN_T(e’)$ and $SN_T(e’)$ also implies $SN_T(e)$.

The second lemma is a generalized proposition of (1):

$ Lemma (Substitution): \text{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 type derivations of $\Gamma \vdash e : T$.

$Case \frac {\Gamma(x) = T}{\Gamma \vdash x : T}:$ Immediate.

$Case \frac {\Gamma \vdash e1 : \tau_1 \rightarrow \tau_2 ~~~~ \Gamma \vdash e2 : \tau_1} {\Gamma \vdash e1~e2 : \tau_2}:$ By induction hypothesis, we have $SN_{\tau_1 \rightarrow \tau_2}(e1[x_i \mapsto v_i])$ and $SN_{\tau_1}(e2[x_i \mapsto v_i])$. By definition of $SN_{\tau_1 \rightarrow \tau_2}$, we can instantiate $e’$ with $e2$, and obtain $SN_{\tau_2}(e1~e2)$.

$Case \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 $\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 definition of $SN$, we know that $e’ \Downarrow v’$ where $v’$ is some value. By lemma (SN Preserved), we can conclude $SN_{\tau_1}(v’)$.
Now by induction hypothesis, after substituion the function body expression is $SN$:
$$ 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’)$. $\square$

$ Theorem (Strong~Normalization): \text{if }\vdash e : \tau, \text{ 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$. $\square$


An Introduction to Logical Relations, Lau Skorstengaard
Types and Programming Languages, Chapter 12, Benjamin C. Pierce