Coq

Coq'Art と格闘しているわけなんですが、

Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions
http://amzn.com/3642058809

まぁ、いろいろひどくって。まず、Scan な PDf で文字がかすれて g とか読めない。

どうも書いている人は、証明とか基本的なことを説明する気はまったくないらしく、カーリーハワード対応だの、β簡約だの、シーケント代数だの説明なしで出まくり。それは、まぁ、僕は我慢するんだが、肝心の Coq の説明も要領を得ず。

まぁ、そんなものでも問題をやってみれば少しはわかるんだけど、最初に出てくるのは型のチェックの例ばかり。いや、確かに重要なんだろうけど。第三章になってようやっと命題論理の証明が出てくる。そこでも、tactics とかは、いったいなんなのか、その実行はなんなのかとか全然説明がない。うーん。

なので、あまりにひどいので(まぁ、もう少し読む気ではあるんだが)、Twitter で聞いたら、

Certified Programming with Dependent Types
Adam Chlipala
http://adam.chlipala.net/cpdt/cpdt.pdf

というのがあるらしい。

こっちは、いきなり induction とか出てくるので、もっと、さっさと証明しよう的な感じ。こっちも証明論の基本的な説明はなしかぁ。まぁ、いいけどさ。

まぁ、どっちの本でも、大変だよな。プログラミングと証明は本質的には同じものだと思うけど、証明は難しい。だいたい4乗ぐらい難しい気がする。

この手の「プログラミング言語とは、全く別の証明系」ってのも、虚しい気もする。プログラミングのエラーって、だいたいスペルミスとか写し間違いとか、そんなものだよね。アルゴリズムが証明されても、それを C とかに写すのだと、そこでエラーが出てしまう。

Coq は、構文的には Haskell (のインデントがないもの) に近いので、どうせなら Haskell にしてくれと思うけど、なかなかね。

そもそも、証明って何とかいうところからやらないといけないので、述語論理とその証明の入門を Coq でやるような、そういうものが欲しいところだな。

シーケント代数とかは、図式的な証明でわかりやすので、そういうのと組み合わせると良い気がする。カーリハワード対応とかも、そこで説明するのに、そんなに枚数が必要なわけではないし。

これに比べると、モデル検証系の方が楽だよな〜 もっとも、証明系でも手で数十ページの証明を書いていた時期もあったので、それに比べれば、ましかな。

あと、Coq で、様相論理扱うにはどうするんだろう? まぁ、いろいろ方法はあるけど。