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

以前といっても購入したのは 2017 年であり、何で購入したのかは覚えてない。そのときは順序数(特に超限順序数)についてはなんら知識はなかったのにもかかわらず、最終章に順序数について記述のある本を手にとっていたものなのだから不思議な話である。

朝まで時間あるし以前購入した少し前から進めていた「集合論・入門 無限への誘い」(遊星社) をやろうと思う。この本、公理的集合論の成果に裏打ちされた素朴な集合論の入門本で面白い。特徴としては一般的な集合論の本とは異なり、背理法を用いる証明がなく全部直接証明するらしい。なんかコンピュータで証明するときって背理法は使いずらい印象(気のせいかも)があるので背理法を使わない証明に慣れると良さそうであり、定理証明に関心のある私に丁度相性が良さそうと思いこの本を選択した。

そして後から気づいたことに最終章に「順序数」の章がある。これは ACL2 を使うのに必要な概念で ACL2 の中でも特に理解が進んでない部分であり、正しく読破できた場合にこれが学べるのは大変有り難いことだ。また、集合論の入門の最後の章に設置されるような概念でありやっぱそんな簡単な概念じゃないんだなと納得もした(軽く概念を学んでフィーリングで使って順序数を使ってメジャー関数を定義してアッカーマン関数的なやつの停止性の証明をしてみたことはあるけどあんま釈然としてなかった)。

何となく helm から ido に移行しようと思ったけど無理だった。helm じゃないと生きていけない。

本当に、EXWM 作った人天才だと思う。これは中々思いつかないでしょ。おすすめの設定に ido を入れるのはやめて欲しかったけど（まあそのおかげ Emacs Lisp で既存関数の挙動を上書きする方法を学べたけどね)。

Window Manager 特有の設定を確認したり弄ったりしてスクショの取り方を確認したり、画面の回転をできるようにしたり、キーボードショートカットを追加する方法を模索するよりも、Window Manager を Emacs にしてしまって Emacs のコマンドで対応した方が話が早くて簡単でいい。

org-capture を頻繁に使うようにしてからは、EXWM を使うことによるデメリット(主にEmacs が何らかの理由で止まったりするとWMとして機能しなくなる件)よりも、org-capture がどこからでもできる利点が勝るようになったため、Xfce4 から EXWM に移行した。どこでも org-capture できるのは快適だし、Emacs なら気軽に画面を回転したりするコマンドとか、スクショするコマンドとかを簡単に追加できるのが嬉しい。

早期に起きてしまった。再度眠れる気配がないのが厳しい。

率直な感想としては、ハルヒっぽいとは思うけどそれが見たいわけではなかったという感じではやく新刊出して欲しい。

なんか、「これは涼宮ハルヒの憂鬱シリーズです！」とただ叫んでアピールしているような印象で、自己二番煎じをしているようにしか見えなかった。もしも、シリーズが完結した後に読んでいたなら面白く感じたと思う。分裂から驚愕までの部分が超面白かったこともあり割と期待外れだった(直観を読むために読んでた)。是非とも生きているうちに伏線を回収して無事に完結して欲しいと思う。

なんか技術的な革命を起こして群馬でもそんなに乾燥が苦でなくなるような感じにできないかな。

上京して驚いたのは冬がそんなに寒くないということだった。そのせいで最初の数年は割と冬でも薄着で過してしまい、周囲から変な目で見られてしまった。

普通、晴れていればあたたかいと思うのが一般的な認識だと思うんだけど群馬の冬にそんな常識は通用せず、そんなに気温が低くなくても圧倒的なからっ風によって体感温度は容赦なく下がる。気温などあてにならない。群馬の冬で外にでるなら完全装備が必須である。舐めてかかってはならない。

この前地元に帰省したとき、ソーラーパネルが大量に設置されててびっくりした。群馬の冬は晴れの日が多いんで太陽光発電には合理的なんだろうな。ただちょっと景観を損ねているような気もするので微妙な気持ちになった。

ほんとうに地震がくるたびに津波の心配がないか確認するのいやだ……。

私は乾燥に対して相当な耐性があることに上京してから気づいたんだよな。とはいえ、群馬に住んでたときはドライアイだったんだけど都心近辺に引っ越してからは完全に治ったので私も多少はダメージを受ける可能性はある。

山本一太知事の活動のせいでなんか最近地元に帰還したい気持ちが増している。ただなあ、自分は良いんだけどやっぱ乾燥に耐えられる人じゃないと住むにはちょっと厳しいところがあるのがなあ。

ああ、地震びっくりした。地震の恐怖が群馬に住んでいたときの数十倍くらいにはなっている。群馬に帰りたい……。

ブランド総合研究所による県別の「魅力度ランキング」に対しては「お葬式」が必要だ。お葬式というのは亡くなったという事実を遺族がありのままに受け止めるために必要とする儀式である。群馬県による徹底的な指摘によって「魅力度ランキング」は既に死んでいる。でも死んだという事実を知らないためにまだ生きているかのような誤解を産み苦しみ続けることになるのである。

「魅力度ランキング」に対しお葬式をして、7月の中旬に亡くなってしまったという事実をありのままに受け止めよう。お墓を作ってもいいかもしれない。

本当に群馬県が法的措置をとったら、もしかするとそれはお葬式として機能するかもしれない。他にもいろいろ手段は考えられるだろう。どんな手段であるかは重要ではない。何らかの方法で魅力度ランキングのお葬式ができればそれでいいのである。

ぐんまちゃん、頭いいな。https://youtu.be/aeGffUi0F7A

ぐんまちゃんもかぜをひいたことがあるんだな。https://www.youtube.com/watch?v=aeGffUi0F7A