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

ACL2 なら cons セルが一番大切ということについて誰も文句がいえない環境というのもよい。

ACL2 の勉強してなんかに役立ててみるというのが、自分の一番やりたいことに近い気がするのでそういう方向に趣味のリソースを倒すのがいいのかもしれない。

この前の会社の飲み会で自分がLispについて語っていたとき、何を話していた瞬間が一番楽しかったのかを思い返すと、cons セルについて熱く語っているときだったので自分は Lisp の中では cons が一番好きなんだと思う。もちろんコード自体が cons で表現されていることも込みで。

まあ、あと二週間くらいは私にとってめっちゃつらく忙しい時期なので、それが終わってから考えるか。

1ドル160円になってしまったので流石に国内VPSの方がいい気がするのだけど、次の大統領選でトランプになってアメリカが自国通貨安誘導するようになっなら、円高になるかもしれんので気軽に動けん。面倒だし。

日本の機関が YouTube にべったり依存しちゃうのどうにかならんのかな。

一回全部みたけど内容覚えてない

直近で予定はないけど、海外旅行をするとなったら外務省のゴルゴ13のやつの「短」の動画を全部みてからにする予定。
https://www.anzen.mofa.go.jp/anzen_info/golgo13xgaimusho.html

いや、ガードよりも矛盾した証明ができないことが重要か。矛盾した定理を導く公理や定理がないから大丈夫という話か。

定理証明手習いに間数が全域じゃない場合には矛盾を証明できるという話があったはず。

値がないとすると間数が全域じゃなくなって困る。間数が全部全域で必ず値がある前提で定理証明をしてるから。
ACL2 でもゼロ除算の結果は 0 だけど、ガードという機能でゼロ除算をしないことを証明できる形になってる。
https://www.cs.utexas.edu/~moore/acl2/v8-5/combined-manual/?topic=ACL2____UNARY-_F2

あの流れならもっとLispの話できたなというので少しの残念さがある。それでも、今回の飲み会は久しぶりに楽しかった。

神bot見つけた

帰りも電車混みすぎたな。東京人多すぎ。

酔っ払って失敗したなあ。せっかく数学科出身の人とお話する機会があったのにどういう研究してたのかなんも聞けなかった。定理証明支援系の話ばかりしてしまった。

渋谷駅、前来たときと構造が違う気がする。不思議のダンジョンじゃん。

ニコニコのクレカ流出疑惑、自分の仕事上の理由でそういった領域に触れたことがあり、おそらく流出してないだろうと思える。というかサーバーを通過しないようにする命令があったはずだし。

都市計画の過ちなのか、JRの過ちなのか。ともかく苦しい。

雨の中での満員電車、傘で服が濡れてつらい

久々の電車なのだけどこれは地獄だな。人が流れず滞留してる。