IT技術とCoqの世界 -- 証明 = プログラム = 計算の意味を考える
セミナーの呼びかけ
プログラマーは考える。プログラミングは論理的である
Coqは、一般には「証明支援システム」と呼ばれています。多くのIT技術者にとって、Coqは、特殊な分野（数学の問題の証明等）での特殊なコンピュータの利用だという印象を与えるかもしれません。ただ、Coqにできることと、IT技術者が日常的に行っていることとの間には、実は、大きな共通点があります。
あらためて確認したいのは、IT技術者にとって一番身近な対象であるプログラムが、極めて「論理的」な性格を持つということです。プログラミングするときに、我々は営業トークやプレゼンをする時とは違った頭を使います。それは端的に言って、「論理的」に考えるということだと思います。プログラムの「意図」を、プログラマは論理的にコードとして実装します。
プログラマーは機械と対話する。人間の「意図」を伝えるために
そのことは、IT技術者にとって、プログラミングと並んで一番身近な活動である、テストやデバッグがどういう活動かを考えてみてもよくわかります。テストでは、簡単なデータを与えてプログラムが予想通り（それは、「意図」に対して論理的に正しく）動いているかをチェックします。デバッグは、予想とは異なる振る舞いをするプログラムを、「意図」に照らして論理的に見直すことに他なりません。
コンピュータの側からみると、コンピュータは、ハードのエラーがない限り、与えられたプログラムのコードを忠実に実行します。コンピュータにとって、そのプログラムが実現すべき「意図」というのは、コードそのものによって与えられます。それ以外の手段で、コンピュータに人間の意図を伝える方法はありません。
プログラムのバグやエラーというものに、コンピュータには責任はありません。基本的な問題は、人間が、その意図を実現するように、コンピュータにコードを与えたかという問題です。
プログラマーは悩む。「仕様」と「実装」の間で
プログラミングでの人間の「意図」は、コードでの「実装」とは区別して「仕様」と呼ばれています。プログラムの開発で、仕様と実装を一致させる必要があります。そのために有効ないろいろな方法が、経験に基づいて提案されています。「テスト・デバッグ・ソースリーディング」のサイクルの繰り返しは、そうした経験的なノウハウの典型的な例です。
Coqが注目されているのは、まさに、この仕様と実装の一致のチェックに、人間のプログラマでなくコンピュータを使おうというところにあります。
難しそうな数式を使った数学と、プログラマが無意識のうちにでも従うプログラムのロジックとは、違ったもののように思われるかもしれませんが、その「論理性」についていえば、両者は同じものです。
仕様が形式的に定義されていれば、あるコードがその仕様の忠実な実装であるかは、形式的に証明できるはずです。Coqは、そうした開発スタイルを可能にします。
2019/11/28 マルレク 「IT技術とCoqの世界」概要
筆者は、これからは、開発者にとってCoqを学ぶことが重要になるだろうと考えている。小論はその理由と背景を、まとめたものである。
冒頭の「なぜ、開発は人間によって担われているのか？」は、人間中心の複雑な構造を持つ開発の世界は、コンピュータの論理的推論能力の利用で、大きく変わるだろうという展望を述べている。
現在では、多くの人にとって、それは非現実的なビジョンだと思われるかもしれない。ただ、それは、バグのないセキュアなソフトを作るという社会的に重要な課題に対して、もっとも根本的な解答を与えるものである。同時に、それは、開発コストの大幅な削減という経済合理性を備えている。Coqは、そうした見通しを実現する上で欠かせないツールになろうとしている。
次章は、先に見た開発過程の刷新の鍵であるコンピュータの「論理的＝数学的推論能力」をテーマにしている。「機械が論理的に推論する」とか「機械が数学的証明を行う」という言葉が腑に落ちない人は多いと思う。
「計算」「証明」「プログラム」という三つの言葉は、もともと別の意味を持っている。それは今でも同じだ。この章は機械の能力を人間がどう認識してきたかを、この三つの概念の関係の認識の歴史をメイン・ストーリーにして述べたものである。
まず、「計算」と「証明」が、本質的には同じものであるという認識が生まれ、ついで、「プログラム」は「証明」とみなせるという認識が生まれる。理論的には、この二つの発見で、三項の関係は明確になった。「コンピュータは、プログラムの実行という形で、証明を計算する」のである。
さいわいなことに、現代人は、「プログラム」と「計算」の関係については、十分な直感を持っている。この直感に依拠すれば、「チャーチ=チューリングのテーゼ」や「カリー=ハワード対応」に遡及しなくても、三項の関係が示す、「機械が論理的・数学的推論能力を持つ」という直感が得られるのではというのが、僕が期待しているところである。
残念ながら、「プログラム」と「計算」の関係だけでは、「証明」へのリンクが欠けている。僕のもう一つの期待は、Coqでの証明構成の経験が、このリンクを作ってくれるだろうということである。
これまで見てきたような、人間には何ができ、機械には何ができるのかという問題は、人工知能論の大きなテーマである。ただ、今回は、こうした問題について触れることができなかった。いずれ、機会を改めて、筆者の考えを述べたいと思う。
第二部 「Coqの世界」は、二つの章からなる。
最初の「Coqとのはじめての対話」は、Coqに触れたことのない人に、擬似的にCoqの対話的証明構築環境を体験してもらうことを目的にしている。
ただ、望むらくは、疑似的にではなく実際にCoqに触れてみてほしいと思っている。丸山は、自習用の Coq チュートリアルを公開している。https://github.com/maruyama097/coq-tutorial
また、12月14日には、二度目のCoq ハンズオンを開催予定である。
ハンズオンの資料は、次のページにまとめてある。https://www.marulabo.net/video/coq/
次章の「Coqによる形式的仕様の記述例」は、実際に、Coqではどのように仕様を記述するのかの紹介である。Coqによる仕様の「形式的記述」に、今一つイメージが掴めない人もいると思う。「形式的」というが、実際にCoqプログラムとして、コンピュータ上で動く仕様である。
紹介するのは、ひとつは、簡単な電卓ライクなスタックマシンの仕様記述例である。もう一つは、Deep Specification の代表的な取り組みの一つである。ChlipalaのKamiプロジェクトからのサンプルである。
第一部 開発の世界を考える
なぜ、開発は人間によって担われているのか？
機械は論理的＝数学的推論能力を持つ
ここでは、機械が論理的＝数学的推論能力を持つという認識がどのように形成されてきたのかを、 歴史的・理論的に振り返りたいと思う。こうした振り返りは、なぜこうした認識が今日まで十分に確立されなかったのか、その理由も明らかにする。
「証明」＝「プログラム」＝「計算」
ここでは、機械の能力を人間がどう認識してきたかを、この三つの概念の関係の認識の歴史をメイン・ストーリーにして述べたものである。
概略を述べておこう。
まず、「計算」と「証明」が、本質的には同じものであるという認識が生まれる。1930年代のことだ。
それから40年ほど経って、「プログラム」は「証明」とみなせるという認識が生まれる。1970年代のことだ。
理論的には、この二つの発見で、三項の関係は明確になった。「コンピュータは、プログラムの実行という形で、証明を計算する」のである。
第二部 Coqの世界
Coqとのはじめての対話
「はじめてのCoq」の「Hello Coq!」のセクションを参照されたい。
Coqによる形式的仕様の記述例
単純なStack Machineの例
http://adam.chlipala.net/cpdt/
https://github.com/phlummox/cpdt/blob/master/src/StackMachine.v
Deep Specificationでの仕様定義
Kami : 仕様定義サンプル https://github.com/sifive/Kami/tutorial.v
