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

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

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

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

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

そんなに伸びてるわけではなくてもかなりまともになった。

ショートスリーパーかもしれない気がしてきた。早く寝ても睡眠時間はそんなに伸びない。

A ならば B が真の時に B ならば A と思っちゃう現象、刺激等価性の話と関係があるかもしれないんだよな。ヒトよりも他の哺乳類や鳥類の方が論理的に学習をしてると言えるのかもしれない。

まだ「不自由なソフトウェアをみんなでボイコットしよう！」ということができる段階になってない。本当の意味で自由ソフトウェアについて知ってる人があまりに少なすぎる。ITエンジニアとそうでない人の集団を比較してもほとんど差がないといって良いレベルで知られていない。

完全に自由ソフトウェアのみを使って生活することができない人でも、自由ソフトウェアを広める運動をする資格はあるということも訴えていきたい。自由ソフトウェアのみを使って生活できない現状に問題があるのであって、自由ソフトウェアを使って生活できない人が悪いということではない。

不自由なソフトウェアがユーザーを支配してる話の記事、日本語での情報が少なくて希少価値あるのでリファクタリングしたい。https://www.tojo.tokyo/freedom-for-yourself.html

git のログを参照することで記事の変更履歴を参照するのいいアイデアだと思ったんだけどなー。

org-mode から CommonMark に変わってファイル名が変わった影響で記事の変更履歴が git のログから確認できなくなってることに気づいた。こまったな。。。

環境が変わって朝早く起きて早めに出勤するようになったのでやっぱ、「意志の力」とか関係ないなーと思う。

外れ値になっちゃうと困るし、単一被験体法を流行らせていきたい。

似たような環境な晒されれば同じような行動をとるのはそりゃそうか。人が多様性を獲得したというよりかは環境が多様性を獲得したんかな。

世代で括られても困るというのはよく思う。集団に意識があるとでも思ってんのかって感じ。実際あるかもしれんけど。

ACL2 で定理を書くのは宣言的に証明探索器を書くようなものなのでただ定理を書けばいいわけではないというのは、とても大切。

15分くらい暇なんだけどそれくらいの時間だと ACL2 をやる気にならない。

プリパテ→privateなぜパにしてしまったのか

最近プリパテが忙しくなってマストドンの浮上率激減してたな。引越し関連の対応が落ち着いてきたのでこれからは余裕ができるはず。

、→。