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

> λ 項と β 簡約を定義し、並行簡約と完全展開によるチャーチ＝ロッサーの定理を証明する。不動点結合子で再帰を実現し、チャーチ数で再帰関数がちょうど λ 定義可能な関数であることを示す。
> https://rikai.mugen-giken.com/mathematics/logic-and-type-theory/lambda-calculus

## 0. この記事の要点

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

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

<Aside type="tip" title="この記事で使う事前知識">

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

</Aside>

## 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. **計算のモデル**。[計算可能性](/mathematics/logic-and-type-theory/computability) のチューリング機械と再帰関数に並ぶ、三つ目の定義です。三者が一致することが、チャーチ＝チューリングの提唱（<Ref to="mathematics/logic-and-type-theory/computability#rem-church-turing" />）の根拠の一つになりました。この記事で、再帰関数との一致を証明します。
2. **プログラミング言語の核**。関数型言語の評価は β 簡約そのものです。どの順に評価しても答えが同じになる、という安心感の数学的な根拠がチャーチ＝ロッサーの定理です。
3. **証明の計算的な中身**。次章で型を付けると、λ 項がそのまま自然演繹の証明になり、β 簡約が「証明の回り道を取り除く」操作になります（カリー＝ハワード対応）。Lean で `theorem` の証明として書く項は、型付きの λ 項です。

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

## 2. λ 項と置換

<Definition id="def-lambda-term" title="λ 項">
可算無限個の変数 $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\}$ で定める。自由変数をもたない項を**閉項**という。
</Definition>

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

<Definition id="def-substitution" title="置換">
$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))
$$
と定める。最後の条件は変数の規約により（束縛変数を付け替えて）いつでも満たせる。
</Definition>

なお、条件を満たすように束縛変数を付け替える手順は単純で、$\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$」のはずが恒等関数に化けるわけで、これを**変数の捕獲**といいます。

<Lemma id="lem-substitution" title="置換補題">
$x\ne y$ かつ $x\notin\mathrm{FV}(L)$ ならば、
$$
M[x:=N][y:=L]\equiv M[y:=L][x:=N[y:=L]].
$$
</Lemma>

<Proof of="lem-substitution">
$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$ についての帰納法の仮定に帰着する。
</Proof>

## 3. β 簡約

<Definition id="def-beta" title="β 簡約">
$(\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$ の正規形という。
</Definition>

<Example id="ex-reductions" title="簡約のいろいろな振る舞い">
$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$ ばかり簡約し続けると、いつまでも終わりません。

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

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

<Theorem id="thm-church-rosser" title="チャーチ＝ロッサーの定理">
$M\twoheadrightarrow_\beta N_1$ かつ $M\twoheadrightarrow_\beta N_2$ ならば、$N_1\twoheadrightarrow_\beta P$ かつ $N_2\twoheadrightarrow_\beta P$ となる項 $P$ が存在する。
</Theorem>

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

<Definition id="def-parallel" title="並行簡約と完全展開">
**並行簡約** $\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^{*}$ で定める。
</Definition>

$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 歩で追いつける、という主張です。これが菱形性そのものになり、チャーチ＝ロッサーの定理が出ます。

<Lemma id="lem-parallel-basic" title="並行簡約の基本性質">
(1) すべての $M$ で $M\Rightarrow M$。(2) $M\to_\beta N$ ならば $M\Rightarrow N$。(3) $M\Rightarrow N$ ならば $M\twoheadrightarrow_\beta N$。したがって $\twoheadrightarrow_\beta$ は $\Rightarrow$ の推移閉包に等しい。
</Lemma>

<Proof of="lem-parallel-basic">
(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) から従う。
</Proof>

<Lemma id="lem-parallel-subst" title="並行簡約と置換">
$M\Rightarrow M'$ かつ $N\Rightarrow N'$ ならば、$M[x:=N]\Rightarrow M'[x:=N']$。
</Lemma>

