講演資料


講義資料スライドの表紙

講義資料スライドの表紙です。スライド画像、または下の要約文中の青いページ番号リンクをクリックすると、別のタブで無駄なノイズのない、純粋なPDFビューア画面が起動し、指定されたページへ直接ジャンプして快適に閲覧できます。

全体概要

本セミナー「プログラムと論理」は、現代の形式的手法（Formal Methods）、とりわけDeep Specificationのような最先端の検証技術を深く理解するための「知的系譜」を丁寧に辿ることを中心的な目的としています [p.5]。

出発点に置かれる問いはシンプルかつ根源的です。「プログラムは正しいと、どうすれば言えるのか？」——この問いに対して、20世紀の知性たちは二つの異なる方向から答えを模索しました。一つは論理学・数学の側から、もう一つは計算機科学の側からです [p.5]。前者の代表はHowardやMartin-Löfであり、彼らは「型の理論」を構築し、プログラムの実行はある定理の証明に他ならないという認識に到達しました。後者の代表はHoareやDijkstraであり、代入文・if文・While文といった具体的なプログラム構成と論理との関係を研究しました [p.5]。

20世紀においては、これら二つのアプローチはそれぞれに限界を抱えていました。数学・論理学からのアプローチは現実のコンピュータ技術との接点が薄く、計算機科学からのアプローチは論理の多様な性質への理解と強力な「証明マシン」を欠いていました [p.6]。80年代に隆盛した形式的手法のムーブメントはやがて後退し、HoareやLamportさえもがその限界を公言する事態となります [p.141], [p.169]。

しかし物語はそこで終わりません。21世紀に入り、CoqをはじめとするDependent Typeに基礎付けられた証明支援システムの成熟が、二つの流れを統合する道を開きました [p.6], [p.7]。コンピュータが論理的・数学的推論を正確に実行できるという認識と、強力な証明マシンの存在こそが、20世紀の形式的手法と現代の形式的手法を分かつ最大の違いです [p.7]。ライプニッツが17世紀に夢見た「計算によって推論を正す」という構想は、計算機科学の世界でこそ現実となりつつあるのです [p.260]。

本セミナーは、この壮大な知的旅程を、Curry-Howard対応・Dependent Type・Hoare Logic・TLA・Coq・Deep Specificationという具体的な技術的トピックを通じて体系的に描き出します。

講義のロードマップ

■ Part 1: 計算と論理 ── 20世紀

  • この部の核心:

プログラムの「型」と数学の「命題」が実は同一の構造を持つという驚くべき対応関係（Curry-Howard対応）を軸に、型の理論がいかにして論理学と融合し、現代の証明支援システムCoqの理論的基盤を形成したかを解説します [p.15], [p.48]。「プログラムを書くことは定理を証明すること」という"Proof as Program"の洞察が、現代の形式的手法の中心概念であることを明らかにします [p.48]。

  • 論理展開:
  • Curry-Howard対応の発見: 1934年にCurryが、関数の型を表す矢印「→」と論理式の含意「→」のあいだに対応関係があることを発見。Howardはこれを深化させ「論理式は型付きラムダ計算の型と見なせる」と定式化しました [p.16], [p.26]。「p が命題Pの証明である（p : P）」と「p が型Pの要素である（p : P）」は双対的に解釈できます [p.27], [p.52]。
  • Dependent TypeとMartin-Löf: 1980年代にMartin-Löfが構築したDependent Type理論により、論理演算子（∧, ∨, →）もベクトルの次元のような値依存型も統一的に型として扱えるようになりました [p.30], [p.33]。全称記号はDependent Type `Π(x:A).B(x)` として自然に導入されます [p.33]。
  • Inductive TypeとCoqの実装: Coqでは自然数natが帰納的型として定義され、その定義から`nat_rect`という型が自動生成されます。これはまさに数学的帰納法に他なりません [p.35], [p.71]。"Propositions as Types / Proofs as Terms"（PAT）の立場がCoqの理論的根拠となっています [p.48]。

■ Part 2: プログラムと論理 ── 20世紀

  • この部の核心:

