プログラムと論理

2019年10月9日 2023年3月15日 MaruyamaFujio

「はじめに」から

小論は、 Deep Specificationのような現代の「形式的手法」の理解を深めることを目的としている。

現代の「形式的手法」には、いずれも50年近く前の1970年代に遡る、二つの異なった「起源」がある。両者ともに「プログラムと論理」という問題意識は共通していたのだが、生まれた場所が異なっていた。一つは、論理学＝数学の領域で生まれ、もう一つは計算機科学の領域で生まれた。

前者の代表は、ハワードやマーチン・レフである。彼らは、「型の理論」を作り上げ、抽象的だが、プログラムの実行は、ある定理の証明に他ならないという認識にたどり着いた。

後者の代表は、ホーアやダイクストラである。彼らは、代入文やif文、シーケンシャルな実行や繰り返しのWhile文といった具体的なプログラムの構成と論理との関係を研究した。

ただ、 20世紀の段階では、「プログラムと論理」という問題を扱うには、論理学＝数学からのアプローチでは、現実のコンピュータ技術や具体的なプログラム言語との接点は明確ではなかった。計算機科学からのアプローチでは、論理の多様な性質への理解と、何よりも強力な「証明マシン」を欠いていた。

様々な紆余曲折を経て、両者の統一は、21世紀に持ち込まれることとなった。筆者は、こうした二つの流れが合流したところに、 Deep Specificationのような現代の「形式的手法」が生まれたと捉えている。

小論では、20世紀に計算機科学の中で追求された「形式的手法」とその「挫折」を、一つのトピックにしている。このテーマでは、歴史を振り返るのには意味があると考えている。なぜなら、現代の「形式的手法」は、かつて一度失敗したムーブメントの再復活という面を持つからである。

現代の形式的手法の紹介は、前回のマルレクに続くものだが、今回は、出来るだけ具体的な実例の紹介を心がけた。

コンピュータが論理的＝数学的推論能力を持つことの認識と強力な証明マシンの存在こそが、20世紀の形式的手法と現代の形式的手法を分かつ最大の違いだと筆者は考えている。

と言っても、講演とスライドだけでは、「コンピュータによる証明」「コンピュータによる証明のチェック」の強力さ（スピードと規模感）が伝わらないと感じている。その技術は、現代の我々の手の届くところにあるのだ。ただ、多くのIT技術者は、そのことに気づいていない。

改めて、現代の形式的手法の基礎であり、現代のソフトウェア科学の Lingua Franca であるCoqの利用者を増やすことの重要性を強く感じている。