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

スコールをくらってびしょびしょになった…

ACL2 でスクリプトを書いてみようと思う。引数に state を取れば副作用も扱えるっぽい。

Twitter の検索結果の表示数が制限されたのでサービスの障害時の状況把握に関するお役立ち度が下がった。

人の行動の説明から仮説構成概念をなくそう

報酬という表現を滅ぼしたい。強化や強化子のことを報酬と呼ぶの分かりやすさ以外には害しかない。

「報酬欲しさに」みたいな表現を「オペラント強化により」に置き換えたい気持ちでいっぱいになる。

素因数分解して結果が全部素数になることを示すか。

なんか定理を示したいが何も思いつかない。

夏休み最後になんか定理証明するか。

あー、夏休みが終わりそうで悲しい気持ちになっている。

定理証明手習いの ACL2 の紹介の部分を読んでいるんだけど、Emacs の話はないな……。DrRacket の Dracula と ACL2 Sedan の話しかない。Emacs は闇なんだろうか……。

ACL2 で n 個の要素からなるリストの長さが n より大きいときに必ず重複が存在することを鳩の巣の原理によって証明できた！

鳩の巣の原理自体は ACL が自動証明してくれたんだけど、それをリストの問題に適用するのが大変だった。

source: https://git.tojo.tokyo/acl2-theorems.git/tree/pigenhole.lisp?id=b420ce87ceae55123e1780a7eddec7eea5388ab7CI: https://ci.tojo.tokyo/jobs/acl2-verify/260

ACL2 のリストの順列の数が階乗になるやつの証明を超リファクタリングした。やはり全てが見えている状態でかくと違う。無駄な定理の証明を省いたことで 300 行あったのが 200 行くらいになったし、全体的に美しくなった。最高だ。

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

疲れたのでもう寝よう…

バウンスリストに入ったという理由で送れないメールなど対したメールではないだろう。あまり気にしないでいよう。

面倒くさいという理由でお名前.com からのドメインの引っ越しの対応はやってなかったんだけど、実害でたしやるべきか……。

お名前.com、重要ではない通知に【重要】って付けるの本当やめて……。

まあ、最初はドメイン乗っとられた説から入っていたので、復旧可能な問題でよかった……。

ドメインが消滅しているときに私へのメール送信に失敗して企業側の送信エラーリスト的なものに入ってしまった可能性があるのが一番つらい。その場合は、最悪私にメールが届かなくなってしまう。

8.8.8.8 みた感じ、まだたまに引けない場合があるな……。明日までには直るだろう。