型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす

0. この記事の要点

この記事で扱うのは、「$x$ に $x^2+1$ を対応させる関数」に名前を付けずに書き、その関数に値を渡して中身を書き換えていく、というだけの小さな計算の体系です。ところがこの体系だけで、数も条件分岐も繰り返しも表せます。読み終えると、「どの順番で書き換えても答えは一つしかない」ことと、「この体系が通常の意味の計算可能な関数をすべて表せる」ことの理由が分かります。

• ラムダ計算は「関数を作る」($\lambda x.M$) と「関数を適用する」($MN$) の二つの操作だけからなる計算の体系です。計算の規則は $(\lambda x.M)N\to M[x:=N]$（β 簡約）ただ一つです。
• チャーチ＝ロッサーの定理（定理 4.1）：どの順番で簡約しても、結果は最後に合流できる。とくに正規形（それ以上簡約できない形）は、存在すればただ一つです。並行簡約と「完全展開」を使って証明します。
• 不動点定理（定理 5.1）：任意の項 $F$ に対して $FX=_\beta X$ となる $X$ がある。名前のない関数だけで再帰的定義を書けるのは、この定理のおかげです。
• 自然数をチャーチ数 $\overline n=\lambda f x.f^n x$ で表すと、λ 定義可能な数論的関数はちょうど再帰関数です（定理 6.4）。チューリング機械と同じ計算能力を、関数の言葉だけで実現しています。
• ラムダ計算は Lisp・Haskell・Lean などの関数型言語の核であり、次章のカリー＝ハワード対応で「証明」の計算側の顔になります。

この記事で使う事前知識

• チューリング機械: 状態と読み書きヘッドをもつ、計算の標準的な数学モデル。→ チューリング機械
• 部分再帰関数: 基本関数から合成・原始再帰・最小化 ($\mu$) で作れる関数（止まらない入力があってもよい）。→ 部分再帰関数
• 原始再帰関数: 基本関数から合成と原始再帰だけで作れる関数。→ 原始再帰関数
• ゲーデル数: 式や項を自然数に符号化したもの。→ ゲーデル数
• 同値関係: 反射的・対称的・推移的な関係。「同じものとみなす」ための道具。→ 同値関係
• 帰納法: 自然数や、項のような帰納的に作られるものについての証明法。→ 証明の技術

1. 動機：名前のない関数で計算を書く

1.1. 「関数そのもの」を書きたい

数学では $f(x)=x^2+1$ のように、関数を名前 $f$ と変数 $x$ を使って定義します。けれども、関数を「値」として扱いたい場面がよくあります。微分作用素 $D$ は関数を受け取って関数を返しますし、積分 $\int_0^1(\cdot)\,dx$ は関数を受け取って数を返します。このとき「$x$ に $x^2+1$ を対応させる関数」を名前なしで書けると便利です。それが $\lambda x.\,x^2+1$ という記法で、プログラミング言語では fun x => x^2 + 1（Lean）や lambda x: x**2 + 1（Python）と書きます。

チャーチ (1930 年代) は、この「名前のない関数」と「適用」だけで数学の基礎を作ろうとしました。論理体系としての試みは矛盾で挫折しましたが、残った計算の部分が驚くほど強力でした。数も、真偽値も、組も、再帰も、すべて関数で表せるのです。

1.2. なぜいま学ぶか

ラムダ計算には、三つの顔があります。

1. 計算のモデル。計算可能性 のチューリング機械と再帰関数に並ぶ、三つ目の定義です。三者が一致することが、チャーチ＝チューリングの提唱（注意 6.4［計算可能性］）の根拠の一つになりました。この記事で、再帰関数との一致を証明します。
2. プログラミング言語の核。関数型言語の評価は β 簡約そのものです。どの順に評価しても答えが同じになる、という安心感の数学的な根拠がチャーチ＝ロッサーの定理です。
3. 証明の計算的な中身。次章で型を付けると、λ 項がそのまま自然演繹の証明になり、β 簡約が「証明の回り道を取り除く」操作になります（カリー＝ハワード対応）。Lean で theorem の証明として書く項は、型付きの λ 項です。

この記事は型を付けない体系を扱います。型がないので $xx$（自分自身への適用）も許され、そこから不動点と無限ループが生まれます。この自由さが計算の万能性の源であり、同時に論理としての矛盾の源でもあります。

2. λ 項と置換

定義 2.1（λ 項）↗

可算無限個の変数 $x,y,z,\ldots$ を用意する。λ 項を次で帰納的に定める。

1. 変数 $x$ は λ 項である。
2. $M,N$ が λ 項ならば、適用 $(MN)$ は λ 項である。
3. $M$ が λ 項で $x$ が変数ならば、抽象 $(\lambda x.M)$ は λ 項である。

括弧は省略し、適用は左結合（$MNL=(MN)L$）、$\lambda$ の作用域はできるだけ右へ伸ばし、$\lambda xy.M=\lambda x.\lambda y.M$ と書く。自由変数の集合 $\mathrm{FV}$ を $\mathrm{FV}(x)=\{x\}$、$\mathrm{FV}(MN)=\mathrm{FV}(M)\cup\mathrm{FV}(N)$、$\mathrm{FV}(\lambda x.M)=\mathrm{FV}(M)\setminus\{x\}$ で定める。自由変数をもたない項を閉項という。

$\lambda x.x$ と $\lambda y.y$ はどちらも恒等関数で、束縛変数の名前だけが違います。束縛変数の付け替えで移り合う項を α 同値（同値関係の一つ）といい、以下では α 同値な項を同一視し、等号 $\equiv$ で表します。さらに、ある議論に現れる束縛変数は、自由変数とも互いにも異なるように選んであるものとします（変数の規約）。

定義 2.2（置換）↗

$M[x:=N]$ を、$M$ の自由な $x$ をすべて $N$ で置き換えた項とする。帰納的には

$$x[x:=N]\equiv N,\quad y[x:=N]\equiv y\ (y\ne x),\quad (PQ)[x:=N]\equiv P[x:=N]\,Q[x:=N],$$$$(\lambda y.P)[x:=N]\equiv\lambda y.P[x:=N]\quad(y\ne x,\ y\notin\mathrm{FV}(N))$$

と定める。最後の条件は変数の規約により（束縛変数を付け替えて）いつでも満たせる。

なお、条件を満たすように束縛変数を付け替える手順は単純で、$\lambda y.P$ の $y$ を $N$ の自由変数ではない新しい変数 $y'$ に取り替え、$P$ の中の自由な $y$ も同じ $y'$ に取り替えるだけです。たとえば $(\lambda y.x)[x:=y]$ なら、先に $\lambda y.x$ を $\lambda y'.x$ と書き直してから置換して $\lambda y'.y$ とします。

条件 $y\notin\mathrm{FV}(N)$ を落とすと、$(\lambda y.x)[x:=y]$ が $\lambda y.y$ になってしまいます。「定数関数 $y$」のはずが恒等関数に化けるわけで、これを変数の捕獲といいます。

補題 2.3（置換補題）✓

$x\ne y$ かつ $x\notin\mathrm{FV}(L)$ ならば、

