Agda

Haskell で書いた証明支援系ですね。院生時代は HOL だった。去年は Coq を使ったんですが、

＊　Haskell やるなら、近い構文の方が良い

というので、Agda をやろうと。「どうせ、おんなじようなものだろ?」とも思ったので。

なんだけど、

cabal install agda

で簡単に install が終わる割には、起動方法がまったくわからない。全然わからない。コマンド名がない。なんなの? いや、Coq でも、Application の中にある裸の coqtop を使っていたりするので、かなり怪しいことしていたわけですが。

で、しばらくしてわかったのだけど、

＊　Emacs の中から使うしかない

らしい。なんだよそれ。いまさら Emacs か? Emacs から脚を洗って vim 使いになった僕に Emacs を、また使えと。

それで、やる気が一気にくじけて、しばらく放置して圏論やりまくっていたんですが、ソフトウェア工学の授業は証明やるつもりなので、やるしかない。

で、Emacs 上げるんだけど、全然動かない。agda-mode が見つからない。locate agda してみたら

＊　~/.cabal/bin/agda-mode

そこか! なんで、そういう隠すようなことするかなぁ。~/.cabal/config をいじると、もっと、まともな path に置いてくれるみたいです。そういうわけで、~/.zshenv の path に ~/.cabal/bin を追加。それで、動きました。

で、Tutorial を見ていくのだけど、

Dependently Typed Programming in Agda
http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

なんだけど、延々、構文の話ばかり。Agda って、どうやって使うの?

Interactive Theorem Proving for Agda Users
http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html

こっちの方の Section 2 の方に、使い方が書いてありました。Refine とか、で Emacs の中で .agda なファイルを直接書き換えていくという方式。

Coq の方は、変数を宣言して、証明すべき式を Theorem や Lemma で書いて、そこに intro とかで、Natural Deduction の推論を直接当てはめていく方式。こっちは、auto とかもあるし、証明支援系らしい。

Agda は、Emacs の中で、式を書いて、これから書くところを ? と書くと、そこに入れる式の型とかを支援してくれる方式のようです。なのだが、いかんせん Haskell なので、

＊　構文がくせありすぎ

もちろん、Indent が構文の一部なんだけど、

＊ : とか -> あるいは任意のUnicode な記号

とかを自由に使える。なので、: と -> には両側に空白を付ける必要がある。しかし、その二つは、最もよく使われる記号だ。あだだだだ。慣れるだろうとは思うけど、どうしても、そこで構文エラーを食らってしまう。実際、 Interactive Theorem Proving for Agda Users でも、スライドの多くを費やして、そこを指摘している。いや、その判断はどうだったのかなぁ。

S:p

と書けないってのは厳しいよ。そんなこんなで、Coq と Agda は全然違うってのがわかりました。

まぁ、もう少し agda 見てみるつもりなんですが、Coq の方が良いという結論になりつつあります。Natural Deduction から、直接、繋がっているのは良いね。