λ計算

同義語：ラムダ計算λ-計算lambda calculusλ-calculus

概要

前提知識: 型理論, μ再帰関数, 数学的帰納法

λ計算（lambda calculus）は、関数を作る操作（抽象）と関数を引数に当てる操作（適用）だけで項を組み立て、関数への代入による書き換え（β 簡約）を計算とみなす体系である。Church が 1930 年代の初めに構成的な論理の基礎として考案し、のちに Turing 機械や部分再帰関数と同じ計算可能性を与えることが分かった（OLT26 §41.1、p. 619）。数も真理値も関数として表され、どの項にもどの項を適用してもよい。型を付けない点で型理論の単純型付き λ 計算と異なり、終わらない計算も起こる。
簡約の仕方は一般に 1 通りではない。それでも結果は食い違わない、というのが Church–Rosser の定理 である。この記事では λ 項・代入・β 簡約を定義し、並行簡約を使って Church–Rosser の定理を完全に証明する。そこから正規形の一意性と体系の無矛盾性を導き、不動点定理と自然数の演算の表し方を示す。

定義

変数の可算無限集合を固定し、$x,y,z,f,g$ などで表す。

λ項

λ項（lambda term）を次の規則で帰納的に定める。

変数 $x$ は λ項である。
$x$ が変数、$M$ が λ項なら、$(\lambda x.\,M)$ は λ項である（抽象）。
$M,N$ が λ項なら、$(MN)$ は λ項である（適用）。
適用は左に結合するものとして括弧を省き（$MNL$ は $((MN)L)$）、$\lambda xy.\,M$ は $\lambda x.\,(\lambda y.\,M)$ を表す。$\lambda x.\,M$ の $x$ は $M$ の中で束縛され、束縛されていない変数の出現を自由な出現という。$M$ の自由変数の集合を $\mathrm{FV}(M)$ と書く。

束縛変数の名前だけが違う項（$\lambda x.\,x$ と $\lambda y.\,y$ など）は同じものとみなす（α 同値 による同一視、OLT26 §42.8、pp. 642–643）。以下、証明の中では、考えている項の束縛変数を、そこに現れる自由変数とも互いとも異なるように選んでおく。以下で定める β 簡約・並行簡約は、束縛変数の名前を取り替えても成り立つかどうかが変わらないので、この同一視のもとの関係として扱い、規則を使うときも束縛変数をこのように選び直してよい。

代入

$M$ の自由な $x$ をすべて $N$ に置き換えた項 $M[N/x]$ を、次の再帰で定める。
$$ x[N/x]:=N,\quad y[N/x]:=y\ (y\ne x),\quad (PQ)[N/x]:=P[N/x]\,Q[N/x],\quad (\lambda y.\,P)[N/x]:=\lambda y.\,P[N/x] $$
最後の式では、束縛変数の名前を変えて $y\ne x$、$y\notin\mathrm{FV}(N)$ としておく。

名前を変えるのは、$N$ の自由変数が $\lambda y$ に捕まるのを防ぐためである。たとえば $(\lambda y.\,x)[y/x]$ は $\lambda y'.\,y$ であって $\lambda y.\,y$ ではない。

代入補題

$x\ne y$、$y\notin\mathrm{FV}(N)$ なら、$M[L/y][N/x]=M[N/x][L[N/x]/y]$ である。また $\mathrm{FV}(M[N/x])\subset(\mathrm{FV}(M)\setminus\{x\})\cup\mathrm{FV}(N)$ である。

$M$ の組み立てについての帰納法である。

詳しい証明を開く

$M=y$ なら両辺は $L[N/x]$ である。$M=x$ なら左辺は $N$、右辺は $N[L[N/x]/y]=N$（$y\notin\mathrm{FV}(N)$）である。それ以外の変数では両辺とも $M$ である。適用では帰納法の仮定を成分に使う。$M=\lambda z.\,P$ では $z\ne x,y$、$z\notin\mathrm{FV}(L)\cup\mathrm{FV}(N)$ にとれるので、両辺とも $\lambda z.$ の内側へ入り、帰納法の仮定に帰着する。後半も同じ帰納法で、$x[N/x]=N$ の場合だけ $\mathrm{FV}(N)$ が加わる。$\square$

β簡約