$$M[x:=N][y:=L]\equiv M[y:=L][x:=N[y:=L]].$$

証明（補題 2.3）

$M$ の構成に関する帰納法。$M\equiv x$ なら両辺とも $N[y:=L]$。$M\equiv y$ なら左辺は $y[y:=L]\equiv L$（$x$ の置換は $y$ を変えない）、右辺は $L[x:=N[y:=L]]\equiv L$（$x\notin\mathrm{FV}(L)$）。$M$ がそれ以外の変数 $z$ なら両辺とも $z$。$M\equiv PQ$ なら帰納法の仮定を各成分に使う。$M\equiv\lambda z.P$ なら、変数の規約で $z\ne x,y$、$z\notin\mathrm{FV}(N)\cup\mathrm{FV}(L)$ としてよく、置換は $\lambda z$ の内側に入るので $P$ についての帰納法の仮定に帰着する。

∎

3. β 簡約

定義 3.1（β 簡約）↗

$(\lambda x.M)N$ の形の項を β 基（redex）といい、$M[x:=N]$ をその縮約という。項の中の一つの β 基を縮約することを 1 ステップの β 簡約 $M\to_\beta N$ という。厳密には、$(\lambda x.M)N\to_\beta M[x:=N]$ を含み、$M\to_\beta M'$ ならば $MN\to_\beta M'N$、$NM\to_\beta NM'$、$\lambda x.M\to_\beta\lambda x.M'$ となる最小の関係である。

$\to_\beta$ の反射推移閉包を $\twoheadrightarrow_\beta$（簡約）、反射対称推移閉包を $=_\beta$（β 同値）と書く。β 基を含まない項を β 正規形といい、$M\twoheadrightarrow_\beta N$ で $N$ が正規形のとき、$N$ を $M$ の正規形という。

例 3.2（簡約のいろいろな振る舞い）

$I\equiv\lambda x.x$、$K\equiv\lambda xy.x$、$\omega\equiv\lambda x.xx$、$\Omega\equiv\omega\omega$ とおきます。

• $IM\to_\beta M$。$KMN\to_\beta(\lambda y.M)N\to_\beta M$（$y\notin\mathrm{FV}(M)$）。
• $\Omega\equiv(\lambda x.xx)(\lambda x.xx)\to_\beta(\lambda x.xx)(\lambda x.xx)\equiv\Omega$。$\Omega$ は自分自身にしか簡約されず、正規形をもちません。
• $KI\Omega$ は、先頭の $K$ から簡約すれば 2 ステップで $I$ になります。一方、引数の $\Omega$ ばかり簡約し続けると、いつまでも終わりません。

最後の例は、簡約の順序によって止まったり止まらなかったりすることを示しています。それでも、止まったときの答えは一つしかない、というのが次節の定理です。

4. チャーチ＝ロッサーの定理

定理 4.1（チャーチ＝ロッサーの定理）✓

$M\twoheadrightarrow_\beta N_1$ かつ $M\twoheadrightarrow_\beta N_2$ ならば、$N_1\twoheadrightarrow_\beta P$ かつ $N_2\twoheadrightarrow_\beta P$ となる項 $P$ が存在する。

1 ステップの $\to_\beta$ について「合流」を示して繰り返す、という素朴な方針はうまくいきません。$(\lambda x.xx)((\lambda y.y)z)$ で引数のほうを先に縮約すると、もう一方の道では引数が 2 か所にコピーされているので、追いつくのに 2 ステップ必要になるからです。そこで、複数の β 基を同時に縮約する関係を考えます（テイトとマーティン＝レーフの方法、高橋の完全展開による簡略化）。

定義 4.2（並行簡約と完全展開）↗

並行簡約 $\Rightarrow$ を次の規則で帰納的に定める。

1. $x\Rightarrow x$。
2. $M\Rightarrow M'$ ならば $\lambda x.M\Rightarrow\lambda x.M'$。
3. $M\Rightarrow M'$、$N\Rightarrow N'$ ならば $MN\Rightarrow M'N'$。
4. $M\Rightarrow M'$、$N\Rightarrow N'$ ならば $(\lambda x.M)N\Rightarrow M'[x:=N']$。

項 $M$ の完全展開 $M^{*}$ を、$x^{*}\equiv x$、$(\lambda x.M)^{*}\equiv\lambda x.M^{*}$、$((\lambda x.M)N)^{*}\equiv M^{*}[x:=N^{*}]$、$M$ が抽象でないとき $(MN)^{*}\equiv M^{*}N^{*}$ で定める。

$M^{*}$ は「$M$ に最初からある β 基を、内側から全部いっぺんに縮約したもの」です。たとえば $M\equiv(\lambda x.xx)(Iz)$（$I\equiv\lambda y.y$）では、引数 $Iz$ の完全展開は $z$、本体 $xx$ の完全展開は $xx$ 自身なので、$M^{*}\equiv(xx)[x:=z]\equiv zz$ です。外側の β 基と引数の β 基が一度に縮約されています。

並行簡約を考える狙いは、次の三角補題にあります。どの並行簡約の行き先 $N$ からも、完全展開 $M^{*}$ という一つの決まった項に 1 歩で追いつける、という主張です。これが菱形性そのものになり、チャーチ＝ロッサーの定理が出ます。

補題 4.3（並行簡約の基本性質）✓

(1) すべての $M$ で $M\Rightarrow M$。(2) $M\to_\beta N$ ならば $M\Rightarrow N$。(3) $M\Rightarrow N$ ならば $M\twoheadrightarrow_\beta N$。したがって $\twoheadrightarrow_\beta$ は $\Rightarrow$ の推移閉包に等しい。

証明（補題 4.3）

(1) $M$ の構成に関する帰納法で、規則 1〜3 を使う。(2) $\to_\beta$ の定義に関する帰納法。β 基の縮約 $(\lambda x.M)N\to_\beta M[x:=N]$ は規則 4 と (1)。文脈の中での縮約は、縮約しない部分に (1) を使って規則 2・3 で組み立てる。(3) $\Rightarrow$ の導出に関する帰納法。規則 4 なら、帰納法の仮定 $M\twoheadrightarrow_\beta M'$、$N\twoheadrightarrow_\beta N'$ から $(\lambda x.M)N\twoheadrightarrow_\beta(\lambda x.M')N'\to_\beta M'[x:=N']$。ほかの規則も同様。最後の主張は (2) と (3) から従う。

∎

補題 4.4（並行簡約と置換）✓

$M\Rightarrow M'$ かつ $N\Rightarrow N'$ ならば、$M[x:=N]\Rightarrow M'[x:=N']$。

証明（補題 4.4）

$M\Rightarrow M'$ の導出に関する帰納法。

• 規則 1：$M\equiv M'\equiv y$。$y\equiv x$ なら両辺は $N\Rightarrow N'$。$y\ne x$ なら $y\Rightarrow y$。
• 規則 2・3：帰納法の仮定をそのまま規則 2・3 に入れる（規則 2 では変数の規約で束縛変数を $x$ と $\mathrm{FV}(N)$ から避ける）。
• 規則 4：$M\equiv(\lambda y.P)Q$、$M'\equiv P'[y:=Q']$、$P\Rightarrow P'$、$Q\Rightarrow Q'$。変数の規約で $y\ne x$、$y\notin\mathrm{FV}(N)\cup\mathrm{FV}(N')$ とする。帰納法の仮定から $P[x:=N]\Rightarrow P'[x:=N']$、$Q[x:=N]\Rightarrow Q'[x:=N']$ なので、規則 4 により

