Pinned post

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

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

Pinned post
Pinned post

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

Pinned post
Pinned post

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

L-99 (Ninety-Nine Lisp Problems) の P12 の RLE のデコードをする問題で、エンコードしたのをデコードしたときに元に戻るのを ACL2 で証明できた!
git.tojo.tokyo/acl2-theorems.g

あと、P11 の encode-modified とP13 の encode-direct が同じように振る舞うことも示せた。
git.tojo.tokyo/acl2-theorems.g

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

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

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

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

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

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

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

Show thread

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

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

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

Show thread

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

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

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

Show thread

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

Show thread

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

Show thread

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

Show older
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!