$(\lambda x.\,M)N$ の形の項を β 基 といい、$M[N/x]$ をその縮約という。β 簡約の一歩 $M\to_\beta M'$ を、次で生成される最小の関係とする：$(\lambda x.\,M)N\to_\beta M[N/x]$。$M\to_\beta M'$ なら $MN\to_\beta M'N$、$NM\to_\beta NM'$、$\lambda x.\,M\to_\beta\lambda x.\,M'$。
$\to_\beta$ を $0$ 回以上続けることを $\to_\beta^*$、$\to_\beta$ を含む最小の同値関係を $=_\beta$ と書く。β 基を含まない項を 正規形 といい、$M\to_\beta^*N$ となる正規形 $N$ を $M$ の正規形という。

この定義は OLT26 Definition 42.39–42.42（pp. 643–645）と同じ内容である。

例

基本的な項

$I:=\lambda x.\,x$ とすると $IM\to_\beta M$ である。$K:=\lambda xy.\,x$ とすると $KMN\to_\beta(\lambda y.\,M)N\to_\beta M$（$y\notin\mathrm{FV}(M)$ に名前を選ぶ）で、$K$ は 2 つ目の引数を捨てる。$\omega:=\lambda x.\,xx$、$\Omega:=\omega\omega$ とすると、$\Omega$ の β 基は $\Omega$ 自身だけで、$\Omega\to_\beta(xx)[\omega/x]=\Omega$ である。したがって $\Omega$ からの簡約は $\Omega$ にとどまり、$\Omega$ は正規形をもたない。$(\lambda x.\,y)\Omega$ は外側の β 基を縮約すれば正規形 $y$ になるが、内側の $\Omega$ を縮約し続けると終わらない。

自然数は、関数を何回当てるかで表す。$f^0x:=x$、$f^{n+1}x:=f(f^nx)$ とする。

Church 数と演算

$\overline n:=\lambda fx.\,f^nx$（Church 数）、$\mathrm{Succ}:=\lambda nfx.\,f(nfx)$、$\mathrm{Add}:=\lambda mnfx.\,mf(nfx)$、$\mathrm{Mult}:=\lambda mnf.\,m(nf)$ とおく。すべての $m,n\in\mathbb N$ について
$$ \mathrm{Succ}\,\overline n\to_\beta^*\overline{n+1},\qquad\mathrm{Add}\,\overline m\,\overline n\to_\beta^*\overline{m+n},\qquad\mathrm{Mult}\,\overline m\,\overline n\to_\beta^*\overline{mn}. $$

まず、任意の項 $F,N$ について $\overline nFN\to_\beta(\lambda x.\,F^nx)N\to_\beta F^nN$ である（$x\notin\mathrm{FV}(F)$ に名前を選ぶ）。
Succ：$\mathrm{Succ}\,\overline n\to_\beta\lambda fx.\,f(\overline nfx)\to_\beta^*\lambda fx.\,f(f^nx)=\overline{n+1}$。
Add：$\mathrm{Add}\,\overline m\,\overline n\to_\beta^*\lambda fx.\,\overline mf(\overline nfx)\to_\beta^*\lambda fx.\,\overline mf(f^nx)\to_\beta^*\lambda fx.\,f^m(f^nx)=\overline{m+n}$。
Mult：$\mathrm{Mult}\,\overline m\,\overline n\to_\beta^*\lambda f.\,\overline m(\overline nf)\to_\beta\lambda f.\,\lambda x.\,(\overline nf)^mx$ である。$k$ についての帰納法で $(\overline nf)^kx\to_\beta^*f^{nk}x$ を示す。$k=0$ は等号、$k+1$ では $(\overline nf)^{k+1}x=\overline nf((\overline nf)^kx)\to_\beta^*\overline nf(f^{nk}x)\to_\beta^*f^n(f^{nk}x)=f^{n(k+1)}x$ である。よって $\mathrm{Mult}\,\overline m\,\overline n\to_\beta^*\lambda fx.\,f^{mn}x=\overline{mn}$。$\square$

ここで、$\to_\beta^*$ が文脈と両立すること（$M\to_\beta^*M'$ なら $MN\to_\beta^*M'N$ など）を使った。これは def-lc-beta の後半の規則を各段に使えばよい。

主定理：Church–Rosser の定理

主定理は、$M$ から 2 通りに簡約した結果が、ある $L$ へそれぞれ簡約できること（下の thm-lc-church-rosser の図式）である。$\to_\beta$ の一歩どうしでは、この形が 1 歩ずつでは閉じない（下の反例の表の 1 行目）。そこで、いくつかの β 基を一度に縮約する並行簡約を使う。

並行簡約と完全展開

並行簡約 $M\Rightarrow M'$ を、次の規則で生成される最小の関係とする。