$$M[x:=N]\equiv(\lambda y.P[x:=N])(Q[x:=N])\Rightarrow P'[x:=N'][y:=Q'[x:=N']]\equiv P'[y:=Q'][x:=N'].$$

最後の $\equiv$ は置換補題（補題 2.3。$y\notin\mathrm{FV}(N')$ を使う）である。右辺は $M'[x:=N']$ に等しい。

∎

補題 4.5（三角補題）✓

$M\Rightarrow N$ ならば $N\Rightarrow M^{*}$。

証明（補題 4.5）

$M\Rightarrow N$ の導出に関する帰納法。

• 規則 1：$x\Rightarrow x\equiv x^{*}$。
• 規則 2：$\lambda x.P\Rightarrow\lambda x.P'$。帰納法の仮定 $P'\Rightarrow P^{*}$ と規則 2 で $\lambda x.P'\Rightarrow\lambda x.P^{*}\equiv(\lambda x.P)^{*}$。
• 規則 3：$PQ\Rightarrow P'Q'$。$P$ が抽象でなければ、帰納法の仮定と規則 3 で $P'Q'\Rightarrow P^{*}Q^{*}\equiv(PQ)^{*}$。$P\equiv\lambda x.R$ なら、$P\Rightarrow P'$ は規則 2 によるしかないので $P'\equiv\lambda x.R'$、$R\Rightarrow R'$ である。帰納法の仮定（$R\Rightarrow R'$ と $Q\Rightarrow Q'$ に対して）$R'\Rightarrow R^{*}$、$Q'\Rightarrow Q^{*}$ と規則 4 により $(\lambda x.R')Q'\Rightarrow R^{*}[x:=Q^{*}]\equiv(PQ)^{*}$。
• 規則 4：$(\lambda x.P)Q\Rightarrow P'[x:=Q']$。帰納法の仮定 $P'\Rightarrow P^{*}$、$Q'\Rightarrow Q^{*}$ と 補題 4.4 により $P'[x:=Q']\Rightarrow P^{*}[x:=Q^{*}]\equiv((\lambda x.P)Q)^{*}$。

∎

証明（定理 4.1）

補題 4.5 より、$M\Rightarrow N_1$ かつ $M\Rightarrow N_2$ ならば $N_1\Rightarrow M^{*}$ かつ $N_2\Rightarrow M^{*}$。つまり $\Rightarrow$ は菱形性（一歩ずつ分かれた二つの道が、それぞれ一歩で合流する）をもつ。

補題 4.3 より、$M\twoheadrightarrow_\beta N_1$ は $\Rightarrow$ の有限列 $M\equiv A_0\Rightarrow A_1\Rightarrow\cdots\Rightarrow A_m\equiv N_1$、$M\twoheadrightarrow_\beta N_2$ は $M\equiv B_0\Rightarrow\cdots\Rightarrow B_n\equiv N_2$ と書ける。格子 $C_{i,j}$（$C_{i,0}=A_i$、$C_{0,j}=B_j$）を、菱形性で $C_{i+1,j}\Rightarrow C_{i+1,j+1}$ かつ $C_{i,j+1}\Rightarrow C_{i+1,j+1}$ となるように $i+j$ の小さい順に埋めていく。$P=C_{m,n}$ とすれば $N_1\Rightarrow\cdots\Rightarrow P$、$N_2\Rightarrow\cdots\Rightarrow P$ であり、補題 4.3 (3) により $N_1\twoheadrightarrow_\beta P$、$N_2\twoheadrightarrow_\beta P$。

∎

チャーチ＝ロッサーの証明の構造。並行簡約の菱形（左）をタイルのように敷き詰めて、任意の長さの簡約を合流させる（右）。

系 4.6（チャーチ＝ロッサーの帰結）✓

(1) $M=_\beta N$ であることと、$M\twoheadrightarrow_\beta P$ かつ $N\twoheadrightarrow_\beta P$ となる $P$ が存在することは同値である。

(2) 正規形は、存在すればただ一つである。さらに $M=_\beta N$ で $N$ が正規形なら $M\twoheadrightarrow_\beta N$。

(3) $\lambda xy.x\ne_\beta\lambda xy.y$。とくに $=_\beta$ はすべての項を等しくするような自明な関係ではない。

証明（系 4.6）

(1) 共通の簡約先が存在すれば、途中を逆にたどって $M=_\beta N$。逆に、「共通の簡約先をもつ」という関係 $\sim$ は反射的・対称的で $\to_\beta$ を含む。推移的でもある：$M\sim N$（共通の簡約先 $P$）、$N\sim L$（共通の簡約先 $Q$）なら、$N\twoheadrightarrow_\beta P$、$N\twoheadrightarrow_\beta Q$ に 定理 4.1 を使って $P,Q\twoheadrightarrow_\beta R$ をとると、$M,L\twoheadrightarrow_\beta R$。$=_\beta$ は $\to_\beta$ を含む最小の同値関係なので $=_\beta\subseteq\sim$。

(2) $N_1,N_2$ がともに $M$ の正規形なら、(1) より共通の簡約先 $P$ がある。正規形は自分自身にしか簡約されないので $N_1\equiv P\equiv N_2$。後半も (1) から同様。

(3) 両者は異なる正規形なので、(2) より β 同値でない。

∎

(3) は地味ですが重要です。β 同値を「等式」とみなす体系（λ 理論）が無矛盾であることを、この定理が保証しています。

注意 4.7（正規形の見つけ方）

例 3.2 の $KI\Omega$ のように、正規形があっても簡約の順序しだいで止まらないことがあります。最左最外の β 基（最も左にある $\lambda$ から始まる β 基）を常に縮約する戦略をとると、正規形があれば必ずそこに到達することが知られています（正規化定理。Barendregt の教科書の第 13 章）。この記事では使わないので、証明は省略します。

5. 不動点と再帰

型のない世界では、すべての項に不動点があります。

定理 5.1（不動点定理）✓

$Y\equiv\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$ とおく。任意の項 $F$ について $YF=_\beta F(YF)$。とくに任意の $F$ に対して $FX=_\beta X$ となる $X$ が存在する。

証明（定理 5.1）

$A\equiv\lambda x.F(xx)$ とおくと、$YF\to_\beta AA\to_\beta F(AA)$。一方 $F(YF)\to_\beta F(AA)$。両者は共通の簡約先 $F(AA)$ をもつので $YF=_\beta F(YF)$。$X\equiv YF$ とすればよい。

∎

$YF$ は $F(YF)$ に簡約されるわけではなく、両者が共通の項に簡約されるだけです。「$2+3$ と $1+4$ は、どちらも計算すれば $5$ になるので等しい」というのと同じ感覚で、$=_\beta$ は「簡約の向きは問わず、どこかで合流する」という関係です。簡約の向きまで欲しいときは、チューリングの不動点結合子 $\Theta\equiv(\lambda xy.y(xxy))(\lambda xy.y(xxy))$ を使います。$\Theta F\twoheadrightarrow_\beta F(\Theta F)$ は 2 ステップで確かめられます（演習）。

不動点定理は、再帰的定義を名前なしで書く方法を与えます。「$f=\cdots f\cdots$」と自分自身を参照して定義したい関数があれば、右辺の $f$ を変数として抽象した $F\equiv\lambda f.\cdots f\cdots$ をつくり、$YF$ をとればよいのです。定理 6.4 の証明で、最小化をこの方法で実現します。

6. λ 定義可能性と再帰関数

6.1. チャーチ数と基本的な符号化

この節では 計算可能性 に合わせて $0$ も自然数に含め、$\mathbb{N}=\{0,1,2,\ldots\}$ とします。

定義 6.1（チャーチ数と λ 定義可能性）↗

$n\in\mathbb{N}$ のチャーチ数を $\overline n\equiv\lambda fx.f^nx$ とする。ここで $f^0x\equiv x$、$f^{n+1}x\equiv f(f^nx)$。全関数 $\varphi:\mathbb{N}^k\to\mathbb{N}$ が λ 定義可能であるとは、閉項 $F$ が存在して、すべての $n_1,\ldots,n_k$ について

$$F\,\overline{n_1}\cdots\overline{n_k}=_\beta\overline{\varphi(n_1,\ldots,n_k)}$$

となることをいう。

チャーチ数 $\overline n$ は「関数を $n$ 回繰り返す」という操作そのものです。すぐに確かめられる性質として、任意の $F,X$ について $\overline nFX\twoheadrightarrow_\beta F^nX$。そこから $\overline{n+1}FX=_\beta F(\overline nFX)$ が従います（両辺とも $F^{n+1}X$ に簡約される）。

補題 6.2（チャーチ数・真偽値・組の基本項）✓

(1) $\mathsf{S}\equiv\lambda nfx.f(nfx)$ について $\mathsf{S}\,\overline n\twoheadrightarrow_\beta\overline{n+1}$。(2) $\mathsf{T}\equiv\lambda xy.x$、$\mathsf{F}\equiv\lambda xy.y$ について $\mathsf{T}MN\twoheadrightarrow_\beta M$、$\mathsf{F}MN\twoheadrightarrow_\beta N$。(3) $\mathsf{Z}\equiv\lambda n.n(\lambda z.\mathsf{F})\mathsf{T}$ について $\mathsf{Z}\,\overline0\twoheadrightarrow_\beta\mathsf{T}$、$\mathsf{Z}\,\overline{n+1}\twoheadrightarrow_\beta\mathsf{F}$。(4) $\langle M,N\rangle\equiv\lambda z.zMN$、$\pi_1\equiv\lambda p.p\mathsf{T}$、$\pi_2\equiv\lambda p.p\mathsf{F}$ について $\pi_i\langle M_1,M_2\rangle\twoheadrightarrow_\beta M_i$。

証明（補題 6.2）

(1) $\mathsf{S}\,\overline n\twoheadrightarrow_\beta\lambda fx.f(\overline nfx)\twoheadrightarrow_\beta\lambda fx.f(f^nx)\equiv\overline{n+1}$（$\overline nfx\twoheadrightarrow_\beta f^nx$）。(2) $\mathsf{T}MN\to_\beta(\lambda y.M)N\to_\beta M$、$\mathsf{F}MN\to_\beta(\lambda y.y)N\to_\beta N$。(3) $\mathsf{Z}\,\overline0\to_\beta\overline0(\lambda z.\mathsf{F})\mathsf{T}\twoheadrightarrow_\beta\mathsf{T}$、$\mathsf{Z}\,\overline{n+1}\twoheadrightarrow_\beta(\lambda z.\mathsf{F})((\lambda z.\mathsf{F})^n\mathsf{T})\to_\beta\mathsf{F}$。(4) $\pi_i\langle M_1,M_2\rangle\to_\beta\langle M_1,M_2\rangle\mathsf{T}$（または $\mathsf{F}$）$\to_\beta\mathsf{T}M_1M_2\twoheadrightarrow_\beta M_1$（$i=2$ なら $\mathsf{F}M_1M_2\twoheadrightarrow_\beta M_2$）。

∎

例 6.3（チャーチ数の演算）

• 後者 $\mathsf{S}\equiv\lambda nfx.f(nfx)$：$\mathsf{S}\,\overline n\twoheadrightarrow_\beta\lambda fx.f(\overline nfx)\twoheadrightarrow_\beta\lambda fx.f(f^nx)\equiv\overline{n+1}$。
• 真偽値 $\mathsf{T}\equiv\lambda xy.x$、$\mathsf{F}\equiv\lambda xy.y$。$\mathsf{T}MN\twoheadrightarrow_\beta M$、$\mathsf{F}MN\twoheadrightarrow_\beta N$ なので、$BMN$ が「if $B$ then $M$ else $N$」になる。
• ゼロ判定 $\mathsf{Z}\equiv\lambda n.n(\lambda z.\mathsf{F})\mathsf{T}$：$\mathsf{Z}\,\overline0\twoheadrightarrow_\beta\mathsf{T}$、$\mathsf{Z}\,\overline{n+1}\twoheadrightarrow_\beta(\lambda z.\mathsf{F})(\cdots)\to_\beta\mathsf{F}$。
• 組 $\langle M,N\rangle\equiv\lambda z.zMN$、射影 $\pi_1\equiv\lambda p.p\mathsf{T}$、$\pi_2\equiv\lambda p.p\mathsf{F}$：$\pi_i\langle M_1,M_2\rangle\twoheadrightarrow_\beta M_i$。

型付きの言語でも、型を固定すればチャーチ数を書けます。次の Lean 4 のコード（標準ライブラリだけで動きます）は、$\overline2$ と $\overline3$ の和を計算し、#reduce で正規形を表示させたものです。

def two   : (Nat → Nat) → Nat → Nat := fun f x => f (f x)
def three : (Nat → Nat) → Nat → Nat := fun f x => f (f (f x))
def add (m n : (Nat → Nat) → Nat → Nat) : (Nat → Nat) → Nat → Nat :=
  fun f x => m f (n f x)

#eval add two three (· + 1) 0   -- 5
#reduce add two three           -- fun f x => f (f (f (f (f x))))
example : add two three (· + 1) 0 = 5 := rfl

fun f x => ... が $\lambda fx.\cdots$ です。#reduce は項を β 簡約（と定義の展開）で正規形にして表示するコマンドで、出力はチャーチ数 $\overline5$ そのものになっています。ただし Lean では $\lambda x.xx$ や $Y$ は型が付かないので書けません。その理由は次章で明らかになります。

6.2. 再帰関数は λ 定義可能

定理 6.4（クリーネの定理（λ 定義可能性と再帰性））✓

全関数 $\varphi:\mathbb{N}^k\to\mathbb{N}$ について、$\varphi$ が再帰関数（定義 4.1［計算可能性］ の意味で、全関数である部分再帰関数）であることと、λ 定義可能であることは同値である。

証明の方向は二つあります。再帰関数から λ 項を作る向きでは、再帰関数の生成規則（合成・原始再帰・最小化）を一つずつ λ 項で実現します。逆向きでは、λ 項の簡約の列を数で表して、簡約を追うことが再帰関数で書けることを示します。

まず、再帰関数の作り方を「全関数のまま」で言い直しておきます。

補題 6.5（再帰関数の全関数による生成）✓

再帰関数全体は、基本関数（ゼロ・後者・射影）を含み、合成、原始再帰、および正則な最小化（全関数 $g$ で、各 $\vec x$ に $g(\vec x,y)=0$ となる $y$ が存在するものへの $\mu$）で閉じた最小の関数族に等しい。

証明（補題 6.5）

この族の元は明らかに全関数である部分再帰関数である。逆に $\varphi$ を再帰関数とすると、チューリング機械で計算でき（定理 6.2［計算可能性］）、クリーネの標準形定理（定理 5.3［計算可能性］）により

$$\varphi(\vec x)=U\bigl(\mathrm{Conf}(e,\vec x,\ \mu t\,[T_k(e,\vec x,t)])\bigr)$$

と書ける。$T_k,U,\mathrm{Conf}$ は原始再帰的で、$\varphi$ が全関数だから各 $\vec x$ について $T_k(e,\vec x,t)$ となる $t$ が存在する。したがって $\mu$ は $T_k$ の否定の特性関数 $1\dot-\chi_{T_k}$ への正則な最小化であり、$\varphi$ はこの族に属する。

∎

次の証明の見どころは最小化です。「$y=0,1,2,\ldots$ と順に $g(\vec n,y)=0$ を試し、最初に成り立った $y$ を返す」という繰り返しを、不動点（§5）を使って $W\,\overline k=$「$g(\vec n,k)=0$ なら $\overline k$、そうでなければ $W\,\overline{k+1}$」という形の項で書きます。長い項 $W_{\vec x}$ は、この if 文（$\mathsf{Z}$ と $\mathsf{T},\mathsf{F}$）に、自分を呼び直す $w$ を $\lambda w$ で受け取らせたものにすぎません。

証明（定理 6.4）

(再帰的 ⇒ λ 定義可能) 補題 6.5 の生成規則ごとに、λ 定義可能な関数の族が閉じていることを示す。以下 $\vec x$ は変数の列 $x_1\cdots x_k$、$\vec{\overline n}$ は数の列 $\overline{n_1}\cdots\overline{n_k}$ を表す。

• 基本関数：ゼロは $\lambda x.\overline0$、後者は $\mathsf{S}$（補題 6.2）、射影 $P^k_i$ は $\lambda\vec x.x_i$。
• 合成：$G,H_1,\ldots,H_m$ が $g,h_1,\ldots,h_m$ を定義するなら、$F\equiv\lambda\vec x.G(H_1\vec x)\cdots(H_m\vec x)$ について $F\vec{\overline n}\twoheadrightarrow_\beta G(H_1\vec{\overline n})\cdots(H_m\vec{\overline n})=_\beta G\,\overline{h_1(\vec n)}\cdots\overline{h_m(\vec n)}=_\beta\overline{g(\vec h(\vec n))}$。$=_\beta$ が項の部分の置き換えと両立することを使っている。
• 原始再帰：$f(\vec n,0)=g(\vec n)$、$f(\vec n,y+1)=h(\vec n,y,f(\vec n,y))$ で、$G,H$ が $g,h$ を定義するとする。$T_{\vec x}\equiv\lambda p.\langle\mathsf{S}(\pi_1p),\,H\vec x(\pi_1p)(\pi_2p)\rangle$ とおき、$\vec x$ に $\vec{\overline n}$ を代入したものを $T$ と書く。$y$ に関する帰納法で $\overline yT\langle\overline0,G\vec{\overline n}\rangle=_\beta\langle\overline y,\overline{f(\vec n,y)}\rangle$ を示す。$y=0$ は $\overline0TP\twoheadrightarrow_\beta P$ と $G\vec{\overline n}=_\beta\overline{g(\vec n)}$ から。$y\to y+1$ は

$$\overline{y+1}\,TP=_\beta T(\overline yTP)=_\beta T\langle\overline y,\overline{f(\vec n,y)}\rangle=_\beta\langle\mathsf{S}\,\overline y,\ H\vec{\overline n}\,\overline y\,\overline{f(\vec n,y)}\rangle=_\beta\langle\overline{y+1},\overline{f(\vec n,y+1)}\rangle.$$

よって $F\equiv\lambda\vec xy.\pi_2(yT_{\vec x}\langle\overline0,G\vec x\rangle)$ が $f$ を定義する。

• 正則な最小化：$f(\vec n)=\mu y[g(\vec n,y)=0]$ で、$G$ が $g$ を定義するとする。$W_{\vec x}\equiv\Theta\bigl(\lambda wy.\mathsf{Z}(G\vec xy)\,y\,(w(\mathsf{S}y))\bigr)$ とおき、$\vec x:=\vec{\overline n}$ としたものを $W$ と書く。$\Theta W'\twoheadrightarrow_\beta W'(\Theta W')$（$\Theta\equiv AA$、$A\equiv\lambda xy.y(xxy)$ なので $\Theta W'\equiv AAW'\to_\beta(\lambda y.y(AAy))W'\to_\beta W'(AAW')$）から

$$W\,\overline k=_\beta\mathsf{Z}(G\vec{\overline n}\,\overline k)\,\overline k\,(W(\mathsf{S}\,\overline k))=_\beta\mathsf{Z}\,\overline{g(\vec n,k)}\,\overline k\,(W\,\overline{k+1}).$$

$g(\vec n,k)=0$ なら右辺は $\mathsf{T}\,\overline k\,(\cdots)=_\beta\overline k$、そうでなければ $\mathsf{F}\,\overline k\,(W\overline{k+1})=_\beta W\overline{k+1}$。$y_0=f(\vec n)$ は $g(\vec n,y)=0$ となる最小の $y$ なので、$W\overline0=_\beta W\overline1=_\beta\cdots=_\beta W\overline{y_0}=_\beta\overline{y_0}$。よって $F\equiv\lambda\vec x.W_{\vec x}\overline0$ が $f$ を定義する。

(λ 定義可能 ⇒ 再帰的) λ 項をゲーデル数で符号化する（定義 4.1［ゲーデルの不完全性定理］ と同じ素数冪の方法で、変数 $v_i$、適用、抽象を符号化する）。次の 3 つが原始再帰的であること（補題 6.6）を使う。(a) $\mathrm{Red}(a,b)$：「$b$ は $a$ から束縛変数の付け替え 1 回か、捕獲の起きない β 基の縮約 1 回で得られる項の符号」（補題 6.6 の 1。その 2 の (i)(ii) により、$\mathrm{Red}$ の列は $\twoheadrightarrow_\beta$ をちょうど表す）。(b) $\mathrm{Num}(b)$：「$b$ はあるチャーチ数（と α 同値な項）の符号」と、そのときの値 $\mathrm{val}(b)$（同 3）。(c) $\vec n\mapsto\ulcorner F\vec{\overline n}\urcorner$（同 4）。これらから「$s$ は $\ulcorner F\vec{\overline n}\urcorner$ から始まり $\mathrm{Red}$ でつながり、チャーチ数で終わる列の符号」という述語 $R(\vec n,s)$ も原始再帰的になる（命題 3.2［計算可能性］ の有界量化と復号 $(s)_i$）。

$F\vec{\overline n}=_\beta\overline{\varphi(\vec n)}$ で $\overline{\varphi(\vec n)}$ は正規形だから、系 4.6 (2) により $F\vec{\overline n}\twoheadrightarrow_\beta\overline{\varphi(\vec n)}$。したがって 補題 6.6 の 2 (ii) により、各 $\vec n$ について $R(\vec n,s)$ を満たす $s$ が存在する。さらに、そのような列が到達するチャーチ数は、同じく 2 (i) により $F\vec{\overline n}$ から $\twoheadrightarrow_\beta$ で到達する正規形なので、正規形の一意性によって $\overline{\varphi(\vec n)}$ に限る。ゆえに

$$\varphi(\vec n)=\mathrm{val}\bigl(\text{列 }\mu s\,[R(\vec n,s)]\text{ の最後の項}\bigr)$$

であり、正則な最小化と原始再帰関数の合成なので $\varphi$ は再帰関数である。

∎

次の補題は、簡約の列を自然数で表し、「ある列が簡約として正しいか」を原始再帰関数で判定できることを示すものです。計算可能性の章でチューリング機械の 1 ステップを数で表したのと同じ作業を、λ 項について行います。証明の中の累積帰納法は、「小さい符号での値を全部使って次の値を決める」再帰の形を、原始再帰に直すための道具です。細部が多いので、まず補題の主張だけ読み、全体の流れは上の説明で追うのがよいでしょう。

補題 6.6（β 簡約の算術化）✓

変数を $v_0,v_1,\ldots$ とし、（α 同値で同一視する前の）項に符号を $\ulcorner v_i\urcorner=\langle0,i\rangle$、$\ulcorner PQ\urcorner=\langle1,\ulcorner P\urcorner,\ulcorner Q\urcorner\rangle$、$\ulcorner\lambda v_i.P\urcorner=\langle2,i,\ulcorner P\urcorner\rangle$ で与える（$\langle x_0,\ldots,x_k\rangle=\prod_{j\le k}p_j^{x_j+1}$）。$\mathrm{Red}(a,b)$ を「$a$ は項の符号で、$b$ は、$a$ の項の部分項 1 つを、(α) $\lambda v_j.P$ と $\lambda v_k.P[v_j:=v_k]$（$v_k$ は $P$ に現れない変数）の一方から他方に付け替えるか、(β) β 基 $(\lambda v_i.M)N$ で $M$ のどの $\lambda v_j$（$v_j\in\mathrm{FV}(N)$）の作用域にも自由な $v_i$ がないものを、$M$ の自由な $v_i$ を $N$ に置き換えた項に縮約して得られる項の符号」とする。ここで §2 の α 同値（束縛変数の付け替えで移り合うこと）は、(α) の付け替えを部分項に有限回施して移り合うこと、と精密に読む（Barendregt の教科書の定義と同じ）。このとき

1. $\mathrm{Red}$ は原始再帰的である。
2. (i) 符号 $a$ から符号 $b$ まで $\mathrm{Red}$ の有限列でつながるならば、$a$ の表す項は $b$ の表す項に $\twoheadrightarrow_\beta$ で簡約される。(ii) $M\twoheadrightarrow_\beta N$ ならば、$M$ の任意の表し方の符号 $a$ から、$N$ のある表し方の符号まで $\mathrm{Red}$ の有限列でつながる。
3. $\mathrm{Num}(b)$「$b$ はあるチャーチ数と α 同値な項の符号」と、そのときの値 $\mathrm{val}(b)$（$\mathrm{Num}(b)$ でなければ $0$）は原始再帰的である。
4. 閉項 $F$ を固定すると、$\vec n\mapsto\ulcorner F\vec{\overline n}\urcorner$ は原始再帰的である。

証明（補題 6.6）

道具は 命題 3.2［計算可能性］ です。符号の第 $j$ 成分は $(w)_j\dot-1$ で取り出せ、$p_j^{x+1}\gt x$ なので各成分は元の符号より真に小さい。項の符号であるかどうか、種類（$0,1,2$）、成分は、以下の累積帰納法で原始再帰的に判定・計算できます。

累積帰納法。 $g$ が原始再帰的で $f(\vec x,w)=g(\vec x,w,\hat f(\vec x,w))$、$\hat f(\vec x,w)=\prod_{u\lt w}p_u^{f(\vec x,u)+1}$（$w$ 未満での値の履歴）と定まる $f$ は原始再帰的です。実際 $\hat f(\vec x,0)=1$、$\hat f(\vec x,w+1)=\hat f(\vec x,w)\cdot p_w^{g(\vec x,w,\hat f(\vec x,w))+1}$ は原始再帰で、$f(\vec x,w)=(\hat f(\vec x,w+1))_w\dot-1$ です。$u\lt w$ での値は $(\hat f(\vec x,w))_u\dot-1$ として $g$ の中で使えます。以下の定義はどれも、値を真に小さい符号での値から場合分け（同 2）で決めるので、この形に入ります。パラメータ（$i,c,x,y$ など）は再帰の間固定です。

基本の関数。 $\mathrm{Tm}(a)$「$a$ は項の符号」は、$a=\langle0,k\rangle$ であるか、$a=\langle1,P,Q\rangle$ で $\mathrm{Tm}(P)\wedge\mathrm{Tm}(Q)$ か、$a=\langle2,j,P\rangle$ で $\mathrm{Tm}(P)$ であること（$k,j,P,Q$ は $a$ の成分）で、累積帰納法です。$\mathrm{Occ}(a,k)$「$v_k$ が $a$ に（束縛の位置も含めて）現れる」、$\mathrm{Fr}(a,k)$「$v_k$ が $a$ に自由に現れる」は成分についての累積帰納法です（たとえば $\mathrm{Fr}(\langle2,j,P\rangle,k)\iff j\ne k\wedge\mathrm{Fr}(P,k)$）。捕獲が起きない条件 $\mathrm{FF}(a,i,c)$ を $\mathrm{FF}(\langle0,k\rangle)$ は真、$\mathrm{FF}(\langle1,P,Q\rangle)\iff\mathrm{FF}(P)\wedge\mathrm{FF}(Q)$、$\mathrm{FF}(\langle2,i,P\rangle)$ は真、$j\ne i$ なら $\mathrm{FF}(\langle2,j,P\rangle)\iff(\neg\mathrm{Fr}(P,i)\vee\neg\mathrm{Fr}(c,j))\wedge\mathrm{FF}(P)$ で定めます。付け替えのない置換 $\mathrm{sb}(a,i,c)$ を

$$\mathrm{sb}(\langle0,i\rangle)=c,\quad\mathrm{sb}(\langle0,k\rangle)=\langle0,k\rangle\ (k\ne i),\quad\mathrm{sb}(\langle1,P,Q\rangle)=\langle1,\mathrm{sb}(P),\mathrm{sb}(Q)\rangle,$$$$\mathrm{sb}(\langle2,i,P\rangle)=\langle2,i,P\rangle,\quad\mathrm{sb}(\langle2,j,P\rangle)=\langle2,j,\mathrm{sb}(P)\rangle\ (j\ne i)$$

で定めます。右辺の再帰呼び出しはすべて $a$ の成分（$a$ より小さい）なので、累積帰納法で原始再帰的です。

$a,c$ が項 $M,N$ の符号で $\mathrm{FF}(a,i,c)$ ならば、$\mathrm{sb}(a,i,c)$ は 定義 2.2 の $M[v_i:=N]$ の表し方の符号です。$a$ についての帰納法で確かめます。まず、$v_i$ が $a$ に自由に現れなければ、$\mathrm{sb}(a,i,c)=a$（$a$ についての帰納法）かつ $M[v_i:=N]\equiv M$（定義 2.2 の各式に沿った帰納法）です。変数と適用の場合は 定義 2.2 の式どおりです。$a=\langle2,j,P\rangle$ で $j\ne i$ かつ $v_j\notin\mathrm{FV}(N)$ なら、定義 2.2 の最後の式がそのまま使え、$\mathrm{FF}(P,i,c)$ なので $P$ に帰納法の仮定が使えます。残りは $j=i$ の場合と、$j\ne i$ かつ $v_j\in\mathrm{FV}(N)$ の場合です。前者では $v_i$ は $a$ に自由に現れず、後者では $\mathrm{FF}$ の定義により $v_i$ は $P$ に自由に現れないので、やはり $a$ に自由に現れません。どちらも最初に述べたことに帰着します。

部分項の置き換え。 $\mathrm{Rp}(a,b,x,y)$「$b$ は $a$ の部分項 $x$ の 1 か所を $y$ に置き換えたもの」は、$a=x\wedge b=y$、または $a=\langle1,P,Q\rangle$、$b=\langle1,P',Q'\rangle$ で（$\mathrm{Rp}(P,P',x,y)\wedge Q'=Q$）か（$P'=P\wedge\mathrm{Rp}(Q,Q',x,y)$）、または $a=\langle2,j,P\rangle$、$b=\langle2,j,P'\rangle$ で $\mathrm{Rp}(P,P',x,y)$、で定めます。再帰呼び出しでは $a$ と $b$ がともに成分に置き換わるので、$w=2^a3^b$ についての累積帰納法（$2^P3^{P'}\lt2^a3^b$）で原始再帰的です。

1. 部分項は元の項以下の符号をもつので、

$$\mathrm{Red}(a,b)\iff\mathrm{Tm}(a)\wedge\exists x\le a\ \exists y\le b\ \bigl[\mathrm{Rp}(a,b,x,y)\wedge(A(x,y)\vee A(y,x)\vee B(x,y))\bigr]$$

と有界量化で書けます。ここで $A(x,y)$ は「$x=\langle2,j,P\rangle$、$y=\langle2,k,\mathrm{sb}(P,j,\langle0,k\rangle)\rangle$、$\neg\mathrm{Occ}(P,k)$」、$B(x,y)$ は「$x=\langle1,\langle2,i,M\rangle,N\rangle$、$\mathrm{FF}(M,i,N)$、$y=\mathrm{sb}(M,i,N)$」で、$j,k,P,i,M,N$ はいずれも $x$ または $y$ 以下の範囲の有界量化で取れます。$v_k$ が $P$ に現れなければ $v_k$ について捕獲は起きないので、$A$ の $y$ は $x$ と α 同値です。

2. α 同値を上のように読むので、部分項を α 同値な項に取り替えても全体の α 同値類は変わりません。

(i) (α) の 1 ステップは α 同値類を変えません。(β) の 1 ステップは、表し方の中に文字どおり現れる β 基 $(\lambda v_i.M)N$（$\mathrm{FF}(M,i,N)$）を、上で見たとおり $M[v_i:=N]$ の表し方 $\mathrm{sb}(M,i,N)$ に取り替えるので、表す項は 定義 3.1 の 1 ステップの β 簡約で移ります（定義 3.1 の $\to_\beta$ は適用・抽象の文脈で閉じている）。よって列の長さについての帰納法で、$a$ の表す項は $b$ の表す項に $\twoheadrightarrow_\beta$ で簡約されます。

(ii) $\twoheadrightarrow_\beta$ のステップ数についての帰納法により、$M\to_\beta M_1$ の場合に、$M$ の任意の表し方 $a$ から $M_1$ のある表し方まで $\mathrm{Red}$ の列でつながることを示せば足ります。定義 3.1 の導出に関する帰納法で（規則を使うたびに、規則に書かれた束縛変数の名前で表し方を選べば）、$M$ のある表し方 $r$ であって、$r$ の中に β 基 $(\lambda v_i.M_0)N_0$ が文字どおり現れ、それを $M_0[v_i:=N_0]$ の表し方に取り替えると $M_1$ の表し方になるものがとれます。ただし $r$ は $a$ と同じとは限りません。そこで次の 3 段でつなぎます。

• $a$ と $r$ は α 同値なので、α 同値の読み方により (α) の付け替え（両向き）の有限列で $a$ から $r$ に移れます。これは $\mathrm{Red}$ の列です。
• $r$ の中で、$M_0$ の束縛変数 $\lambda v_j$ を一つずつ、そのときの項のどこにも現れない新しい変数に (α) で付け替えます（変数は無限個あるので取れる）。得られる $M_0'$ は $M_0$ と α 同値で、そのどの束縛変数も $N_0$ に自由に現れないので $\mathrm{FF}(M_0',i,N_0)$ が成り立ちます。
• (β) の 1 ステップで β 基 $(\lambda v_i.M_0')N_0$ を $\mathrm{sb}(M_0',i,N_0)$ に取り替えます。これは $M_0'[v_i:=N_0]\equiv M_0[v_i:=N_0]$ の表し方なので、得られる項は $r$ の β 基を $M_0[v_i:=N_0]$ の表し方に取り替えたもの、すなわち $M_1$ の表し方です。

3. チャーチ数 $\overline n=\lambda f.\lambda x.f^nx$ と α 同値な項は、$\lambda v_i.\lambda v_j.T$ で $T$ が $v_i$ を $v_j$ に $n$ 回適用した項 $v_i(v_i(\cdots(v_iv_j)))$ であり、$n\ge1$ なら $i\ne j$ であるもの（$n=0$ なら $T=v_j$ で $i=j$ でもよい）にちょうど限ります（この形は (α) の付け替えで保たれ、$n$ が同じこの形の項どうしは (α) の付け替えで移り合う）。$T$ がこの形かどうかと回数 $n$ は、$t=\langle0,j\rangle$ なら回数 $0$、$t=\langle1,\langle0,i\rangle,t'\rangle$ なら $t'$ の回数 $+1$、それ以外は「この形でない」という累積帰納法（パラメータ $i,j$）で原始再帰的に計算でき、$i,j,T$ は $b$ の成分として取り出せます。

4. $\nu(0)=\langle0,1\rangle$、$\nu(n+1)=\langle1,\langle0,0\rangle,\nu(n)\rangle$ とおくと、$\ulcorner\overline n\urcorner=\langle2,0,\langle2,1,\nu(n)\rangle\rangle$ は $n$ の原始再帰で定まります。$\ulcorner F\vec{\overline n}\urcorner=\langle1,\cdots\langle1,\langle1,\ulcorner F\urcorner,\ulcorner\overline{n_1}\urcorner\rangle,\ulcorner\overline{n_2}\urcorner\rangle\cdots,\ulcorner\overline{n_k}\urcorner\rangle$ は定数 $\ulcorner F\urcorner$ とこれらの合成です。

∎

注意 6.7（簡約の算術化について）

$\mathrm{Red}$ の原始再帰性は、計算可能性 でチューリング機械の 1 ステップを算術化した 補題 5.2［計算可能性］ と同じ型の作業です。補題 6.6 の証明の要点は、捕獲を避けるための束縛変数の付け替えを置換の中で行わず、(α) の独立した 1 ステップとして $\mathrm{Red}$ に入れたことです。付け替えを置換の中で行うと、付け替えた後の項は元の項の部分項ではないので、部分項の符号についての累積帰納法がそのままでは使えません。

定理 6.4 と 計算可能性 の 定理 6.3［計算可能性］ を合わせると、チューリング計算可能・再帰的・λ 定義可能の三つが一致します。チャーチがこの一致を根拠に「計算可能 = λ 定義可能」と提唱したのが、チャーチ＝チューリングの提唱の起源です。停止問題の決定不能性（定理 7.2［計算可能性］）も λ 計算の言葉に移り、「与えられた λ 項が正規形をもつか」は決定不能になります。

注意 6.8（型のない論理の矛盾）

チャーチは当初、λ 計算に論理記号を加えて論理体系を作ろうとしました。しかし型のない体系では、否定 $\neg$ を表す項 $N$ にも不動点 $X=_\beta NX$ があり、「$X$ は $X$ の否定と等しい」という嘘つきの文が作れてしまいます（クリーネとロッサーが 1935 年に矛盾を示しました）。不動点定理は計算には恵みですが、論理には毒です。次章では型を付けて自己適用を禁じ、その代わりにすべての計算が止まる（強正規化）体系を得ます。

7. 演習

演習 7.1易

$\mathsf{add}\equiv\lambda mnfx.mf(nfx)$ について、$\mathsf{add}\,\overline m\,\overline n\twoheadrightarrow_\beta\overline{m+n}$ を示せ。

解答

$\mathsf{add}\,\overline m\,\overline n\twoheadrightarrow_\beta\lambda fx.\overline mf(\overline nfx)\twoheadrightarrow_\beta\lambda fx.\overline mf(f^nx)\twoheadrightarrow_\beta\lambda fx.f^m(f^nx)\equiv\lambda fx.f^{m+n}x\equiv\overline{m+n}$。各段で、$\overline kFX\twoheadrightarrow_\beta F^kX$ を内側の項に使っている（簡約は部分項の中でも行える）。§6 の Lean のコードの add は、この項に型を付けたものです。

演習 7.2標準

$M\equiv(\lambda x.xx)(Iz)$ とする（$I\equiv\lambda y.y$）。$M\to_\beta N_1$、$M\to_\beta N_2$ となる二つの項 $N_1,N_2$ で、「$N_1$ と $N_2$ がどちらも高々 1 ステップで同じ項に簡約される」ことのないものを挙げよ。これは 1 ステップの $\to_\beta$ が菱形性をもたないことを示す。

解答

$N_1\equiv(Iz)(Iz)$（外側の β 基を縮約）、$N_2\equiv(\lambda x.xx)z$（引数の β 基を縮約）。$N_1$ から 0 または 1 ステップで行けるのは $N_1$、$z(Iz)$、$(Iz)z$ の 3 つ。$N_2$ から行けるのは $N_2$、$zz$ の 2 つ。共通部分は空である。$N_1$ は 2 ステップで $zz$ に着くので、合流はするが歩数がそろわない。並行簡約なら $N_1\Rightarrow zz$ と 1 歩で行けるので、補題 4.5 の菱形が成り立つのです。

演習 7.3標準

(1) チューリングの不動点結合子 $\Theta\equiv AA$（$A\equiv\lambda xy.y(xxy)$）について、$\Theta F\twoheadrightarrow_\beta F(\Theta F)$ を示せ。(2) 不動点を使って、すべての項 $X$ について $GX=_\beta XG$ となる閉項 $G$ を作れ。

解答

(1) $\Theta F\equiv AAF\to_\beta(\lambda y.y(AAy))F\to_\beta F(AAF)\equiv F(\Theta F)$。 (2) $G\equiv\Theta(\lambda gx.xg)$ とおく。(1) より $G\twoheadrightarrow_\beta(\lambda gx.xg)G$ なので、$GX\twoheadrightarrow_\beta(\lambda gx.xg)GX\twoheadrightarrow_\beta XG$。「自分自身を引数に渡す」ような定義も、不動点を使えば名前なしで書けます。

演習 7.4難

前者関数 $\mathrm{pd}(0)=0$、$\mathrm{pd}(n+1)=n$ を λ 定義する項を、組を使って直接書け。（ヒント：$\langle a,b\rangle\mapsto\langle b,b+1\rangle$ を $n$ 回繰り返す。）

解答

$T\equiv\lambda p.\langle\pi_2p,\mathsf{S}(\pi_2p)\rangle$、$\mathsf{P}\equiv\lambda n.\pi_1(nT\langle\overline0,\overline0\rangle)$ とおく。$n$ に関する帰納法で $\overline nT\langle\overline0,\overline0\rangle=_\beta\langle\overline{\mathrm{pd}(n)},\overline n\rangle$ を示す。$n=0$ は $\overline0TP\twoheadrightarrow_\beta P$。$n\to n+1$：$\overline{n+1}TP=_\beta T(\overline nTP)=_\beta T\langle\overline{\mathrm{pd}(n)},\overline n\rangle=_\beta\langle\overline n,\mathsf{S}\,\overline n\rangle=_\beta\langle\overline{\mathrm{pd}(n+1)},\overline{n+1}\rangle$。よって $\mathsf{P}\,\overline n=_\beta\overline{\mathrm{pd}(n)}$。チャーチ数は「繰り返す」ことしかできないので、1 を引くには一つ遅れた値を持ち歩く工夫が要ります。クリーネはこの構成を思いついたことで、λ 定義可能な関数の範囲が広いことを確信したと伝えられています。

参考文献

• H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, revised ed., North-Holland, 1984 — 第 2・3 章（簡約とチャーチ＝ロッサー）、第 6 章（不動点）、第 13 章（正規化）。
• J. R. Hindley and J. P. Seldin, Lambda-Calculus and Combinators: An Introduction, Cambridge University Press, 2008 — 第 1〜4 章。
• M. Takahashi, “Parallel reductions in λ-calculus”, Information and Computation 118 (1995), 120–127.
• A. Church and J. B. Rosser, “Some properties of conversion”, Transactions of the American Mathematical Society 39 (1936), 472–482.
• S. C. Kleene, “λ-definability and recursiveness”, Duke Mathematical Journal 2 (1936), 340–353.