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

ACL2 さん、これを自動証明してくるのは楽でいいんだけど自動証明されるのでデモにならなくて困るな。(0 から n までの総和が n 番目の三角数であることを自動証明してくれた)

BS 契約している人あんまいない気がするけど、今日の午後10時から始まるコズミックフロントはおすすめ。宇宙に興味がなくてあんま知らない人向けの内容になってて最初に見るのに良い内容になってる。https://www.nhk.jp/p/cosmic/ts/WXVJVPGLNZ/

あと、ACL2 の勉強は Lisp モチベによって維持されているところがあり、他の定理証明支援系にはそれがないので最初の学習コストの山を乗り越えるのが難しい。

#ACL2 以外の他の定理証明支援系も使ってみたい気もするけどなんか直観主義論理だし型で命題を記述する感じなので少しハードルが高い。

たぶん、ACL2 は定理証明支援系の中ではかなりクセの強いものだと思うのでその強みと弱みをしっかりと理解して使っていきたい。

ACL2 を今後も使っていくことを考えるとちゃんと一階述語論理についても学んだ方がよいのだろうか。

ACL2 は一階述語論理を使ってるのでゲーテルの完全性定理により恒真の定理は証明できるはずなのだ……。(それ必要な公理が欠けてたらどうなるんみたいな感じで、なんでそんなことがいえるのかについてはなんも分かってない)

順列の数がリストの長さの階乗になることの証明は、途中で心が折れそうになっても正しければ証明はできるのだということを学ぶ良い機会になった。

再帰関数の引数で状態を扱う関数の性質を証明するのは簡単ではない。ただしプログラムが少し複雑になれば状態を扱わざるを得ないのでこういった壁は超えなければならない。

やはり私が実装した順列は複雑なのではないだろうか。順列の数に関する性質を証明するだけでも大変で、それ以外の性質もなんか証明してみようかなーとか思って始めてみたらまた沼にハマっている。いったん順列からは離れるか。

ACL2 でリストの全ての順列を求める関数を書いて、順列の数が元のリストの長さの階乗個になることを証明できた。これは想像以上に大変だった。順列の実装は20行未満なのに補助関数や補助定理で 300 行くらい書いている……。たぶん何か回り道をしている気がするので短縮は可能だと思う。

source: https://git.tojo.tokyo/acl2-theorems.git/tree/permutations.lisp?id=c7cb466e2caf7bc500f66472d8781a14037eec1eCI: https://ci.tojo.tokyo/jobs/acl2-verify/221

結局 org-mode でスライド作ってる。スライドを GUI で作るのは厳しいと分かった。

@manzyun なるほど。pandoc で変換して odt にするのは合理的ですね。なんかこれから TeX の環境をセッティングすると思うとだるいなと思ってやめようと思ったんですが、pandoc なら楽勝なのでやってみます。

Nextcloud にもう collabora 入れるか。

3年前の自分ならスライド作るなら org-mode でなんかするかTeX でなんかするかを検討していると思うんだけど、今の私は LibreOffice に手が伸びているのでだいぶ堕落した感がある。

趣味なのにやりたくもないことを考えるのはやめたほうがいいのかもしれない。(ACL2 の用途について Web 技術者にとって分かりやすい例が求められているが、自分自身にとってはどうでもいいので考えるのをやめたい)

と思って ACL2 の出力を眺めていたら無駄なヒントを出していたことに気づいて消した。ACL2 マスターまでの道は長い。https://git.tojo.tokyo/acl2-theorems.git/commit/?id=12132a24ad279fd3c1443cb79d52f897acaa49a7

ACL2 が証明に失敗したときに、適切なヒントを出せるようになってきたな。最初の頃と比較してヒントを考える時間が明らかに短くなっている。まあ、今やっているのが簡単な問題だからというだけかもしれんけど。code: https://git.tojo.tokyo/acl2-theorems.git/commit/?id=80ff85f0f558e31a5aff784b2d38547c870f9d95CI: https://ci.tojo.tokyo/jobs/acl2-verify/169

Push した瞬間にジョブが走り出すの最高。

やはり、CI 独り占めの体験はいいな。時代はセルフホストだ。