λ計算入門 — 型なしから単純型付きへ
計算の最小モデル
初級（大学1-2年レベル）
このページの目標
関数の定義と適用だけからなる型なし λ計算と β簡約を理解し、項に型を与える単純型付き λ計算へ進む。なぜ型を付けると計算が必ず止まるのか、その意義をつかむ。
1. 型なし λ計算
λ計算は、関数を作ることと使うことだけで計算を表す、極限まで切り詰めた計算モデルである。項は次の三つだけから作られる。
- 変数：$x, y, z, \dots$
- 抽象：$\lambda x.\,M$（$x$ を受け取り $M$ を返す関数）
- 適用：$M\,N$（関数 $M$ に引数 $N$ を渡す）
たったこれだけだが、自然数・真偽値・データ構造・再帰まで符号化でき、チューリング機械と同じ計算能力を持つ。変数の束縛は 束縛変数と自由変数 と同じ考え方で、$\lambda x.\,M$ の $x$ は束縛変数、名前は付け替えられる（$\alpha$ 変換）。
2. β簡約：計算の一歩
関数適用 $(\lambda x.\,M)\,N$ を、$M$ の中の自由な $x$ をすべて $N$ で置き換えた式 $M[x := N]$ に書き換える操作を β簡約という。
$$(\lambda x.\,M)\,N \;\to_\beta\; M[x := N]$$恒等関数 $\mathrm{id} = \lambda x.\,x$ に $y$ を渡すと、$x$ を $y$ に置き換えて $y$ になる。
$$(\lambda x.\,x)\,y \;\to_\beta\; y$$「$2$ 倍して $1$ 足す」を表す $\lambda x.\,(x+x+1)$ に $3$ を渡せば、$3+3+1 = 7$ に簡約される。β簡約はプログラムの実行そのものである。
これ以上 β簡約できない形を正規形という。正規形は「計算が終わった状態」にあたる。ただし型なしでは、簡約が永遠に終わらない項も書ける。たとえば $(\lambda x.\,x\,x)(\lambda x.\,x\,x)$ は、関数 $\lambda x.\,x\,x$（「引数を自分自身に適用する」関数）を、引数としてその関数自身に渡したものである。β簡約すると本体 $x\,x$ の $x$ が $\lambda x.\,x\,x$ に置き換わり、$(\lambda x.\,x\,x)(\lambda x.\,x\,x)$ というまったく同じ形に戻る。これが延々と繰り返されるので、計算は永遠に止まらず正規形に達しない。
3. 単純型付き λ計算
計算が止まらないのは困る場面が多い。そこで各項に型を割り当て、型の合う適用しか許さないのが単純型付き λ計算である。型は基本型と関数型 $A \to B$ から作る。
記法：項のうしろにコロンを付けて型を書く。$M : B$ は「$M$ の型は $B$（$M$ は型 $B$ を持つ）」と読む。同様に $x : A$ は「$x$ の型は $A$」、$\lambda x{:}A.\,M$ は「型 $A$ の引数 $x$ を受け取る関数」を表す。横線の上の $x:A \vdash M:B$ は「$x$ を型 $A$ と仮定すると、$M$ は型 $B$ を持つ」と読む（$\vdash$ は 構文と意味 で見た「〜から導ける」）。
規則は前章の 自然演繹 と同じ横線の形で、「横線の上が言えれば、下が言える」と読む。覚える規則は次の 2 つだけである。
① 適用の規則（関数を使う）：関数 $M$ の型が $A \to B$（型 $A$ を受け取り型 $B$ を返す）で、引数 $N$ の型が $A$ なら、適用 $M\,N$ の型は $B$ になる。
$$\dfrac{M : A \to B \quad N : A}{M\,N : B}$$② 抽象の規則（関数を作る）：引数 $x$ を「型 $A$ である」と仮定したとき、本体 $M$ の型が $B$ になるなら、その関数 $\lambda x{:}A.\,M$ の型は $A \to B$ である。横線の上の $x:A \vdash M:B$ が「$x:A$ と仮定すれば $M:B$」を表す。
$$\dfrac{x:A \;\vdash\; M:B}{\lambda x{:}A.\,M \;:\; A \to B}$$自然数の型を $\mathbb{N}$ とする（$A, B$ のような抽象的な型を実際の型に置き換えて読む）。例として「1 を足す関数」 $f = \lambda x{:}\mathbb{N}.\,(x+1)$ を使う。この関数が「何をするか」は、$\lambda$ の本体 $x+1$ に書かれている。
- 抽象（$f$ の型を決める）：$x : \mathbb{N}$ と仮定すると、本体 $x+1$ の型は $\mathbb{N}$。ゆえに $f = \lambda x{:}\mathbb{N}.\,(x+1)$ の型は $\mathbb{N} \to \mathbb{N}$（規則②、$A=B=\mathbb{N}$）。
- 適用（$f$ を使う）：その $f$ に $3 : \mathbb{N}$ を渡すと $f\;3 : \mathbb{N}$。実際 $(\lambda x{:}\mathbb{N}.\,(x+1))\,3$ を β簡約すると、本体の $x$ が $3$ に置き換わって $3+1 = 4$（規則①、$A=B=\mathbb{N}$）。
このように、関数の値（$4$）は本体 $x+1$ から決まる。一方、型付けの規則は値ではなく型だけを見る（$x+1$ が $\mathbb{N}$ なら結果は $\mathbb{N}$、と型の上で計算する）。「型が合う」とは、適用の規則①で関数の入力型と引数の型が一致すること（上の例では両方 $\mathbb{N}$）。一致しなければ型が付かず、その適用は許されない。
強正規化定理（概要）
単純型付き λ計算では、型の付くすべての項について、β簡約はどんな順序で進めても必ず有限回で停止する。型を付けるだけで、止まらない計算が排除される。
$(\lambda x.\,x\,x)$ のような自己適用は、整合する型を割り当てられないため、そもそも型が付かない。型システムが「危ない項」をはじいているのである。停止性のしくみは 強正規化・停止性 で詳しく扱う。
4. 証明との対応
型付けの規則をよく見ると、自然演繹 の規則と形がそっくりである。関数の型付け規則は含意の導入・除去そのものになっている。これが Curry–Howard 対応である。
$\lambda x{:}A.\,M : A \to B$ は「$A$ を仮定して $B$ を導き、放電して $A \to B$」（$\to$I）に、$M\,N : B$ は「$A \to B$ と $A$ から $B$」（$\to$E、モーダスポネンス）に対応する。型付き λ項がそのまま証明であり、β簡約が証明の簡約（正規化）にあたる。
こうして λ計算は、単なる計算モデルを超えて、論理の証明そのものを表す言語になる。単純型付き λ計算が表すのは命題論理の証明であり、量化子まで含む論理に対応させると 依存型理論 に至る。
まとめ
この章のポイント
- λ計算：変数・抽象 $\lambda x.\,M$・適用 $M\,N$ だけからなる計算の最小モデル
- β簡約：$(\lambda x.\,M)\,N \to M[x:=N]$。計算の一歩＝プログラムの実行
- 型なしでは止まらない計算も書けるが、単純型付きでは必ず停止（強正規化）
- 型付け規則は自然演繹の規則と一致し、型付き項＝証明（Curry–Howard）
よくある質問
λ計算とは何か
関数の定義と適用だけからなる計算の最小モデルである。$\lambda x.\,M$ で「$x$ を受け取って $M$ を返す関数」を表し、$(\lambda x.\,M)\,N$ を $M$ の中の $x$ を $N$ で置き換える（β簡約）ことで計算を進める。チューリング機械と同じ計算能力を持ち、関数型プログラミングと型理論の基礎である。
β簡約とは何か
関数適用 $(\lambda x.\,M)\,N$ を、$M$ の中の自由な $x$ をすべて $N$ で置き換えた式に書き換える操作である。これがλ計算における計算の一歩であり、プログラムの実行に相当する。これ以上簡約できない形を正規形という。
型なしと単純型付きの違いは何か
型なし λ計算はどんな項にも適用を許すため、自己適用など簡約が止まらない項も書ける。単純型付き λ計算は各項に型を割り当て、型の合う適用しか許さない。その結果すべての項の簡約が必ず停止する（強正規化）。この型付き版が Curry–Howard 対応で論理の証明に対応する。