日曜日も一日 Coq で遊んでいた。Coq'Art の冒頭に、Coq を使えばソートプログラムの証明が出来ると書いてあって、それが知りたくて頑張って読んでいるがいつまでたっても具体的な方法が出てこなくてがっかりしている。これだけの本をさっと読むのは大変だし、もうちょっと簡単に書いてある文章は無いかな。
Coq で興味のある事は二つあって、一つは機械で証明出来る範囲を知りたいという事。もう一つは、依存型が本当に実用になるのかを知りたい。
私は昔から計算が苦手だったが証明も大の苦手だった。計算は電卓でも出来るが証明は出来ない。その事で、証明はどことなく文系の香りのする、言葉遊びのような胡散臭い物だと思っていた。だからある程度コンピュータでも証明という事が出来ると分かってとても嬉しい。
今の所の感想だと、Coq とその背後の理論はとてもすばらしいし、中学生くらいまでの証明なら全然余裕なんじゃないかと思う。惜しむべきはその取っ付きにくさだけど、なんとか改良して子供でも使えるようにして、義務教育で教えるべきだと思う。私が証明嫌いだった理由の一つに、教師が嫌いで教師の言う事を信じてなかったという事があるが、機械の言う事なら信じれたと思う。
もう一つ依存型について。これもまだちゃんと理解できてないが素晴らしいと言うしか無い。プログラミング言語始まって以来の大発明だと思う。でも依存型にしても、その応用のプログラムの証明にしても、イマイチこんなの役に立たないという意見も聞くので、もうちょっと勉強したら悪い所も見つかるのかもしれない。
依存型というのは引数に応じて別の型を返す仕組みで、Coq では forall x:A, B のように書く。もしも B の中に x が無ければそれは A->B と同じで、つまり依存型は普通の静的な関数型のスーパーセットになっている。たったそれだけの改良なのに、突然証明に使えたり、仕様記述に使えたりすし、もしかしてSmalltalk のような型に無節操な言語でも、型検査の恩恵を受けられるんじゃないかと思う。
プログラム言語の議論をしていると、よく実装と仕様の話題が出てくる。理想は実装の細々した事に惑わされず仕様が書けたらいいのになー。というのは良くある話のパターンで、色んな人が色んなやり方を考えていると思うけど、少なくとも依存型を使うと、実装と仕様の区切りは明快で、もうこれ以上議論の余地が無いほど正しい！という気になる。
こういうのを勉強してラッキーだなと思うのは、例えば Coq'Art の出版は 2004 年なので、もしも私が出版される前に死んでいたら、この知識に近づく方法は全くなかっただろう事だ。そして中学生の時のまま証明が嫌いで、プログラムの仕様記述なんて不可能！と思って一生を終えたに違いない。生きてて良かった！あとはどうやったらこの素晴らしい理論をもっと実用に生かす事が出来るのだろうか。
