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

Common Lisp よりも Scheme の方が好きだったんだけど、ACL2 を使い始めてからどうでもよくなった。というか ACL2 では全ての関数が全域(guard で制約をかけることは可能で静的に検証もできるけど、論理的には全ての関数は全域)なので、Common Lisp の方が相性いい気がしてる。

ここ最近 ACL2 が楽しすぎて生活が…

#ACL2 で鳩の巣の原理の証明を試みたら自動証明がうまくいって、何もしなくても証明できてしまった。https://gitlab.com/tojoqk/practice-acl2/-/commit/c7177564cc7d6e83afcb04d88174a2a8af5747d8

今日は #ACL2 で基礎的な集合に関する関数の定義とか定理の証明をしてた。https://gitlab.com/tojoqk/practice-acl2/-/commit/ecd68c1d625a72cba2670bbe3d303e78d38d2e85

普通のフィボナッチ関数と末尾再帰バージョンのフィボナッチ関数が等しいことを #ACL2 で証明できた！

https://gitlab.com/tojoqk/sicp-acl2/-/commit/fe05bfd1fbea2a013948913f39e4746c6140beba

順序数、いまのところ「 X ＜＜＜＜越えられない壁＜＜＜＜ Y 」のような超えられない壁を含む順序を表現するのに使うやつという超雑な理解しかできていないので、本格的に必要になったら困る。

#ACL2 で SICP の問題解くのめちゃくちゃ楽しい。SICP が説明している関数の性質を ACL2 で証明できることがある。https://gitlab.com/tojoqk/sicp-acl2

アッカーマン関数の停止性の証明、順序数を使ったら良さげなところまでは分かったんだけど、そっからどうやって証明すればいいのかさっぱり分かってないのに指示したら #ACL2 がスパッと証明してくれたの、なんか禁断の領域に踏み込んだ気がする。

適当に順序数を使って measure を定義したら、アッカーマン関数の停止性の証明に成功してしまった。 #ACL2 すごい！https://gitlab.com/tojoqk/sicp-acl2/-/commit/97b078fedf4fb2f3934cf35cd68ca87fc66b8591

仕事始めないと…。最近は趣味が楽しすぎて仕事の苦痛度が上がってる。

lambda がでてくると結構辛くなるなぁ……。マクロ使って適当に書き直せばいいか……。

ACL2 で SICP を二章までやってみようかな。不動小数点使っちゃうやつは飛ばす方針で。

ACL2 のプロジェクトに CI の設定をしてみた。これで定理証明に成功しているかどうかを GitLab の画面から確認できる。https://gitlab.com/tojoqk/practice-acl2/-/jobs/1002292298

CI で ACL2 を走らせるか。そうすれば、証明がうまくいっているか確認できて良さそう。

二分木に要素を挿入した後にその要素を探すと必ず挿入された要素が見つかる定理を追加した。これは #ACL2 的にも自明だったらしく一瞬で証明できた。https://gitlab.com/tojoqk/practice-acl2/-/commit/722c82b0120964966e04927800c9e54f48954be5

ACL2 と「仲良く」なることが重要なわけか。

ACL2 を広めて世界を Lisp の国に…

定理証明手習いの J-Bob やこの前作った vikalpa (https://mastodon.tojo.tokyo/@tojoqk/105579715190206801) で同じことを証明にようとしたら膨大な時間がかかるはずなので、これでも ACL2 によって得られたものはめちゃくちゃ大きいと言っていいはず。経験を積めばもっと短い時間で証明できるような気もする。

絶対正しいだろうけど具体的にどうやって証明したらいいのか見当もつかない状態から、私と ACL2 で S 式によるコミニュケーションを行った結果、定理だと証明できた。これはもう人工知能との対話による定理証明であるといっていいはず。(実際には ACL2 はルールセットを使って証明を探索しているだけだけどね)

長い間取り組んでいた趣味の問題が解決したのでもう一日終わった感がある。