強正規化定理

要点：一歩先が有限個なので、長さに上限がなければ、上限のない一歩先を次々に選んで無限の列が作れる。

3 条件をまとめて $A$ についての帰納法で示す。
基本型 $o$。 (CR1) は $\mathrm{RED}_o=\mathrm{SN}$ なので自明である。(CR2) は lem-sn-nu の 3、(CR3) は同じ補題の 4 である（(CR3) では中立であることを使わない）。
関数型 $A\to B$。 $A$ と $B$ について 3 条件が成り立つと仮定する。(CR1) は変数 $x\in\mathrm{RED}_A$ に当てた $Mx$ の強正規化から、(CR2) は $MN\to M'N$ から従う。

• $M'N$（$M\to M'$）。仮定により $M'\in\mathrm{RED}_{A\to B}$ なので $M'N\in\mathrm{RED}_B$ である。
• $MN'$（$N\to N'$）。$A$ についての (CR2) により $N'\in\mathrm{RED}_A$ であり、lem-sn-nu の 3 により $\nu(N')<\nu(N)$ なので、帰納法の仮定から $MN'\in\mathrm{RED}_B$ である。
  $MN$ は適用なので中立であり、一歩先がすべて $\mathrm{RED}_B$ に属するから、$B$ についての (CR3) により $MN\in\mathrm{RED}_B$ である。$\square$

1：$P\to P'$ を生成する規則についての帰納法である。$P$ 自身が縮約される β 基 $(\lambda y{:}C.\,R)S$ で $P'=R[S/y]$ のとき、$y\ne x$、$y\notin\mathrm{FV}(N)$ に名前を選ぶと
$$ P[N/x]=(\lambda y{:}C.\,R[N/x])\,S[N/x]\to R[N/x]\,[\,S[N/x]/y\,]=R[S/y][N/x]=P'[N/x] $$
である。等号のうち 2 つ目は λ計算 の記事の補題「代入補題」で、その証明は型の注釈 $C$ があっても変わらない。

$x,A,B$ を固定し、項 $P$ が「すべての $N\in\mathrm{RED}_A$ について $P[N/x]\in\mathrm{RED}_B$」を満たすことを $(\mathrm H_P)$ と書く。$(\mathrm H_P)$ を満たす $P$ について、lem-sn-cr の最後の主張により $x\in\mathrm{RED}_A$ なので $P=P[x/x]\in\mathrm{RED}_B$ であり、(CR1) により $P\in\mathrm{SN}$ である。また $N\in\mathrm{RED}_A$ なら (CR1) により $N\in\mathrm{SN}$ である。
$(\mathrm H_P)$ を満たす $P$ と $N\in\mathrm{RED}_A$ について $(\lambda x{:}A.\,P)N\in\mathrm{RED}_B$ となることを、$\nu(P)+\nu(N)$ についての帰納法で示す。$(\lambda x{:}A.\,P)N$ の β 基は、それ自身と、$P$ の中のものと、$N$ の中のものだけなので、一歩先は次の 3 種類である。

• $P[N/x]$。$(\mathrm H_P)$ により $\mathrm{RED}_B$ に属する。
• $(\lambda x{:}A.\,P')N$（$P\to P'$）。任意の $N''\in\mathrm{RED}_A$ について、lem-sn-subst の 1 により $P[N''/x]\to P'[N''/x]$ であり、$P[N''/x]\in\mathrm{RED}_B$ なので (CR2) により $P'[N''/x]\in\mathrm{RED}_B$ である。よって $P'$ も $(\mathrm H_{P'})$ を満たし、lem-sn-nu の 3 により $\nu(P')<\nu(P)$ なので、帰納法の仮定からこの項は $\mathrm{RED}_B$ に属する。
• $(\lambda x{:}A.\,P)N'$（$N\to N'$）。(CR2) により $N'\in\mathrm{RED}_A$、$\nu(N')<\nu(N)$ なので、帰納法の仮定から $\mathrm{RED}_B$ に属する。
  $(\lambda x{:}A.\,P)N$ は適用なので中立であり、一歩先がすべて $\mathrm{RED}_B$ に属するから、(CR3) により $\mathrm{RED}_B$ に属する。$N\in\mathrm{RED}_A$ は任意なので、定義から $\lambda x{:}A.\,P\in\mathrm{RED}_{A\to B}$ である。$\square$

導出の最後の規則で場合を分ける。$\sigma:=[\vec N/\vec x]$ と略記する。