<Proof of="lem-parallel-subst">
$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$ は置換補題（<Ref to="lem-substitution" />。$y\notin\mathrm{FV}(N')$ を使う）である。右辺は $M'[x:=N']$ に等しい。
</Proof>

<Lemma id="lem-triangle" title="三角補題">
$M\Rightarrow N$ ならば $N\Rightarrow M^{*}$。
</Lemma>

<Proof of="lem-triangle">
$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^{*}$ と <Ref to="lem-parallel-subst" /> により $P'[x:=Q']\Rightarrow P^{*}[x:=Q^{*}]\equiv((\lambda x.P)Q)^{*}$。
</Proof>

<Proof of="thm-church-rosser">
<Ref to="lem-triangle" /> より、$M\Rightarrow N_1$ かつ $M\Rightarrow N_2$ ならば $N_1\Rightarrow M^{*}$ かつ $N_2\Rightarrow M^{*}$。つまり $\Rightarrow$ は**菱形性**（一歩ずつ分かれた二つの道が、それぞれ一歩で合流する）をもつ。

<Ref to="lem-parallel-basic" /> より、$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$ であり、<Ref to="lem-parallel-basic" /> (3) により $N_1\twoheadrightarrow_\beta P$、$N_2\twoheadrightarrow_\beta P$。
</Proof>

<Figure caption="チャーチ＝ロッサーの証明の構造。並行簡約の菱形（左）をタイルのように敷き詰めて、任意の長さの簡約を合流させる（右）。">
<svg viewBox="0 0 640 245" width="100%" role="img" aria-label="並行簡約の菱形性と、それを格子状に敷き詰めて合流を得る図">
  <defs>
    <marker id="cr-arrow" markerWidth="8" markerHeight="8" refX="6" refY="3" orient="auto">
      <path d="M 0 0 L 6 3 L 0 6 z" fill="currentColor" />
    </marker>
    <marker id="cr-arrow-acc" markerWidth="8" markerHeight="8" refX="6" refY="3" orient="auto">
      <path d="M 0 0 L 6 3 L 0 6 z" fill="var(--sl-color-accent)" />
    </marker>
  </defs>
  <text x="120" y="24" text-anchor="middle" fill="currentColor" font-size="14">M</text>
  <text x="50" y="104" text-anchor="middle" fill="currentColor" font-size="14">N₁</text>
  <text x="190" y="104" text-anchor="middle" fill="currentColor" font-size="14">N₂</text>
  <text x="120" y="184" text-anchor="middle" fill="var(--sl-color-accent)" font-size="14">M*</text>
  <line x1="112" y1="32" x2="60" y2="88" stroke="currentColor" stroke-width="1.5" marker-end="url(#cr-arrow)" />
  <line x1="128" y1="32" x2="180" y2="88" stroke="currentColor" stroke-width="1.5" marker-end="url(#cr-arrow)" />
  <line x1="60" y1="112" x2="110" y2="168" stroke="var(--sl-color-accent)" stroke-width="1.5" stroke-dasharray="5 3" marker-end="url(#cr-arrow-acc)" />
  <line x1="180" y1="112" x2="130" y2="168" stroke="var(--sl-color-accent)" stroke-width="1.5" stroke-dasharray="5 3" marker-end="url(#cr-arrow-acc)" />
  <text x="250" y="60" fill="currentColor" font-size="12">⇒ の菱形</text>
  <g stroke="currentColor" stroke-width="1.5" fill="none">
    <line x1="440" y1="20" x2="360" y2="100" />
    <line x1="440" y1="20" x2="560" y2="140" />
  </g>
  <g stroke="var(--sl-color-accent)" stroke-width="1.2" fill="none" stroke-dasharray="4 3">
    <line x1="400" y1="60" x2="520" y2="180" />
    <line x1="360" y1="100" x2="480" y2="220" />
    <line x1="480" y1="60" x2="400" y2="140" />
    <line x1="520" y1="100" x2="440" y2="180" />
    <line x1="560" y1="140" x2="480" y2="220" />
  </g>
  <text x="440" y="14" text-anchor="middle" fill="currentColor" font-size="13">M</text>
  <text x="344" y="104" text-anchor="middle" fill="currentColor" font-size="13">N₁</text>
  <text x="578" y="144" text-anchor="middle" fill="currentColor" font-size="13">N₂</text>
  <text x="480" y="238" text-anchor="middle" fill="var(--sl-color-accent)" font-size="13">P</text>
  <text x="630" y="60" text-anchor="end" fill="currentColor" font-size="12">破線は菱形で補う</text>
</svg>
</Figure>

<Corollary id="cor-cr" title="チャーチ＝ロッサーの帰結">
(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$ はすべての項を等しくするような自明な関係ではない。
</Corollary>

<Proof of="cor-cr">
(1) 共通の簡約先が存在すれば、途中を逆にたどって $M=_\beta N$。逆に、「共通の簡約先をもつ」という関係 $\sim$ は反射的・対称的で $\to_\beta$ を含む。推移的でもある：$M\sim N$（共通の簡約先 $P$）、$N\sim L$（共通の簡約先 $Q$）なら、$N\twoheadrightarrow_\beta P$、$N\twoheadrightarrow_\beta Q$ に <Ref to="thm-church-rosser" /> を使って $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) より β 同値でない。
</Proof>

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

<Remark id="rem-normalization" title="正規形の見つけ方">
<Ref to="ex-reductions" /> の $KI\Omega$ のように、正規形があっても簡約の順序しだいで止まらないことがあります。**最左最外**の β 基（最も左にある $\lambda$ から始まる β 基）を常に縮約する戦略をとると、正規形があれば必ずそこに到達することが知られています（正規化定理。Barendregt の教科書の第 13 章）。この記事では使わないので、証明は省略します。
</Remark>

## 5. 不動点と再帰

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

<Theorem id="thm-fixed-point" title="不動点定理">
$Y\equiv\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$ とおく。任意の項 $F$ について $YF=_\beta F(YF)$。とくに任意の $F$ に対して $FX=_\beta X$ となる $X$ が存在する。
</Theorem>

<Proof of="thm-fixed-point">
$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$ とすればよい。
</Proof>

$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$ をとればよいのです。<Ref to="thm-lambda-definable" /> の証明で、最小化をこの方法で実現します。

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

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

この節では [計算可能性](/mathematics/logic-and-type-theory/computability) に合わせて $0$ も自然数に含め、$\mathbb{N}=\{0,1,2,\ldots\}$ とします。

<Definition id="def-church-numeral" title="チャーチ数と λ 定義可能性">
$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)}
$$
となることをいう。
</Definition>

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

