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

証明が終わってから、ACL2 に証明させるには必要のない補題を定義していたことに気づく。必要ないというかむしろ有害な補題だった。https://gitlab.com/tojoqk/practice-acl2/-/commit/c58f7ce61cdf2bbcc86dfd7eb14be7eb31802e6f

Subgoal のヒントが必須なの笑えるな…。ACL2 に華麗にヒントを与えられる必要がある。経験とかノウハウで解決できる問題なら蓄積して公開したい。

絶対正しいし必ず証明できると思ってから実際に証明できるまで3日くらいかかってる。

ついに二分木の探索と二分木を連想リストに変換してから assoc するのが等しいことを証明できたー！！嬉しすぎて泣きそう。ACL2 を使いこなせる気がしてきた。

https://gitlab.com/tojoqk/practice-acl2/-/blob/3ad5bef9259a2837e25b63dcf8be8d7bee535f1a/binary-tree.lisp#L211

#ACL2

出前でバーガーキング頼んだ

尊厳を超えてそう。『自由と尊厳を超えて』もおすすめ。

後からみると10分くらいで思い付きそうなことしかしていないのが悲しい…

ACL2 エキスパートになれば、補題とヒントをすぐに思い付けるようになるのだろうか…。もしも、訓練によって補題とヒントがすぐに思い付けるようになったらめっちゃ効率的に証明によってプログラムの信頼性を保証していけるわけなので頑張っていきたい。

二分木に要素を追加しても全てのノードのキーが、左の木の全てのノードのキーよりも大きく、右の木の全てのノードのキーよりも小さくなることを証明した。

補題を思い付くのが難しい。たぶん3時間くらいかかった。

https://gitlab.com/tojoqk/practice-acl2/-/blob/b9222e3aad3d4c8d9eb78a04f49621e56e13a718/binary-tree.lisp

#ACL2

電光掲示板の3を8に見間違えて、思っていたよりも5分電車が早く来てびっくりした。

生産性があがっても労働時間には影響を与えない

効率化しても今の社会システムのままだと無意味な仕事が増えて働くことになるので AI が今の仕事を奪ってもどうせ働くことになる。

無限ループに入ったのかと思って眺めてたら、12.32 秒かけて、838070 steps で証明された……

#ACL2

サラダ食べてたら、昨日考えてた問題の解き方思いついた。

すれ違っている状況を「アンジャッシュみたいな」っていうふうに言えて便利だったんだけど使いにくくなったな……。

職場でこの仕事ブルシットだなとか言えないのかなりストレス

ブルシットジョブ つらい

RuntimeMaxSec めっちゃ便利じゃん。これで一日一回 Mastodon の service の再起動がかるように設定した。

systemd のdaemon のサービスを定期的に再起動する unit ファイルの書き方-timerを省略する - それマグで！https://takuya-1st.hatenablog.jp/entry/2019/08/22/131146

ma かどうかをしらべる述語なのか、map という関数なのかが区別できないのはやばいのでは……。もしかしてだから Common Lisp は map じゃなくて mapcar にしているのかな。

map、p が付くと mapp になっちゃう激レアケースじゃん。