• (var)：$M=x_i$、$A=A_i$ なら、$M\sigma=N_i\in\mathrm{RED}_{A_i}$ である。
• (app)：$M=PQ$ で $\Gamma\vdash P:B\to A$、$\Gamma\vdash Q:B$ なら、帰納法の仮定により $P\sigma\in\mathrm{RED}_{B\to A}$、$Q\sigma\in\mathrm{RED}_B$ なので、定義から $M\sigma=(P\sigma)(Q\sigma)\in\mathrm{RED}_A$ である。
• (abs)：$M=\lambda y{:}B.\,P$、$A=B\to C$ で $\Gamma,y{:}B\vdash P:C$ とする。$y$ は $\Gamma$ に現れず、$N_1,\dots,N_n$ に自由に現れないように選んでおく。任意の $N\in\mathrm{RED}_B$ について、文脈 $\Gamma,y{:}B$ と項 $N_1,\dots,N_n,N$ に帰納法の仮定を使うと $P[\vec N/\vec x,\,N/y]\in\mathrm{RED}_C$ であり、上の等式により左辺は $(P\sigma)[N/y]$ に等しい。よって lem-sn-abs により $\lambda y{:}B.\,P\sigma\in\mathrm{RED}_{B\to C}$ であり、これは $M\sigma$ に等しい。$\square$

$\Gamma=\{x_1{:}A_1,\dots,x_n{:}A_n\}$ とする。各 $x_i$ は中立な正規形なので、lem-sn-cr の最後の主張により $x_i\in\mathrm{RED}_{A_i}$ である。thm-sn-adequacy を $N_i:=x_i$ に使うと $M=M[\vec x/\vec x]\in\mathrm{RED}_A$ であり、(CR1) により $M\in\mathrm{SN}$ である。簡約の列が止まった項には一歩先がないので、β 基を含まず正規形である。$\square$

$N_1,N_2$ が $M$ の β 基の出現 $r_1,r_2$ を縮約したものとし、$M$ の組み立てについての帰納法で示す。$r_1=r_2$ なら $N_1=N_2$ である。$r_1,r_2$ がともに $M$ の真部分にあるとき、同じ成分の中にあれば帰納法の仮定を使い、$M=PQ$ で一方が $P$、他方が $Q$ の中にあれば、両方を縮約した項が共通の簡約先になる。
残るのは、一方、たとえば $r_1$ が $M$ 自身で、$M=(\lambda x{:}A.\,P)Q$、$N_1=P[Q/x]$ の場合である。$r_2$ が $P$ の中にあり $P\to P'$ なら、$N_2=(\lambda x{:}A.\,P')Q\to P'[Q/x]$ であり、lem-sn-subst の 1 により $N_1\to P'[Q/x]$ である。$r_2$ が $Q$ の中にあり $Q\to Q'$ なら、$N_2=(\lambda x{:}A.\,P)Q'\to P[Q'/x]$ であり、lem-sn-subst の 2 により $N_1\to^*P[Q'/x]$ である。$\lambda x{:}A.\,P$ 自身は β 基でないので、ほかの場合はない。$\square$

$\nu(M)$ についての帰納法で示す。$M\to^*N_1$、$M\to^*N_2$ のどちらかが $0$ 回の簡約なら、もう一方の終点を $L$ にとればよい。そうでなければ $M\to M_1\to^*N_1$、$M\to M_2\to^*N_2$ と書ける。prop-sn-local により $M_1\to^*L_0$、$M_2\to^*L_0$ となる $L_0$ がある。
$M_1\in X$ で lem-sn-nu の 3 により $\nu(M_1)<\nu(M)$ なので、帰納法の仮定を $M_1\to^*N_1$、$M_1\to^*L_0$ に使うと、$N_1\to^*L_1$、$L_0\to^*L_1$ となる $L_1$ がある。次に $M_2\in X$、$\nu(M_2)<\nu(M)$ で、$M_2\to^*L_0\to^*L_1$ と $M_2\to^*N_2$ があるから、帰納法の仮定により $L_1\to^*L$、$N_2\to^*L$ となる $L$ がある。$N_1\to^*L_1\to^*L$ なので、この $L$ が求めるものである。$\square$

$X$ を、ある文脈で型付け可能な項の全体とする。型理論 の記事の定理「主部簡約」により $X$ は簡約で閉じており、thm-sn-main により $X$ の項はすべて強正規化可能である。
1：$N_1,N_2$ が $M$ の正規形なら、thm-sn-confluence により $N_1\to^*L$、$N_2\to^*L$ となる $L$ があるが、正規形からの簡約は $0$ 回しかないので $N_1=L=N_2$ である。簡約の列は thm-sn-main により正規形で止まり、それは $M$ の正規形なので $\mathrm{nf}(M)$ である。
2：$M\to^*L$、$M'\to^*L$ なら、$L\in X$ なので $L\to^*\mathrm{nf}(L)$ であり、$\mathrm{nf}(L)$ は $M$ と $M'$ の両方の正規形だから、1 により $\mathrm{nf}(M)=\mathrm{nf}(L)=\mathrm{nf}(M')$ である。逆に $\mathrm{nf}(M)=\mathrm{nf}(M')$ ならそれを $L$ にとればよい。正規形は、1 により β 基を任意に選んで縮約し続ければ有限回で得られる。$\square$