<Lemma id="lem-church-arith" title="チャーチ数・真偽値・組の基本項">
(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$。
</Lemma>

<Proof of="lem-church-arith">
(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$）。
</Proof>

<Example id="ex-church-arith" title="チャーチ数の演算">
- 後者 $\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$。
</Example>

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

```lean
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. 再帰関数は λ 定義可能

<Theorem id="thm-lambda-definable" title="クリーネの定理（λ 定義可能性と再帰性）">
全関数 $\varphi:\mathbb{N}^k\to\mathbb{N}$ について、$\varphi$ が再帰関数（<Ref to="mathematics/logic-and-type-theory/computability#def-mu-recursive" /> の意味で、全関数である部分再帰関数）であることと、λ 定義可能であることは同値である。
</Theorem>

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

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

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

<Proof of="lem-total-recursive">
この族の元は明らかに全関数である部分再帰関数である。逆に $\varphi$ を再帰関数とすると、チューリング機械で計算でき（<Ref to="mathematics/logic-and-type-theory/computability#thm-recursive-to-tm" />）、クリーネの標準形定理（<Ref to="mathematics/logic-and-type-theory/computability#thm-normal-form" />）により
$$
\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$ はこの族に属する。
</Proof>

次の証明の見どころは最小化です。「$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$ で受け取らせたものにすぎません。

<Proof of="thm-lambda-definable">
**(再帰的 ⇒ λ 定義可能)** <Ref to="lem-total-recursive" /> の生成規則ごとに、λ 定義可能な関数の族が閉じていることを示す。以下 $\vec x$ は変数の列 $x_1\cdots x_k$、$\vec{\overline n}$ は数の列 $\overline{n_1}\cdots\overline{n_k}$ を表す。

- 基本関数：ゼロは $\lambda x.\overline0$、後者は $\mathsf{S}$（<Ref to="lem-church-arith" />）、射影 $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$ を定義する。

**(λ 定義可能 ⇒ 再帰的)** λ 項をゲーデル数で符号化する（<Ref to="mathematics/logic-and-type-theory/incompleteness-theorems#def-godel-numbering" /> と同じ素数冪の方法で、変数 $v_i$、適用、抽象を符号化する）。次の 3 つが原始再帰的であること（<Ref to="lem-lambda-coding" />）を使う。(a) $\mathrm{Red}(a,b)$：「$b$ は $a$ から束縛変数の付け替え 1 回か、捕獲の起きない β 基の縮約 1 回で得られる項の符号」（<Ref to="lem-lambda-coding" /> の 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)$ も原始再帰的になる（<Ref to="mathematics/logic-and-type-theory/computability#prop-pr-toolbox" /> の有界量化と復号 $(s)_i$）。

$F\vec{\overline n}=_\beta\overline{\varphi(\vec n)}$ で $\overline{\varphi(\vec n)}$ は正規形だから、<Ref to="cor-cr" /> (2) により $F\vec{\overline n}\twoheadrightarrow_\beta\overline{\varphi(\vec n)}$。したがって <Ref to="lem-lambda-coding" /> の 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$ は再帰関数である。
</Proof>

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

<Lemma id="lem-lambda-coding" title="β 簡約の算術化">
変数を $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$ は原始再帰的である。
</Lemma>

<Proof of="lem-lambda-coding">
道具は <Ref to="mathematics/logic-and-type-theory/computability#prop-pr-toolbox" /> です。符号の第 $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)$ は <Ref to="def-substitution" /> の $M[v_i:=N]$ の表し方の符号です。$a$ についての帰納法で確かめます。まず、$v_i$ が $a$ に自由に現れなければ、$\mathrm{sb}(a,i,c)=a$（$a$ についての帰納法）かつ $M[v_i:=N]\equiv M$（<Ref to="def-substitution" /> の各式に沿った帰納法）です。変数と適用の場合は <Ref to="def-substitution" /> の式どおりです。$a=\langle2,j,P\rangle$ で $j\ne i$ かつ $v_j\notin\mathrm{FV}(N)$ なら、<Ref to="def-substitution" /> の最後の式がそのまま使え、$\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)$ に取り替えるので、表す項は <Ref to="def-beta" /> の 1 ステップの β 簡約で移ります（<Ref to="def-beta" /> の $\to_\beta$ は適用・抽象の文脈で閉じている）。よって列の長さについての帰納法で、$a$ の表す項は $b$ の表す項に $\twoheadrightarrow_\beta$ で簡約されます。

(ii) $\twoheadrightarrow_\beta$ のステップ数についての帰納法により、$M\to_\beta M_1$ の場合に、$M$ の任意の表し方 $a$ から $M_1$ のある表し方まで $\mathrm{Red}$ の列でつながることを示せば足ります。<Ref to="def-beta" /> の導出に関する帰納法で（規則を使うたびに、規則に書かれた束縛変数の名前で表し方を選べば）、$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$ とこれらの合成です。
</Proof>

<Remark id="rem-coding" title="簡約の算術化について">
$\mathrm{Red}$ の原始再帰性は、[計算可能性](/mathematics/logic-and-type-theory/computability) でチューリング機械の 1 ステップを算術化した <Ref to="mathematics/logic-and-type-theory/computability#lem-step" /> と同じ型の作業です。<Ref to="lem-lambda-coding" /> の証明の要点は、捕獲を避けるための束縛変数の付け替えを置換の中で行わず、(α) の独立した 1 ステップとして $\mathrm{Red}$ に入れたことです。付け替えを置換の中で行うと、付け替えた後の項は元の項の部分項ではないので、部分項の符号についての累積帰納法がそのままでは使えません。
</Remark>

<Ref to="thm-lambda-definable" /> と [計算可能性](/mathematics/logic-and-type-theory/computability) の <Ref to="mathematics/logic-and-type-theory/computability#thm-equivalence" /> を合わせると、チューリング計算可能・再帰的・λ 定義可能の三つが一致します。チャーチがこの一致を根拠に「計算可能 = λ 定義可能」と提唱したのが、チャーチ＝チューリングの提唱の起源です。停止問題の決定不能性（<Ref to="mathematics/logic-and-type-theory/computability#thm-halting" />）も λ 計算の言葉に移り、「与えられた λ 項が正規形をもつか」は決定不能になります。

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

## 7. 演習

<Exercise id="exr-plus" difficulty="易">
$\mathsf{add}\equiv\lambda mnfx.mf(nfx)$ について、$\mathsf{add}\,\overline m\,\overline n\twoheadrightarrow_\beta\overline{m+n}$ を示せ。
<Solution>
$\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` は、この項に型を付けたものです。
</Solution>
</Exercise>

<Exercise id="exr-diamond-fails" difficulty="標準">
$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$ が菱形性をもたないことを示す。
<Solution>
$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 歩で行けるので、<Ref to="lem-triangle" /> の菱形が成り立つのです。
</Solution>
</Exercise>

<Exercise id="exr-turing" difficulty="標準">
(1) チューリングの不動点結合子 $\Theta\equiv AA$（$A\equiv\lambda xy.y(xxy)$）について、$\Theta F\twoheadrightarrow_\beta F(\Theta F)$ を示せ。(2) 不動点を使って、すべての項 $X$ について $GX=_\beta XG$ となる閉項 $G$ を作れ。
<Solution>
(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$。「自分自身を引数に渡す」ような定義も、不動点を使えば名前なしで書けます。
</Solution>
</Exercise>

<Exercise id="exr-pred" difficulty="難">
前者関数 $\mathrm{pd}(0)=0$、$\mathrm{pd}(n+1)=n$ を λ 定義する項を、組を使って直接書け。（ヒント：$\langle a,b\rangle\mapsto\langle b,b+1\rangle$ を $n$ 回繰り返す。）
<Solution>
$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 を引くには一つ遅れた値を持ち歩く工夫が要ります。クリーネはこの構成を思いついたことで、λ 定義可能な関数の範囲が広いことを確信したと伝えられています。
</Solution>
</Exercise>

## 参考文献

- 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.