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

そろそろ行動分析学者の人はなんか活動した方がいいんじゃないだろうか。さすがにこのまま続くともうだめだと思う。

この記事、行動分析学よりの提言してた。https://news.yahoo.co.jp/byline/haradatakayuki/20210105-00216054

引っ越しして部屋が分かれたことで休日には仕事のことを忘れられるようになってきている。だいぶよくなった。

L-99 (Ninety-Nine Lisp Problems) の P12 の RLE のデコードをする問題で、エンコードしたのをデコードしたときに元に戻るのを ACL2 で証明できた!https://git.tojo.tokyo/acl2-theorems.git/tree/L-99.lisp?id=af0b9d96812a399bd7e3d20a1157b361ec227ae4#n341

あと、P11 の encode-modified とP13 の encode-direct が同じように振る舞うことも示せた。https://git.tojo.tokyo/acl2-theorems.git/tree/L-99.lisp?id=af0b9d96812a399bd7e3d20a1157b361ec227ae4#n399

普段は末尾再帰の関数が好まれがちだけど、関数の性質を証明するには遅くて愚直な再帰関数の方が圧倒的に優れている。

状態を回すタイプの再帰関数に関する証明、ACL2 を使ってるとなんか証明に辿り着けるんだけどどうなってんのかあんまりわかってない。

定理証明、末尾再帰の状態をひきずるタイプの関数がでてくると難しくなってくる。

ACL2 で関数の性質を証明しながら L-99 の問題を解くの楽しい。

ACL2 の defun-sk について勉強して存在する系の証明できるようになろう

ACL2 でリストモナドがモナド則を満たすことを証明した。https://git.tojo.tokyo/acl2-theorems.git/commit/?id=086cbd344e702fecf6de144c2313e824a4aa075a

ACL2 で証明をすると最終的に答えに行きつくまでの道筋を失なってしまうので、マインドマップに試行したことをメモしながら証明しようと思う。

undefined じゃなくてもっと激しく爆散して欲しい

JavaScript、なんか都合の悪いことが起きるとすぐに undefined っていうのやめて欲しい。

最近、なんかよく分からん仕事をやる人になってて厳しいな。SREとはって感じになってる。なぜ私は JavaScript を書いているの？

300 円寄付してくれっていう圧がすごい。あとでするか…。

Wikipedia から唐突に「あなたは特別な存在です」とかいうメールが来てなにかの勧誘かと思った(再寄付のお願いメールだった)。

生活環境の変化によって、スマホで ACL2 ができることがもとめられるようになった

大変だったアピールするためには解説記事書くしかないな

はあ、仕事するか。。。

やっぱ、ACL2 は自動証明なので後からコードだけ読んでもそれがどうしたって感じになるなー。