単純型付ラムダ計算の弱正規化定理の証明

本記事は Mathlog Advent Calendar の2021/12/15の記事です。2021/12/14は kazuさんがソフトマックス関数と数値微分という記事 を書かれています。

今後執筆予定の記事で確認するがラムダ計算は、抽象化された計算の理論である。
弱正規化定理が意味するのは、型付け可能なラムダ項が表現する関数が計算可能である、ということである。

ラムダ項

ラムダ項 $\lambda$-term を以下で帰納的に定義する。

1. 変数$x_0, x_1, \dots$はラムダ項であり、原子 atom という。
2. $M$と$N$がラムダ項ならば、$(MN)$はラムダ項であり、適用 application という。
3. $M$がラムダ項で$x$が変数ならば$(\lambda x. M)$はラムダ項であり、抽象 abstraction という。

型

ラムダ項$M$が型 type $\tau$を$\Gamma$で持つことを$\Gamma \vdash M \colon \tau$と書き、以下の規則によって
$\Gamma \vdash M \colon \tau$を得られると定義する。このとき、$M$は$\tau$により型づけられているという。

$$\frac{}{\Gamma, x \colon \vdash x \colon \tau}$$
$$\frac{\Gamma, x \colon \sigma \vdash M \colon \tau}{\Gamma \vdash (\lambda x. M) \colon \sigma \to \tau}$$
$$\frac{\Gamma \vdash M \colon \sigma \to \tau; \Gamma\vdash N\colon \sigma}{\Gamma \vdash (MN)\colon \tau}$$

$\beta$-簡約

次の四つの規則から導かれるラムダ項間の関係を$\beta$-簡約 $\beta$-reduction という。

$$\frac{}{(\lambda x.M)N \rhd_1 M[N \leftarrow x]}$$
$$\frac{M \rhd_1 M'}{MN \rhd_1 M'N}, \frac{N \rhd_1 N'}{MN \rhd_1 MN'}, \frac{M \rhd_1 M'}{\lambda x. M \rhd_1 \lambda x. M'}$$

$\beta$-正規形

それ以上$\beta$-簡約できないラムダ項を$\beta$-正規形 $\beta$-normal form と言う。ラムダ項が$\beta$-正規形であるのは、その中に$(\lambda x.M)N$という形の部分を持たないである。
このような部分を$\beta$-可簡約表現 $\beta$-reducible expression という。

弱正規化定理

すべての型付ラムダ項は$\beta$-正規形をもつ。

正規化の戦略

この証明のために特定の戦略で簡約をすることで型のついたラムダ項が$\beta$-正規形になることを示す。
今回は次の戦略を採用する。

• 複雑な順に簡約する;
• 複数の候補があるとき、右から順に簡約する。

実際にこれらはそれぞれ、カリーハワード対応で言うと、いちばん長い局所的ピークから$\beta$-変形していることと証明木の上から順に$\beta$-変形していることに対応する。

いつか述べるが局所的ピークという考え方は、導入規則の適用直後の除去規則の適用という「遠回り」を拾い上げたものである。この「遠回り」に相当するのが可簡約表現であり、したがって、局所的ピークの論理式の長さに対応する、可簡約表現の尺度である次数を定義する。

次数

型$\tau$の次数 degree $d(\tau)$を
つぎのように帰納的に定義する。

1. $d (p) = 0$;
2. $d (\gamma \to \delta) = 1 + \max(d (\gamma) , d (\delta))$

これを用いて$x \colon \delta , P \colon \gamma$なる可簡約表現$\Delta = (\lambda x . P)Q$の次数を$d (\Delta) := d (\gamma \to \delta)$で 定義する。

弱正規化定理の証明

ラムダ項$M$に対して、$d$を$M$に出現する可簡約表現の次数で最大のものと$m$を$d$の次数をもつ可簡約表現の数とする。この$M$に対して、$\Gamma \vdash M$なるとき、 $\Gamma {\vdash}^{d}_{m} M$と表記しよう。

実際にこの戦略による$\beta$-簡約の様子をみてみよう。$M$を$\beta$-正規形でないとし、さらに$M$の部分項のうち次数 $d$ の可簡約表現の中で冒頭の記号が最も右にあるものを $\Delta$とする。