$x\Rightarrow x$。
$M\Rightarrow M'$ なら $\lambda x.\,M\Rightarrow\lambda x.\,M'$。
$M\Rightarrow M'$、$N\Rightarrow N'$ なら $MN\Rightarrow M'N'$。
$M\Rightarrow M'$、$N\Rightarrow N'$ なら $(\lambda x.\,M)N\Rightarrow M'[N'/x]$。
項 $M$ の 完全展開 $M^\circ$ を、$x^\circ:=x$、$(\lambda x.\,P)^\circ:=\lambda x.\,P^\circ$、$P$ が抽象でないとき $(PQ)^\circ:=P^\circ Q^\circ$、$((\lambda x.\,P)Q)^\circ:=P^\circ[Q^\circ/x]$ で定める。

$M^\circ$ は $M$ にもとからある β 基をすべて内側から縮約した項であり、並行簡約は、そのうちの好きなものだけを縮約することにあたる（OLT26 Definition 43.3・43.5、pp. 649–650）。

並行簡約の基本性質

すべての $M$ で $M\Rightarrow M$。
$M\to_\beta M'$ なら $M\Rightarrow M'$。
$M\Rightarrow M'$ なら $M\to_\beta^*M'$ であり、$\mathrm{FV}(M')\subset\mathrm{FV}(M)$。
$M\Rightarrow M'$、$N\Rightarrow N'$ なら $M[N/x]\Rightarrow M'[N'/x]$。

