markdown
λ計算の基本
lecture/information/programming-languages/lambda-calculus/ラムダ計算の基本-講義.n.md
λ計算の基本
informationprogramming-languageslambda-calculuslecture
導入
この講義の核心は、「計算とは関数適用の繰り返しであり、関数適用の実体は置換である」という点にある。λ計算は、変数・関数の定義・関数の適用という 3 つの概念だけで、すべての計算可能な操作を表現できる最小の計算モデルである。
中心課題
(\lambda x. \lambda y. x) \; a \; b はどのように計算が進み、何に至るか。「計算が進む」とはどういうことか。
用語
- λ計算: 変数・λ抽象・適用の 3 規則で定義される計算モデル
- β簡約: (\lambda x. t) \; s \to_\beta t[x := s] という計算の 1 ステップ
- 簡約基: β簡約が適用できる部分の形 (\lambda x. t) \; s
- 正規形: これ以上β簡約できない項
- η変換: \lambda x. (f \; x) =_\eta f（x \notin \mathrm{FV}(f) のとき）
方針
まずλ項の構文（BNF）を確認する。つぎにβ簡約の規則を一段ずつ追う。最後にη変換の意味（外延性）を加える。評価戦略（どの簡約基を先に選ぶか）はこの講義では扱わず、別講義に委ねる。
直感的な説明
(\lambda x. t) \; s は「t の中の x を s で置き換える」ことで計算が一歩進む。これがβ簡約である。
(λx. λy. x) a b
→β (λy. a) b ← 外側の λx に a を渡した（x を a に置換）
→β a ← 内側の λy に b を渡した（y は出現しないので b は捨てられる）
「計算が進む」とは「簡約基を選び、置換を実行する」ことである。計算が止まるとは「正規形に到達する」ことである。
厳密な説明
1. λ項の構文（再掲）
t ::= x \mid \lambda x. t \mid t_1 \; t_2
2. β簡約
\frac{}{(\lambda x. t) \; s \to_\beta t[x := s]}\ (\text{β})
この規則は項のどこに現れる簡約基にも適用できる。
文脈での簡約: t \to_\beta t' ならば
\frac{t \to_\beta t'}{t \; s \to_\beta t' \; s}, \quad \frac{t \to_\beta t'}{s \; t \to_\beta s \; t'}, \quad \frac{t \to_\beta t'}{\lambda x. t \to_\beta \lambda x. t'}
3. η変換
\lambda x. (f \; x) =_\eta f \quad (x \notin \mathrm{FV}(f))
η変換は「f と \lambda x. (f \; x) は外延的に同じ関数だ」という主張である。どんな引数を渡しても同じ結果になるなら、「関数として等しい」とみなせる。
4. α・β・η のまとめ
| 操作 | 意味 |
|---|
| α変換 | 束縛変数の改名（意味を変えない） |
| β簡約 | 関数適用の展開（計算の 1 歩） |
| η変換 | 外延的同一性（関数の等価性） |
最小の具体例
例 1: 恒等関数
(\lambda x. x) \; a \to_\beta a
I = \lambda x. x（恒等関数）と名前を付けると I \; a \to_\beta a。
例 2: 定数関数
(\lambda x. \lambda y. x) \; a \; b
\to_\beta (\lambda y. a) \; b
\to_\beta a
一番目の引数だけを返す関数。K = \lambda x. \lambda y. x と書く（K コンビネータ）。
例 3: 正規形に至らない項
\Omega = (\lambda x. x \; x) \; (\lambda x. x \; x)
\to_\beta (\lambda x. x \; x) \; (\lambda x. x \; x) = \Omega
\Omega はβ簡約するとまた \Omega に戻る。正規形が存在しない項の例である。型無しλ計算では任意の計算が停止するとは限らない。
別の見方
λ計算はチューリング機械と計算能力が等しい（チャーチ–チューリングテーゼ）。チューリング機械が「テープの状態を遷移させる」計算モデルであるのに対し、λ計算は「式の変形規則の連鎖」という計算モデルである。前者は物理的な操作に近く、後者は数学的な書き換えに近い。
見分け方
- (\lambda x. \ldots) \; s という形がβ簡約基である
- \lambda x. (f \; x) の形で x が f に現れないならη変換の対象
- 正規形かどうかは「β簡約基が存在するか」で判定する
一言でいうと
λ計算とは「変数・関数定義・関数適用」の 3 要素だけで計算を記述する体系であり、計算の 1 ステップは (\lambda x. t) \; s \to_\beta t[x := s] という置換で与えられる。