きゅーけー @tojoqk@mastodon.tojo.tokyo

高校生向けなんだけど内容は自由と尊厳を超えてて、行動分析学がどういう心理学なのか分かりやすく説明されているのでおすすめ。

心なんてない？！行動分析学を始めよう_福田実奈_高校生のための心理学講座(日本心理学会)_4
https://youtu.be/ld8EGEBwiWE

やかん

ブラウザの実装についてはなんも知らないけどいま GNU IceCat を使っていること自体が、Firefox が自由ソフトウェアであるありがたみだったのだ。

TootCloudでワードクラウドを作成しました！ #TootCloud https://tootcloud.ml

開発者による支配から身を守るために自由ソフトウェアを使いましょう
https://www.tojo.tokyo/freedom-for-yourself.html

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 は自動証明なので後からコードだけ読んでもそれがどうしたって感じになるなー。

これを証明するのすごく大変だったんだけど後から見返すと全然大変じゃなさそうなの困る。

ACL2 で回文に関する定理を証明した。ACL2 で定理を書くのがうまくなってきている気がする。

https://git.tojo.tokyo/acl2-theorems.git/commit/palindrome-sandwich.lisp?id=658812d37e3be083623a63c9839ac056451df1cd

早起きしたけど仕事は9時からでいいかな