1 は $M$ の組み立て、2 は $\to_\beta$ の生成、3・4 は $M\Rightarrow M'$ の導出についての帰納法である。要の 4 の規則 4 の場合を示す。$M=(\lambda y.\,P)Q$、$M'=P'[Q'/y]$（$P\Rightarrow P'$、$Q\Rightarrow Q'$）とし、$y\ne x$、$y\notin\mathrm{FV}(N)\cup\mathrm{FV}(N')$ に名前を選ぶ。帰納法の仮定と規則 4 により
$$ M[N/x]=(\lambda y.\,P[N/x])\,Q[N/x]\Rightarrow P'[N'/x]\,[\,Q'[N'/x]/y\,] $$
であり、右辺は lem-lc-substitution により $P'[Q'/y][N'/x]=M'[N'/x]$ に等しい。

残りの部分を開く

1：変数は規則 1、抽象と適用は規則 2・3 による。2：根の β 基 $(\lambda x.\,P)Q\to_\beta P[Q/x]$ は 1 と規則 4、文脈の中の一歩は帰納法の仮定と 1 と規則 2・3 による。3：規則 4 では帰納法の仮定から $(\lambda x.\,P)Q\to_\beta^*(\lambda x.\,P')Q'\to_\beta P'[Q'/x]$。自由変数は lem-lc-substitution の後半による。ほかの規則は帰納法の仮定をそのまま使う。4 の規則 1 の場合：$M=M'=x$ なら $N\Rightarrow N'$ そのもの、$M=M'=z\ne x$ なら $z\Rightarrow z$。規則 2・3 の場合は帰納法の仮定を成分に使う（抽象の束縛変数は $x$ とも $N,N'$ の自由変数とも異なるように選ぶ）。$\square$

完全展開の補題

$M\Rightarrow N$ なら $N\Rightarrow M^\circ$ である。とくに、$M\Rightarrow N_1$ かつ $M\Rightarrow N_2$ なら $N_1\Rightarrow M^\circ$ かつ $N_2\Rightarrow M^\circ$ である。

$M\Rightarrow N$ の導出についての帰納法

規則 1：$x\Rightarrow x=x^\circ$。
規則 2：$\lambda x.\,P\Rightarrow\lambda x.\,P'$ なら、帰納法の仮定 $P'\Rightarrow P^\circ$ と規則 2 で $\lambda x.\,P'\Rightarrow\lambda x.\,P^\circ=(\lambda x.\,P)^\circ$。
規則 3：$PQ\Rightarrow P'Q'$ とする。$P$ が抽象でなければ、帰納法の仮定と規則 3 で $P'Q'\Rightarrow P^\circ Q^\circ=(PQ)^\circ$。$P=\lambda x.\,R$ なら、$P\Rightarrow P'$ に使える規則は 2 だけなので $P'=\lambda x.\,R'$、$R\Rightarrow R'$ である。帰納法の仮定 $R'\Rightarrow R^\circ$、$Q'\Rightarrow Q^\circ$ と規則 4 で $(\lambda x.\,R')Q'\Rightarrow R^\circ[Q^\circ/x]=((\lambda x.\,R)Q)^\circ$。
規則 4：$(\lambda x.\,R)Q\Rightarrow R'[Q'/x]$ なら、帰納法の仮定 $R'\Rightarrow R^\circ$、$Q'\Rightarrow Q^\circ$ と lem-lc-parallel-basic の 4 で $R'[Q'/x]\Rightarrow R^\circ[Q^\circ/x]=((\lambda x.\,R)Q)^\circ$。
後半は前半を 2 回使えばよい。$\square$

Church–Rosser の定理

$M\to_\beta^*N_1$ かつ $M\to_\beta^*N_2$ なら、$N_1\to_\beta^*L$ かつ $N_2\to_\beta^*L$ となる項 $L$ がある。
$$ \xymatrix{ & M \ar[dl]_{*} \ar[dr]^{*} & \\ N_1 \ar@{.>}[dr]_{*} & & N_2 \ar@{.>}[dl]^{*} \\ & L & } $$

格子に菱形を敷き詰める

$\Rightarrow$ を $m$ 回続けることを $\Rightarrow^m$ と書く。lem-lc-parallel-basic の 1〜3 により、$M\to_\beta^*N$ はある $m$ で $M\Rightarrow^mN$ となることと同値である（$\to_\beta$ の一歩は $\Rightarrow$ の一歩であり、$\Rightarrow$ の一歩は $\to_\beta^*$ である）。したがって次を示せばよい。
主張：$M\Rightarrow^mN_1$、$M\Rightarrow^nN_2$ なら、$N_1\Rightarrow^nL$、$N_2\Rightarrow^mL$ となる $L$ がある。
まず $n=1$ の場合を $m$ についての帰納法で示す。$m=0$ なら $L:=N_2$。$M\Rightarrow^mP\Rightarrow N_1$、$M\Rightarrow N_2$ なら、帰納法の仮定により $P\Rightarrow L'$、$N_2\Rightarrow^mL'$ となる $L'$ がある。$P\Rightarrow N_1$ と $P\Rightarrow L'$ に lem-lc-takahashi を使うと $N_1\Rightarrow P^\circ$、$L'\Rightarrow P^\circ$ なので、$L:=P^\circ$ とすれば $N_2\Rightarrow^{m+1}L$ である。
一般の $n$ は $n$ についての帰納法による。$M\Rightarrow^nQ\Rightarrow N_2$ なら、帰納法の仮定で $N_1\Rightarrow^nL''$、$Q\Rightarrow^mL''$ となる $L''$ をとり、$Q\Rightarrow N_2$ と $Q\Rightarrow^mL''$ に $n=1$ の場合を使うと、$L''\Rightarrow L$、$N_2\Rightarrow^mL$ となる $L$ がある。$N_1\Rightarrow^{n+1}L$ である。$\square$

完全展開を使うこの証明の流れは OLT26 §43.2–43.3（Theorem 43.12、p. 652）にもある（同書は一部の場合を演習に残している）。

正規形の一意性と β 同値の判定

$M=_\beta N$ であるのは、$M\to_\beta^*L$ かつ $N\to_\beta^*L$ となる $L$ があるときに限る。
項の正規形は、あれば（α 同値を除いて）ただ 1 つである。$M=_\beta N$ で $N$ が正規形なら $M\to_\beta^*N$ である。
異なる正規形どうしは β 同値でない。とくに $\lambda xy.\,x\ne_\beta\lambda xy.\,y$ であり、$m\ne n$ なら $\overline m\ne_\beta\overline n$ である。

1：「共通の簡約先がある」という関係 $\sim$ は反射的・対称的で、$\to_\beta$ を含む。推移的でもある：$M\to_\beta^*L_1\leftarrow N$、$N\to_\beta^*L_2\leftarrow P$（矢印は $\to_\beta^*$）なら、thm-lc-church-rosser を $N$ に使って $L_1\to_\beta^*L$、$L_2\to_\beta^*L$ となる $L$ をとれる。よって $\sim$ は $\to_\beta$ を含む同値関係なので $=_\beta$ を含む。逆の包含は明らかである。2：$N_1,N_2$ が $M$ の正規形なら、thm-lc-church-rosser の $L$ について $N_i\to_\beta^*L$ だが、正規形からの簡約は 0 回しかないので $N_1=L=N_2$。後半は 1 による。3：2 の後半による。$\square$

3 は、$=_\beta$ がすべての項を同一視するわけではないこと、すなわち β 同値の等式の体系が矛盾しないことを示している。

不動点定理

$Y:=\lambda f.\,(\lambda x.\,f(xx))(\lambda x.\,f(xx))$、$A:=\lambda xy.\,y(xxy)$、$\Theta:=AA$ とおく。任意の項 $F$ について $YF=_\beta F(YF)$、$\Theta F\to_\beta^*F(\Theta F)$ である。

$x\notin\mathrm{FV}(F)$ に名前を選び、$W:=(\lambda x.\,F(xx))(\lambda x.\,F(xx))$ とおく。$YF\to_\beta W\to_\beta F\bigl((\lambda x.\,F(xx))(\lambda x.\,F(xx))\bigr)=FW$ であり、$F(YF)\to_\beta FW$ である。共通の簡約先があるので $YF=_\beta F(YF)$。次に $\Theta F=AAF\to_\beta(\lambda y.\,y(AAy))F\to_\beta F(AAF)=F(\Theta F)$。$\square$

$Y$ は Curry の不動点結合子、$\Theta$ は Turing の不動点結合子と呼ばれる（OLT26 §41.12、p. 629、Theorem 44.14、p. 663）。不動点定理により、$g$ を含む式 $N$ による再帰的な定義 $gx=N$ は、$G:=\Theta(\lambda gx.\,N)$ とおけば $Gx\to_\beta^*N[G/g]$ として実現できる。

λ定義可能な関数

λ定義可能性

$\mathbb N^k$ の部分集合の上で定義された関数 $f\colon\mathbb N^k\rightharpoonup\mathbb N$ を考える。項 $F$ が $f$ を λ 定義する とは、すべての $n_1,\dots,n_k$ について、$f(n_1,\dots,n_k)$ が定義されていれば $F\overline{n_1}\cdots\overline{n_k}\to_\beta^*\overline{f(n_1,\dots,n_k)}$ で、定義されていなければ $F\overline{n_1}\cdots\overline{n_k}$ が正規形をもたないことをいう（OLT26 Definition 44.2、p. 656）。

cor-lc-unique-normal-form により、$F\overline{n_1}\cdots\overline{n_k}$ の正規形はあればただ 1 つで、Church 数どうしは β 同値でないので、$F$ が定める関数は 1 つに決まる。prop-lc-church-numerals により、後者関数・和・積は λ 定義可能である。

λ定義可能性と部分再帰関数

部分関数 $f\colon\mathbb N^k\rightharpoonup\mathbb N$ が λ 定義可能であるのは、$f$ が部分再帰関数（μ再帰関数）であるときに限る。

証明の所在

この記事では証明しない。全域的な再帰関数が λ 定義可能であることは OLT26 Proposition 44.16（p. 666）が、基本関数が λ 定義可能で、λ 定義可能な関数が合成・原始再帰・正則な最小化（不動点結合子を使う）で閉じることから示している。部分関数への拡張は Theorem 44.17（p. 666、証明は述べていない）、逆向きは Theorem 44.18（p. 667、証明の概略）である。この一致は Church–Turingのテーゼの根拠の 1 つになっている。

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
並行簡約 $\Rightarrow$（lem-lc-takahashi の後半の形を一歩の $\to_\beta$ で述べる）	$(\lambda x.\,xx)(Iz)$	2 つの一歩の簡約先が、それぞれ高々一歩で共通の項になること
型を付けること（型理論の定理「弱正規化定理」の仮定）	$\Omega=(\lambda x.\,xx)(\lambda x.\,xx)$	正規形をもつこと
$N_1,N_2$ が正規形であること（cor-lc-unique-normal-form の 2）	$(\lambda x.\,y)(Iz)$	簡約先がただ 1 つであること

反例の確かめ

1 行目：$M:=(\lambda x.\,xx)(Iz)$ は、外側を縮約して $(Iz)(Iz)$、内側を縮約して $(\lambda x.\,xx)z$ になる。$(\lambda x.\,xx)z$ から一歩で行けるのは $zz$ だけで、$(Iz)(Iz)$ から高々一歩で行けるのは $(Iz)(Iz)$、$z(Iz)$、$(Iz)z$ である。共通の項はない。並行簡約では $(Iz)(Iz)\Rightarrow zz$ と $(\lambda x.\,xx)z\Rightarrow zz$ が一度にでき、$M^\circ=zz$ である。2 行目：ex-lc-basic のとおり $\Omega$ からの簡約は $\Omega$ にとどまる。3 行目：$(\lambda x.\,y)(Iz)$ は外側を縮約して $y$、内側を縮約して $(\lambda x.\,y)z$ になり、2 つは異なる。後者は正規形でなく、さらに一歩で $y$ になるので、正規形は一致する。