論理学入門 II — ラムダ計算と関数型言語

全体概要

本セミナー「ラムダ計算と関数型言語」は、1930〜40年代にAlonzo Churchが構築した「ラムダ計算」の理論が、20世紀後半の計算機科学、とりわけ関数型言語の誕生と発展にいかなる影響を与えたかを追跡する知的な旅程です [p.2]。

中心的な問いは「計算とは何か」という根源的な問いに端を発します。Gödel・Church・Turingがそれぞれ独立に構築した「帰納関数論」「ラムダ計算」「チューリングマシン」という三つの計算モデルが互いに同値であるという認識が、現代計算機科学の礎を形成しています [p.9], [p.10]。

セミナーは大きく「型のないラムダ計算（Part I）」と「型付きラムダ計算（Part II）」、そして「ラムダ計算とLISP・Haskell・OCaml（Part III）」「Coqでの関数型プログラミング（Part IV）」の四部構成で展開されます。Part Iでは関数の抽象化（Abstraction）・適用（Application）・代入（Substitution）という三つの基本操作を厳密に定式化し、Part IIではそれに「型」を導入することで計算が必ず停止するという重要な性質が得られることを示します [p.97]。

著者が特に強調するのは「型付きラムダ計算の登場」、すなわち「関数は型を持つ」という認識の転換が、その後のプログラム言語発展の最大の転換点であったという視座です [p.3]。型概念のさらなる拡張である「従属型理論（Dependent Type Theory）」へと射程を伸ばすことで、初めて「計算」と「論理」の深い対応関係（Curry-Howard対応）が明らかになります [p.4], [p.105], [p.106]。

実装の側面では、LISPからHaskell・OCaml・Coqに至る関数型言語の系譜を辿りながら、各言語がChurchのラムダ記法をどのような構文で継承・実装しているかを具体的なコードで比較対照します [p.182]。本セミナーは「論理学III – 計算と論理」への架け橋として位置づけられる「中間的な」作品です [p.4]。

---

講義のロードマップ

■ Part I: 型のないラムダ計算

• この部の核心:

関数という概念を「入力に対して一つの出力を返す写像」として定義し直したうえで、Churchのラムダ記法によって関数を名前なしに抽象化する手法（λ記法）を導入します [p.12], [p.19]。Abstraction・Application・Substitutionの三操作とα変換・β簡約・η変換の三規則を形式化し、型のないラムダ計算の完全な定義を与えます [p.52]。

• 論理展開:
• 関数の定義と「関数でない例」（一入力に複数出力を持つ関係はNGという明確化）[p.12], [p.15]
• λ記法による抽象化：`λx.(x+1)`、多変数のCurry化 `λxy.M = λx.(λy.M)` [p.19], [p.24], [p.25]
• β簡約の核心規則：`(λx.M) a => M[x:=a]`、適用は左結合、λ束縛は右結合 [p.52], [p.54]
• 特殊なλ式：無限ループするΩ = `(λx.xx)(λx.xx)` と不動点コンビネータY [p.56]〜[p.71]

---

■ Part II: 型付きラムダ計算

• この部の核心:

型のないラムダ計算に「型」を導入し、変数・抽象化・適用のそれぞれに型推論規則を与えます [p.76]。最大の意義は「適用は型によって制限される」という制約であり、これによりΩのような計算が排除され、全ての計算が必ず停止する（強正規化性）という重要な性質が保証されます [p.95], [p.97]。

• 論理展開:
• 型の導入：`v : τ`（項 : 型）という記法、集合の∈を:に置き換えれば集合論と対応 [p.77], [p.81]
• 抽象化の型：`x:σ`かつ`e:τ`ならば`λxσ.eτ : σ→τ` [p.82], [p.83]
• 適用の型制約：`e1 : (σ→τ)`かつ`e2 : σ`のときのみ`(e1 e2) : τ` [p.87], [p.90], [p.96]
• Curry-Howard対応の萌芽：証明を項、命題を型と同一視する解釈と命題 `A→B` の証明が関数として表現される見通し [p.102], [p.104], [p.106]

---

■ Part III: ラムダ計算とLISP・Haskell・OCaml

• この部の核心:

Churchのラムダ計算が実際の関数型言語にどのように実装されてきたかを、歴史的系譜と具体的なコードの両面から追跡します。LISPはS式というデータ構造を通じて型なしラムダ計算を忠実に実装した最初の言語であり [p.111]、HaskellとOCamlはMilnerの多相型理論（1978）を基盤に型付きラムダ計算を実用言語として結実させました [p.139]。

• 論理展開:
• LISP：S式・cons/car/cdr、LAMBDA・LABEL・COND、evalquoteによるβ簡約の実装 [p.113]〜[p.135]
• 関数型プログラミング史の要衝：Backus 1978チューリング賞講演、Milner ML 1978、FPCA 1981、Turner lazy evaluation 1981、Haskell 1987 [p.138]〜[p.145]
• Haskell：Curry化 `f::Float->Float->Float`、型クラス `class Eq a where`、Declaration style対Expression style [p.152]〜[p.163]
• OCaml：`fun x -> fun y -> ...` による同形のλ記法、list.mlの`fold_left`・`fold_right` [p.171], [p.176], [p.177]
• 四言語のλ記法比較表 [p.182]

---

■ Part IV: Coqでの関数型プログラミング

• この部の核心:

証明支援系Coqにおける関数定義を通じて、型付きラムダ計算が「計算」と「論理」を統合する言語として機能することを具体的に示します。Coqでは`fun x => ...`がChurchのλx.に直接対応し、`Check`コマンドで型の整合性を確認しながらプログラムを構築します [p.181], [p.185], [p.186]。

• 論理展開:
• 型チェックと定義：`Check`・`Compute`・`Definition`コマンド、型エラーの例示 [p.185], [p.186], [p.187]
• 帰納的データ型：`Inductive bool/nat/list/natBinTree` によるデータ型定義 [p.190], [p.191]
• パターンマッチングと再帰：`match`による`negb`・`tail`・`andb`の定義 [p.192]〜[p.194]、`Fixpoint`による`plus`・`minus`・`mult` [p.195]〜[p.197]
• List操作の実装：`length`（fix使用）・`app`（++）・`map`・`naive_reverse` と動作確認 [p.200]〜[p.203]