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.

#### Definition

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$.

#### Proof

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$

##### References

An Introduction to Logical Relations, Lau Skorstengaard

Types and Programming Languages, Chapter 12, Benjamin C. Pierce