Cacher is the code snippet organizer for pro developers

== The Incredible Proof Machine ==

この投稿はlink:http://www.adventar.org/calendars/1785[今年読んだ一番好きな論文_アドベントカレンダー2016]の 1 日目の記事です。

昨晩、もう 12 月も始まるからと Adventar 漁って RSS 登録していたら、このカレンダーを見つけてしまった。せっかく素晴らしい企画なのに初日から無人なんてもったいない（そしてあわよくば賞品欲しい）、ということで駆け込み一番槍をいただいた。

=== とりあえずゲーム ===

なにはともあれ、まずはこのサイトを紹介したい。

http://incredible.pm

たくさん並んでいる箱の一つを適当にクリックすると、画面が切り替わる。なお、 Chrome 以外だと正常に動作しないかもしれないので注意。

image::https://gist.github.com/yamarten/a352c0ba3c0d52ba9f96e23fb8ec6f8b/raw/371b84c8e439506041bb4bf9c1a391e6863ea52b/syllogism.png[プレイ画面,,400]

これは簡単に言うと配線ゲームだ。画面上のブロックにはデータを出すもの・受け取るもの・変換するものの3つがある。これらをうまく配置・配線して、左端のブロックに書かれている通りのデータを渡し、緑色にすることができればクリアだ。とりあえず適当に弄ってみればルールはわかってくる。

image::https://gist.github.com/yamarten/a352c0ba3c0d52ba9f96e23fb8ec6f8b/raw/371b84c8e439506041bb4bf9c1a391e6863ea52b/modusponens.png[クリア,,400]

少々慣れが必要だが、個人的には割と楽しめた。わからなくなったらゴール側から伸ばしていくとわかりやすいと思う。

=== 本題 ===

というわけで紹介したい論文はこれだ。

link:http://pp.ipd.kit.edu/uploads/publikationen/breitner16incredible.pdf[Visual theorem proving with the Incredible Proof Machine]

と言っても、リンクを貼った時点で紹介はほぼ終わったようなものだ。実際、論文の半分ほどの内容が既に終わっている。というのも、論文の前半は基本的に先のゲームのルール説明になっているからだ。

この論文は簡単に言えば、数学の学習用ソフトを作りました、という内容。言うまでもなく、ブロックは仮定や結論、推論規則を表すもので、それらを操作することは紛れもない証明だ。あのゲームはグラフィカルに証明を行う、いわば証明版link:http://www.mext.go.jp/programin/[プログラミン]のようなものだと言える。利点をまとめると以下のような感じ。

* グラフィカルで直感的
** 使いながら一般的な記法を覚えることもできる
* インタラクティブ
** 自分が何をすべきか、どこで間違っているかわかりやすい
* 様々な論理体系が扱える
** ルールは yaml 形式で簡単に設定可能

=== 本システムの利点 ===

まだ日付変更まで少し時間があるので、もう少し細かい話をしようと思う。

==== 証明の表記法の比較 ====

一般的に、自然言語以外で証明を表す場合には証明図を用いる。上に仮定、下に結論を書く形式だ。

image::https://gist.github.com/yamarten/a352c0ba3c0d52ba9f96e23fb8ec6f8b/raw/0569a401595c658c3b6903020d3604545787f9ad/proof1.png[証明図,,150]


また、インタラクティブな証明が行えるツールとして、定理証明支援系と呼ばれるプログラムが存在する。代表的な例としてはINRIA（フランス国立情報学自動制御研究所）が開発したlink:http://coq.inria.fr[Coq]が挙げられる。これはプログラミングのように文字列で証明を与える。

image::https://gist.github.com/yamarten/a352c0ba3c0d52ba9f96e23fb8ec6f8b/raw/371b84c8e439506041bb4bf9c1a391e6863ea52b/proof2.png[Coq プログラム,,400]

そして、これらと（概ね）同様の証明をしているのが、先程もあげたこの図だ。

image::https://gist.github.com/yamarten/a352c0ba3c0d52ba9f96e23fb8ec6f8b/raw/371b84c8e439506041bb4bf9c1a391e6863ea52b/modusponens.png[,,400]

どれが見てわかりやすいかは人にもよるだろうが、どれが書きやすいかは明白だろう。実際著者は高校生に対して利用後アンケートをとり、好印象を得ている。

==== 検証 ====

もう一つ重要な点として、本システムは定理証明支援系 link:http://isabelle.in.tum.de[Isabelle] 上で形式化が行われていることが挙げられる。言い換えれば、本システムに出てくるブロックや配線は数学的な対象として記述されている。

さらに、本システムで作成した図と既存の証明がちゃんと対応する、つまり本システムがちゃんと証明していることが証明されている。少々ややこしい言い回しだが、要するに安心して利用できるというわけだ。

=== おわり ===

実際のところこれを見せても「へー、そんなのがあるんだ」で終わってしまいそうな話ではあるのだが、個人的には割とインパクトがあった。というのも、自分は（そして著者も）定理証明支援系の文脈にいるからだ。本システムは、普段テキストベースで証明をしている人に、「こういう方法もあるよ」という提言をする意味合いも強いように思う。実際発表スライドなどを見ているとそのあたりを強調しているように見える。

論文中のも書いてあるが、ここから他の形式（証明図など）に出力できれば、とかlink:http://link.springer.com/chapter/10.1007/978-3-319-08970-6_30[最近]link:http://www.proofpeer.net[流行りの]（？）コラボレート機能とかあったらもっと面白くなりそうだ。

というところでタイムアップの様子。お粗末さまでした。

**11/2 追記**

もし定理証明支援系に興味を持った方がいれば、ちょうどlink:http://qiita.com/advent-calendar/2016/theorem-prover[アドベントカレンダー]もやっているので是非……と言いたいところだが、明らかに入門者向きではない。おそらくここで何かを紹介するより、検索してもらった方が早いだろう。

と言いつつ少しだけ紹介すると、プログラミングにおける定理証明支援系の立ち位置はlink:http://blog-randmax.azurewebsites.net/archives/1691/[この記事]などを読んでもらえると大まかなイメージがつかめるのではないかと思う。数学側から見たわかりやすい説明はすぐに思い当たらないが、link:https://ja.wikipedia.org/wiki/四色定理[四色定理]の証明に使われたことで有名だ。

**11/20 追記**

割と読んでくれる方の中に定理証明支援系を知っている人もいるようなので、念のため補足。

定理証明支援系では基本的にプログラミング言語を備えており、その性質を証明できることが強みの一つだが、本システムはそこまで強力ではない。デモページの最下段にはチューリング完全な計算体系である（型付き）ラムダ計算を扱っている。しかし、ここでは「関数 f が型 T を持つこと」を証明しているだけで、関数を組み上げることはできない。組み上げられる体系を用意することもできなくはない気がするが、そのためには相当のお膳立てが必要だろう。

プログラミング関係を扱うとすれば、例えば「指定された API の組み合わせで望む型のデータが得られるか」などの問題になるか、頑張って新たな体系を作って「以下の実行例を満たす関数を作れ」とする（できるのか？）か、もしくは定理証明支援系（やそれに準ずるもの）と連携して一部の命題の証明だけこちらで扱えるように改造するか、といったところだろう。なんにせよ、本システムの本来の目的は論理の教育であって、定理証明支援系を置き換えるものではない。

link:http://www.adventar.org/calendars/1785[アドベントカレンダー]の方は終盤となり、次々に面白い論文紹介記事が投稿されている。どれも全くの門外漢なので詳しいことはさっぱりだが、それはそれで楽しめる。残り5日間にも期待したい。