講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
本セミナー「ラムダ計算と関数型言語」は、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]。
■ Part II: 型付きラムダ計算
型のないラムダ計算に「型」を導入し、変数・抽象化・適用のそれぞれに型推論規則を与えます [p.76]。最大の意義は「適用は型によって制限される」という制約であり、これによりΩのような計算が排除され、全ての計算が必ず停止する（強正規化性）という重要な性質が保証されます [p.95, p.97]。
■ Part III: ラムダ計算とLISP・Haskell・OCaml
Churchのラムダ計算が実際の関数型言語にどのように実装されてきたかを、歴史的系譜と具体的なコードの両面から追跡します。LISPはS式というデータ構造を通じて型なしラムダ計算を忠実に実装した最初の言語であり [p.111]、HaskellとOCamlはMilnerの多相型理論（1978）を基盤に型付きラムダ計算を実用言語として結実させました [p.139]。
■ Part IV: Coqでの関数型プログラミング
証明支援系Coqにおける関数定義を通じて、型付きラムダ計算が「計算」と「論理」を統合する言語として機能することを具体的に示します。Coqでは`fun x => …`がChurchのλx.に直接対応し、`Check`コマンドで型の整合性を確認しながらプログラムを構築します [p.181, p.185, p.186]。
ページのナビゲート