この$\Delta$を簡約して、$M$から$N$を得られたとする。ラムダ項$N$は、一般に$M$より多くの可簡約表現を持つ。
しかし、次数 $d$ である可簡約表現の数は、この簡約により真に減少する。
実際、可簡約表現 $\Delta$ は消え、この簡約により生じる新しい可簡約表現は$\Delta$より真に小さい次数を持つ。このことを確認するのに、可簡約表現の数が増えうるのがつぎの場合のみであることに注意したらよい:

1. 新しい可簡約表現が生じる場合
2. すでに$M$に含まれている可簡約表現がコピーされる場合

前者が起こるのは、抽象でない項$A$が $(AB)$ のかたちで出現し、$A$が$\Delta$にかんする簡約で抽象になるときである。よって、$A = \Delta$の場合についてのみ考える。
なお、$A$が変数、たとえば$x$であるときも新しい可簡約表現がつくられるが、現在の議論では無視してよい。

(1)の場合の最初のパターンは、以下である。
変数$x, y$と項$P, Q$について、その型付けが$x \colon \tau = \gamma \to \delta, y \colon \gamma, P \colon \gamma, Q \colon \delta$であるとき、$\Delta$として、$(\lambda x. \cdots xP \cdots) (\lambda y.Q)$を考える。簡約により$ \cdots (\lambda y.Q）)P \cdots$が新しい可簡約表現として生じる。
この次数は、$d (\tau)$であり、$d$より真に小さい。

つぎに変数$x, y$と項$P, Q$について、その型付けが$x \colon \tau = \gamma \to \delta, y \colon \gamma, P \colon \gamma, Q \colon \delta$であるとき、$\Delta$として$(\lambda xy.Q)P$を考える。
このとき、$d = d (\tau \to \gamma \to \delta)$である。
簡約により生じる新しい可簡約表現は、$\lambda y. Q[ P \leftarrow x ] $であり、その次数は、$d (\tau) < d$である。

最後に変数$x, y$と項$P$について、その型付けが$x \colon \tau = \gamma \to \delta, y \colon \gamma, P \colon \delta$であるとき、$\Delta$として$(\lambda x.x)(\lambda y.P)$を考える。
このとき、$d = d (\tau \to \tau)$である。
いま、$Q \colon \gamma$なる項$Q$が存在し、$\Delta Q\$が\(M$の部分項であるならば、簡約により新しい可簡約表現 $(\lambda y.P)Q$が生じる。
この次数は、$d (\tau)$であり、$d$より真に小さい。

(2))の場合は、$\Delta = (\lambda x.P)Q$とし、$x$が$P$に自由に出現するときを考える。
ただし、$x \colon \gamma, P \colon \delta, Q \colon \gamma$である。
このとき、$d (\Delta) = d (\gamma \to \delta)$である。
この$\Delta$が$M$に出現するとき、$N$は$P[Q \leftarrow x]$を部分項に持つ。よって、$Q$内のコピーが$N$に含まれることになる。
しかし、$\Delta$の選び方により$Q$内のどの可簡約表現もその次数は$d$より真に小さい。

以上の簡約手順を$m, d$の大きさに着目してつぎのふたつの補題を得る。

補題A

$\Gamma \vdash^{d}_{1} M$でかつ$M \rhd_{1 \beta} N$でならば、適当な$n$と$e < d$が存在して、 $\Gamma \vdash^{e}_{n} N$である。

補題B

$m > 1$のとき$\Gamma \vdash^{d}_{m} M$でかつ$m > 1$でかつ$M \rhd_{1 \beta} N$ならば、$m > n \geq 1$なる$n$が存在して$\Gamma \vdash^{d}_{n} N$である。

証明

補題Aと補題Bから$d, m$が簡約により真に減少することから弱正規化定理が従う。

最後に

この記事は参照リンクにもある私が書いた解説、 論理と計算の科学シリーズ「カリーハワード対応」 をもとにしています。
今後気が向いて時間を取れれば関連記事を書かせていただきますが、わかりやすく親切な解説は上記リンクからご購入いただけます。ご購入いただけると私が喜びます。

また、数理論理学と計算機科学関連でいろいろやっていますので、 profileからも確認できる私のwebサイト や twitter 、 researchgate 等々をご覧になっていただけると幸いです。