講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編の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]。
■ Part 2: プログラムと論理 ── 20世紀
計算機科学の側から「プログラムと論理」を追求したHoare・Dijkstra・Lamportの三人の仕事を順に辿り、形式的手法の20世紀における到達点と限界、そして後退の経緯を客観的に描きます [p.74]。証明の性質をめぐる論争を経て、形式的手法がなぜ一度挫折したのかを、当事者たちの言葉で検証します [p.128, p.141]。
■ Part 3: 21世紀の形式的手法
証明支援システムCoqを軸に、仕様・実装・証明が一体化したDeep Specificationというパラダイムを紹介します [p.190]。人間とコンピュータが協働して証明を構成し、その正しさをコンピュータがチェックするという新しい開発サイクルが、20世紀の形式的手法の限界をどのように乗り越えるかを具体的な実装例で示します [p.184, p.217]。
ページのナビゲート