Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 253

今日は以前に書いた AVL 木の実装を ACL2 に移植してみる。https://github.com/tojoqk/map-avl/blob/master/lib/tokyo/tojo/map/avl.ss

たまたま自分は Emacs ユーザーだったのですんなりと ACL2 の実行環境を受け入れているけど人によっては厳しいのでは……。Eclipse と Dracula の環境の出来栄え次第か……。

Dracula っていう DrRacket から ACL2 を動かせるやつがあった。これでもよさそう。http://dracula-lang.github.io/

Agda も Emacs から使うことが前提になってるっぽい。https://agda.readthedocs.io/en/latest/getting-started/installation.html#installation-from-hackage

ACL2 を動かす環境の選択肢が Emacs か Eclipse かの二択なのやばい気がする。こういうことが結構あるので、エディタの選択で迷っている人には Emacs をおすすめしたくなる。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____EMACS

用意された例題ではなくて、自分が適当に証明しようとしたものも証明できるのは結構嬉しいな。

初めて ACL2 のドキュメントをみたときには、ACL2 に証明させるための補題を与えるとか難しすぎて、たぶん自分でやった方が早いとか思ったんだけど、意外といけるんだよな……。

ACL2 は最初の学習コストはめちゃくちゃ高いと思うんだけど、それさえ乗り越えればうまく ACL2 に自動証明させられるようになるので生産性と信頼性のバランスがとても良いのではないかと期待している。

初歩的なチュートリアルはだいたい読み終わったので、そろそろ ACL2 を使って何かしてみたいけど特にやることがないので困ってる。

リストの最後の要素を取得する関数とリストを逆順に並びかえてから先頭を取り出すのが同じであることの証明をした。key checkpoint を見て、「これは解けないのでは…」とか思ってしまったけどしばらくしたら car-rev-cdr を定義すれば証明できることに気づいた。勉強と経験を重なれば一瞬で証明できるようになるんだろうか…。

https://gitlab.com/-/snippets/2066838

loop を使いたくないとかいってたけど、むしろ loop は使った方がいいと確信した。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____LOOP_42?path=3603/6919/365/255

Computer-Aided Reasoning: An Approach を買ってしまった……。

ACL2 を使っていれば再帰じゃなくて loop マクロで書けと言われることはもうないのだ。

ACL2 では末尾再帰ではない普通の再帰関数を書くことが正当化されるだけでも正直嬉しい。再帰で書いた方が証明しやすいので再帰をしようすることにははっきりとした正当性がある。

機械が良い感じに簡約したS式を生成して人に見せて、人がS式を読みとって機械にアドバイスをするという循環なんだけど、これはS式でないとかなり厳しいのではないかと思っている。

末尾再帰で書いた高速だけどなんかよく分からん関数と普通に再帰で書いた関数が等しいことを証明する手段を手にしたのは、長年の夢を叶えた感がある。

ACL2 は定理の証明を自動で探索してくれるんだけど、少し複雑なだけの定理でも普通に失敗する。そこで人間がその定理を ACL2 に解かせるのに必要な補題を考えたり、証明の方向性をミスっているときは ACL2 にヒントを与えてあげたりするのだ。

停止性の証明については定理証明手習いで学んだ。厳密には理解してないんだけど、再帰する度に引数がなんらかの尺度(順序数)で小さくなっていくやつは停止性を証明できるという認識でいる。https://www.lambdanote.com/products/littleprover-ebookonly

@tacumi LISP 最高ですね！

ACL2、AI と人間の対話という未来のプログラミング体験をしている気がする。