ゴルフ

最近ちょぼちょぼまた再開してる。いまいち手応えがないが粛々とやっていこう。

平和にくらしております

毎日フラッシュバックスペル使ってる感じ。平和。

なんか家帰ったら妻がいるというだけですげーいい感じなのが不思議。私ってこんな普通な感覚持ってる人だったっけ？

退職

本日、長年つとめてきた独身貴族を退職し、人生の墓場へ異動になりました。
今後は第二の手札たるグレイブヤードを最大限に活かして生きていこうと思います。

二重Quine みたいなの作ってみた

@eval_of c *x="main=putStr%c*x=%c%c%s%c%c;main(){printf(x,34,92,34,x,92,34,34);}%c";main(){ printf(x,34,92,34,x,92,34,34);}

— 岡本暁広〄へんくまモン (@henkma) 2013, 6月 14

@eval_of hs main=putStr"*x=\"main=putStr%c*x=%c%c%s%c%c;main(){printf(x,34,92,34,x,92,34,34);}%c\";main(){printf(x,34,92,34,x,92,34,34);}"

— 岡本暁広〄へんくまモン (@henkma) 2013, 6月 14

二重Quine みたいなの作ってみた eval_of へのコマンド含めて140字にするのけっこうめんどかった。

さとのやとかソ連とか

さとのや行ってソ連やって情熱ホルモン行った週末だった。
ビールいっぱい飲んだ。

ソ連。なかなか楽しかった。部室暑い。

イカ演算子（>=>）の圏論的な意味について聞かれたんだけどわからなかった。だれか詳しい人教えて。

5/25～5/26

KMCの新歓コンパに行ったり別邸の棚卸したりした。

ボードゲーム数えあげたら 189個（しかもリストに入れそこなっているやつがでてきたりしたのでもうちょっとある）もあった。
拡張とかを別々に数えたら200個いきそうだった。

背理法がどうのこうのについて

背理法、P を前提にして矛盾を導いて ¬P を言うっていう理解が多すぎると思うんだけど、
こんなもんまで問題にするのはそれこそ問題であって、これは否定の導入だとか含意の導入だとか言えばいい。ここらへんまで認めないのは直観主義よりもさらにアレなのでアレである。
よくある√2が無理数であることの証明なんて、少なくとも高校での無理数の定義（有理数でないこと）から考えればこちらの場合に属するので背理法でもなんでもない。

¬P を前提にして矛盾を導いて P を言うっていうんであればそこは何か問題の本質に踏み込んでいるので意味がある。これは背理法だ。二重否定除去と言ってもいい。

そこらへん区別してないもんが多すぎる気がする。