計算機科学の側から「プログラムと論理」を追求したHoare・Dijkstra・Lamportの三人の仕事を順に辿り、形式的手法の20世紀における到達点と限界、そして後退の経緯を客観的に描きます [p.74]。証明の性質をめぐる論争を経て、形式的手法がなぜ一度挫折したのかを、当事者たちの言葉で検証します [p.128], [p.141]。

  • 論理展開:
  • Hoare Logicの登場（1969年）: Hoareは公理的手法によりプログラムの性質を演繹的推論で導けると宣言し、事前条件・事後条件・プログラムの三つ組（Hoare triple）とWhile rule等の推論規則を定式化しました [p.76], [p.83]。ただし彼自身、30年後に「世界は我々が解決しようとした問題に深刻には苦しんでいなかった」と形式的手法の限界を公言します [p.141]。
  • Dijkstraのguarded commands（1975年）: Dijkstraは非決定性を導入したguarded commandsと、事後条件から事前条件を導くWeakest Precondition（wp）計算体系を構築しました [p.91], [p.96]。この枠組みの簡潔さと優雅さは、非決定性を受け入れることで初めて実現したと彼は述べています [p.98]。
  • LamportのTLA（1990年）: PnueliのTemporal Logicを発展させ、述語を「状態のペアに関するアサーション（Action）」に一般化することで、並行プログラムの仕様記述に十分な表現力を持つTemporal Logic of Actionsを提案しました [p.107], [p.121]。Safety PropertyとLiveness Propertyを統一的に扱えます [p.123]。
  • 証明の性質をめぐる論争（1979年）: De Milloらが「数学での定理への確信は社会的プロセスで決まる。それと同等のプロセスがないプログラム検証は必ず失敗する」と主張し、Lamportが直ちに反論しました [p.131], [p.136]。Dijkstraはこの立場を「全くの愚論」と評しています [p.133]。
  • Lamportの理論的総括（1997年）: 証明の長さは低レベル仕様の長さの二乗に比例するという「実証則」を示し、現実のシステムに形式的手法を適用することの本質的困難を指摘。「数学で推論する最良の方法は数学を使うことであり、擬似プログラム言語ではない」と結論付けました [p.173], [p.178]。

■ Part 3: 21世紀の形式的手法

  • この部の核心:

証明支援システムCoqを軸に、仕様・実装・証明が一体化したDeep Specificationというパラダイムを紹介します [p.190]。人間とコンピュータが協働して証明を構成し、その正しさをコンピュータがチェックするという新しい開発サイクルが、20世紀の形式的手法の限界をどのように乗り越えるかを具体的な実装例で示します [p.184], [p.217]。

  • 論理展開:
  • Deep Specificationの条件: 仕様はrich（詳細）・two-sided（実装とクライアント双方に接続）・formal（数学的表記）・live（コンピュータチェック可能な証明と結合）の四条件を満たすべきとされます [p.192]。仕様自身もプログラムとして動作し、そこからOCaml・C・Verilogコードが抽出される設計思想が核心です [p.215]。
  • Kamiプロジェクトの実例: CoqベースのDSLでハードウェアモジュールを記述し、`producerConsumerImpl [p.222], [p.232]。実装がトレースの意味で仕様を含意することをCoqの戦術スクリプトで機械的に確認できます [p.233]。
  • Software Foundationsの位置づけ: DeepSpec傘下のSoftware Foundations（Vol.1〜4）は、Coqを用いた形式的推論の実践的教材であり、現代のソフトウェア科学のLingua Francaとしてのコミュニティ形成を担います [p.234], [p.237]。

■ おわりに: ダイクストラの最後のメッセージ

  • この部の核心:

2001年の論文"Under the spell of Leibniz's Dream"でDijkstraが遺した思想的遺言を紹介します [p.241]。HoareやLamportが形式的手法の限界を認めた後も、彼は最後まで「信頼は証明の上にのみ基礎付けられる」という立場を貫きました [p.242], [p.243]。

  • 論理展開:
  • 四つの原則: ①テストが不可能な場合、信頼は証明のみに基づく。②信頼すべき理由が不明なプログラムは疑わしい価値しか持たない。③プログラムは正しさの議論が容易になるよう構造化すべき。④証明を先に与え、それに適合するプログラムを導く方が逆より遥かに容易である [p.243], [p.244]。
  • ライプニッツの夢の実現: 計算機科学こそが「記号が推論を導く」というライプニッツの夢を実現した場であり、それは数学科ではなく計算機科学科で起きたのは必然だったとDijkstraは述べています [p.260]。コンパイラや定理証明器は「未解釈の記号の操作」を日常的に行っており、コンピューティングの世界はまさにライプニッツの故郷となったのです [p.260]。