IT技術とCoqの世界 – 証明 = プログラム = 計算の意味を考える

2019/11/28 マルレク

概要:https://coq1.peatix.com/view
資料ダウンロード:http://bit.ly/2qE43tq

資料viewer

「はじめに」から

筆者は、これからは、開発者にとってCoqを学ぶことが重要になるだろうと考えている。小論はその理由と背景を、まとめたものである。

冒頭の「なぜ、開発は人間によって担われているのか?」は、人間中心の複雑な構造を持つ開発の世界は、コンピュータの論理的推論能力の利用で、大きく変わるだろうという展望を述べている。

現在では、多くの人にとって、それは非現実的なビジョンだと思われるかもしれない。ただ、それは、バグのないセキュアなソフトを作るという社会的に重要な課題に対して、もっとも根本的な解答を与えるものである。同時に、それは、開発コストの大幅な削減という経済合理性を備えている。Coqは、そうした見通しを実現する上で欠かせないツールになろうとしている。

次章は、先に見た開発過程の刷新の鍵であるコンピュータの「論理的=数学的推論能力」をテーマにしている。「機械が論理的に推論する」とか「機械が数学的証明を行う」という言葉が腑に落ちない人は多いと思う。

「計算」「証明」「プログラム」という三つの言葉は、もともと別の意味を持っている。それは今でも同じだ。この章は機械の能力を人間がどう認識してきたかを、この三つの概念の関係の認識の歴史をメイン・ストーリーにして述べたものである。

まず、「計算」と「証明」が、本質的には同じものであるという認識が生まれ、ついで、「プログラム」は「証明」とみなせるという認識が生まれる。理論的には、この二つの発見で、三項の関係は明確になった。「コンピュータは、プログラムの実行という形で、証明を計算する」のである。

さいわいなことに、現代人は、「プログラム」と「計算」の関係については、十分な直感を持っている。この直感に依拠すれば、「チャーチ=チューリングのテーゼ」や「カリー=ハワード対応」に遡及しなくても、三項の関係が示す、「機械が論理的・数学的推論能力を持つ」という直感が得られるのではというのが、僕が期待しているところである。

残念ながら、「プログラム」と「計算」の関係だけでは、「証明」へのリンクが欠けている。僕のもう一つの期待は、Coqでの証明構成の経験が、このリンクを作ってくれるだろうということである。

これまで見てきたような、人間には何ができ、機械には何ができるのかという問題は、人工知能論の大きなテーマである。ただ、今回は、こうした問題について触れることができなかった。いずれ、機会を改めて、筆者の考えを述べたいと思う。

第二部 「Coqの世界」は、二つの章からなる。

最初の「Coqとのはじめての対話」は、Coqに触れたことのない人に、擬似的にCoqの対話的証明構築環境を体験してもらうことを目的にしている。

ただ、望むらくは、疑似的にではなく実際にCoqに触れてみてほしいと思っている。丸山は、自習用の Coq チュートリアルを公開している。 https://github.com/maruyama097/coq-tutorial
また、12月14日には、二度目のCoq ハンズオンを開催予定である。

次章の「Coqによる形式的仕様の記述例」は、実際に、Coqではどのように仕様を記述するのかの紹介である。Coqによる仕様の「形式的記述」に、今一つイメージが掴めない人もいると思う。「形式的」というが、実際にCoqプログラムとして、コンピュータ上で動く仕様である。

紹介するのは、ひとつは、簡単な電卓ライクなスタックマシンの仕様記述例である。もう一つは、Deep Specification の代表的な取り組みの一つである。ChlipalaのKamiプロジェクトからのサンプルである。