Strong Normalization of Simply Typed Lambda Calculus

  From the (pure) \lambda_{\rightarrow}'s perspective(and only from its perspective since this theorem does not extend to the real world programming languages for most of them supports recursion function and recursive types thus makes the encoding of non-terminate programs become possible), we want to prove that every typable term is normalizable(strong normalization, for accuracy, where by "strong" means every term eventually halts after finite step of reductions. Weak Normalization, in contrast, means there exist a derivation that will halts in finite steps.), which means that any evaluation on them is guaranteed to halt (evaluates to normal form) in finite steps.

Definition(Termination):

e\Darr\ \stackrel{\text{def}}{=}\ \exist v.\ e\rightarrow^\ast v\\
e\Darr v\ \stackrel{\text{def}}{=}\ e\rightarrow^\ast v

where v stands for normal form(value)

Definition(Normalization):

\begin{aligned}
1. R_{\tau}(t)\iff \vdash t:\tau\Darr\text{, where } \tau\text{ is of the unique base type } \tt A\\
2. R_{\tau_1\rightarrow\tau_2}(t)\iff\vdash t:\tau_1\rightarrow\tau_2\ \land\vdash t\Darr\land\ \forall s.R_{\tau_1}(s)\implies R_{\tau_2}(t\ s)
\end{aligned}

Proof

  We need to prove both (1): \forall t\in R_{\tau(t)}.(t\Darr) and (2): \vdash t:\tau\implies R_{\tau}(t), i.e., every R_{\tau} is normalizable and every typable t:\tau is in some R_{\tau}.
  The proof for (1) is immediate from the definition of R. The following contents focusing on proving (2).

Lemma(Termination)

  If t\rightarrow t', then t halts iff t' halts.

Subproof. The result is immediate. ∎

Lemma(Preservation)

  If t\rightarrow t', then R_{\tau}(t)\iff R_{\tau}(t')

Subproof. By induction on the structure of \tau

  1. If \tau = \tt A then the the result is immediate.
  2. If \tau=\tau_1\rightarrow\tau_2, We have:
    1. From definition we know R_{\tau}(t), \forall s:\tau_1. R_{\tau_1}(s), and R_{\tau_2}(t\ s), since t\ s\rightarrow t'\ s, we have R_{\tau_2}(t'\ s) from induction hypothesis, from \Darr_\text{def} we can conclude that R_{\tau}(t)\implies R_{\tau}(t'). ∎
    2. From R_{\tau}(t') we have \forall s:\tau_1.R_{\tau_1}(t'\ s), since t\ s\rightarrow t'\ s, from induction hypothesis we have R_{\tau_2}(t\ s), combined with the fact that R_{\tau_1}(s) and Termination Lemma we have R_{\tau}(t')\implies R_{\tau}(t). ∎

Lemma(Substitution)

  If \bigcup\limits_{i=1}^{n}x_n:\tau_n\vdash t:\tau with a set of values \{v_i:\tau_i\vert 1\leqslant i\leqslant n \} where \forall i\leqslant n.R_{\tau_i}(v_i), then R_{\tau}([x_1\mapsto v_1],...,[x_n\mapsto v_n]t)

Subproof. By induction on the derivation of t

  1. Case \cfrac{x:\tau\in\Gamma}{\Gamma\vdash x:\tau}: The result is immediate. ∎
  2. Case \cfrac{\Gamma,x:\tau_1\vdash t:\tau_2}{\vdash \lambda x:\tau_1.t:\tau_1\rightarrow \tau_2}:

    Definition. Let [x_i \mapsto_{i=1}^n v_i]\ t \stackrel{\text{def}}{=} [x_1\mapsto v_1],...,[x_n\mapsto v_n]\ t

    Suppose that \tau=\tau'\rightarrow\tau'', t=\lambda x:\tau'.\ k, and from Inversion Lemma we know that \bigcup\limits_{i=1}^{n}x_n:\tau_n,x:\tau'\vdash k:\tau'', what left is to prove i. t\Darr. ii. R_{\tau'}(s)\implies R_{\tau''}([x_i \mapsto_{i=1}^n v_i]\ t\ s).

    1. Under the call-by-value strategy, an abstraction is itself a value, thus t\Darr is trivial.
    2. From (1) we know that k\Darr v, and by Preservation Lemma we have R_{\tau'}(v), by induction hypothesis it is clear that:
      R_{\tau''}([x\mapsto v][x_i \mapsto_{i=1}^n v_i]\ k)

      however, since:

      \begin{aligned}
      t\ s &= (\lambda.x:\tau'.\ [x_i \mapsto_{i=1}^n v_i]\ k)\ s \\ &\rightarrow[x\mapsto v][x_i \mapsto_{i=1}^n v_i]\ k
      \end{aligned}

      by Preservation Lemma we get:

      R_{\tau''}((\lambda.x:\tau'.\ [x_i \mapsto_{i=1}^n v_i]\ k)\ s)

      which is equals to

      R_{\tau''}([x_i \mapsto_{i=1}^n v_i](\lambda.x:\tau'.\ k)\ s)

      now, combined with the fact that R_{\tau'}(s), by the definition of R we get:

      R_{\tau'\rightarrow\tau''}([x_i \mapsto_{i=1}^n v_i](\lambda.x:\tau'.\ k))
      \begin{aligned}
      \tag*{∎}
      \end{aligned}
  3. Case \cfrac{\Gamma\vdash t_1:\tau_1\rightarrow \tau_2,t_2:\tau_1}{\Gamma\vdash t_1\ t_2:\tau_2}: Let t=t_1\ t_2 where t_1:\tau'\rightarrow \tau'' and t_2:\tau', from induction hypothesis we can obtain that R_{\tau''}([x_i \mapsto_{i=1}^n v_i]\ t_1\ [x_i \mapsto_{i=1}^n v_i]\ t_2), which implies R_{\tau''}([x_i \mapsto_{i=1}^n v_i](t_1\ t_2)). ∎

Normalization Theorem

Theorem (Strong Normalization): Every typable term is normalizable.

Proof: By handling each possible case of a term t
1. Case \cfrac{x:\tau\in\Gamma}{\Gamma\vdash x:\tau}: Since t it self is already a normal form, this case is trivial.
2. Case \cfrac{\Gamma,x:\tau_1\vdash t:\tau_2}{\vdash \lambda x:\tau_1.t:\tau_1\rightarrow \tau_2}: Since t itself is already a normal form, this case is trivial.
3. Case \cfrac{\Gamma\vdash t_1:\tau_1\rightarrow \tau_2,t_2:\tau_1}{\Gamma\vdash t_1\ t_2:\tau_2}: By apply Subsitution Lemma until it reaches a normal form, since every normal form is already normalizing, so t is normalizable.

The proof is hereby completed. ∎

(呜呜呜,这是一整个通宵(6个小时)的忙活结果,我好笨)


We Choose to Go to the Moon