自分らしくないものができあがると楽しい

またもや昼ごろ起床. 昨日 H 研究室に呼ばれた時に,失踪した某人についての話がでていた.係についてはよく知らないが,研究室からいなくなったことについて,自分に落ち度があるのかないのかよくわからない状態で色々いうのもどうかと思って,特に擁護も…

地味に LaTeX 歴が5年目に入った

昼ごろ起床.そのあとなんだかんだで夜まで家にいた. んで,深夜に H 研究室に呼び出されたので行ってみる.なんか半年ぶりぐらいに M 君を見た気がするが多分気のせい. よくわからないが,S 研究室の N 君が LaTeX で一悶着あったらしい.一瞬で解決した…

センター国語の誤答選択肢みたいな会話の応答をどうするか問題

昨日,くだんの実験の件で大騒ぎしたあと寝落ちして,昼ごろ起床.結局一人で大騒ぎしただけじゃないかという気がして,少し嫌になってくる.昨日のブログの PV 数がやたら多くて, Hatena のアクセス解析によれば,全記事の中で最も読まれていることになっ…

研究室には来た方がいい,マジで

昼ごろ起床し,Amazon でポチっておいた本などをヤマトの営業所まで出向いて受け取ってから出勤. んで,夜に,明らかに不安なツイートが飛び込んでくる.友情パワーで次々人が集まっているのは結構なこと,だがしかし,これは絶対何も考えてないやつだと私…

大物を倒す

あんまり寝てない.寝てないせいで勢いで制御の教科書を買ってしまうなど.普段はプログラミング言語の研究ごっこをしているが,一方で機械学習とか制御とかも,やりたいことの親戚分野として気になってはいるのだ. んで,証明としては大物を倒した.やはり…

Beamerで狙い撃ちで矢印を出す

起床時間とかよく覚えてない.Beamerで,こういうスライドを作った. このスライドみたいに,Beamerスライドの任意の位置から任意の位置へ矢印を出せると便利である.WYSIWYG系のプレゼンテーション作成ツールに慣れていると「そんなの簡単じゃん」と思うだ…

インフルエンザ

朝寝て,昼ごろ起床. インフルエンザの第一報.一緒に雪見に行ったりカラオケ行ったり唐揚げを揚げたりした人なので,これは俺も来るな…. www.meiji.co.jp によれば,インフルエンザウイルスの潜伏期間は1日〜2日だそう.ということは,今日の夜から遅くと…

唐揚げ

昼ごろ起床.証明の続きをちょろっと書く.シフト系の補題を全部倒せて Happy. そのあと某所にて唐揚げを揚げる.H 研の U 君とか,Y 研の @ 君,M 君,F さんなどが来る.今回は漬ける時間を短めにして若干薄味にしてみたら美味い. んで,毎年企画側だっ…

センター現代文を解いてみた

昼ごろ起床.前日朝 4 時ごろまで歌ってて,そのあと勢いでデスボイスの練習とかしてたので仕方ない気もする.なんか惜しいのは出るようになったっぽい.が,最大の問題はレパートリーにデスボイス出すような曲がないこと.意味ないじゃん. んで,この日は…

カラオケで証明

7時起床.外を見たら雪がすごいことに. 雪のなか歩いて100万分の2のために病院まで行く.雪の中歩くのは慣れてるし楽しい.んで,もう今日で通院終わって良いとのこと.9月の真ん中に病院に運ばれたので,4ヶ月間通院していたことになる.奇病とお別れする…

良い趣味・微妙な趣味

また朝は6時ごろ起床.地味に研究を進める.若干気まぐれで Notation を追加した.実はもう Notation の整理については,めんど臭いものも多くてあんまり乗り気じゃないのだが,まあそれはあったほうが便利かもな,と思うもののうち,簡単だなと思うものは対…

大学生の服装

2日に1回の更新が続いている.いかん.できるだけ毎日続けたい. やはり6時ごろ起床.朝からちょっとした会議.というとあくせく働いているように見えるが,まあ時間帯以外はのんびりとしたものなのでよろしい. 最近はよく食堂でご飯を食べている.んで,食…

さらに Coq

朝6時ごろ起床. 朝は線形代数のお話を聞く.絶賛 Coq に没頭中なので,かなり細かいところばかりに目がいってしまいよろしくない.が,まあ 1 年生相手だったらちょっとうるさいぐらい論理の訓練をしてもらった方が良いだろうということで許してほしい. ん…

Bool型を使った古典命題論理の埋め込み?

昼ごろ起床.昼夜逆転を半回転させるのに成功した. んで,本題.Coq というか Gallina の if-then-else を使った証明が扱いにくくて悩ましいが,if の後の bool 値は,中身の構造に立ち入らなくても, true だった場合と false だった場合に場合分けしてし…

証明が証明を呼ぶ

なんだかんだで昼前に起床. 証明が証明を呼び,がっはっは,という感じに.非形式的な証明ってどれだけ行間があるのか痛感させられる.しかもちょこちょこ行間として難問が現れる.Coq 力が足りないだけなのか数学力が足りないのかはたまたその両方か,よく…

昼夜逆転を巻き戻すために

とりあえず証明の目処がたったので[要出典],昼夜逆転を巻き戻すためにあとはほぼ一日寝ていた. 途中,うどんを食べるために, N さんと 5km ぐらい散歩したりした.適当に色々話しつつ散歩するの楽しいので,春先に散歩部でもやりませんか.んまあ普段は歩…

二日連続ボヤ騒ぎ(比喩ね

日付変わってしばらくは証明をして,日が昇る前にはコインランドリーで洗濯.そのあと病院で「100万人に2人」を見てもらう. 「100万人に2人」については,皮膚がすっかり閉じて「もう大丈夫ですね」ということだそうだ.だが,ステロイドの分量を減らしてい…

オーダー表記

日付がわかってからまだ寝てない.今から寝る.多分今日中に起きないので寝る前に日記を書いてしまう. 日付が変わるまでは論文書きと,追加のデモ実装.以外に捗る. んで,午後は某所にて某発表を聞いた.んで,その発表の本質とはあまり関係ないが,そこ…

わりかしおもしろい定理をみつける

Twitter でだべっていたら(論文書け),わりかし面白い定理を見つける. 人が,「全員が同じ帽子の色ということはない」という条件のもとで,赤・白の帽子をかぶって一列に並ぶ.このとき,各人は,自分より前の人の帽子の色は見えるが,自分の防止の色はみ…

走り初め

今年も徒歩で色々と旅行をするため,体力をつけておかなければならない.ということで走り初め. スーパームーンらしいので月が出ているうちに走り始める.最近スーパームーン多い気がするが多分気のせい. やはり iPhone での撮影にも限界があって,やっぱ…

2018年の抱負など

みなさま,あけましておめでとうございます.今年は穏やかに新しい年を迎えられました.きっと良い年になることでしょう. 昨年度はどうもすみませんでした.本年もご迷惑をおかけすると思いますが,どうか勘弁してください.そしてその都度,忌憚のない率直…

初日の出とモナド

初日の出を拝むために,Kさんの車で阿蘇山につれていってもらう.ここを 03:00 ごろ出発して,5:30 ごろつく.まだまだ暗い. 寒すぎるので一旦車に戻り,N さんと「モナドは単なる自己函手の圏におけるモノイド対象だよ。何か問題でも?」という話をした.…

2017年を振り返る:11月12月編

いよいよラスト,11月・12月分を振り返ります. 12/26:1月・2月編 12/27:3月・4月編 12/28:5月・6月編 12/29:7月・8月編 12/30:9月・10月編 12/31:11月・12月編 2017年11月 月初めは諸々面倒臭い書類の処理に追われる.また某お勉強会の資料作りに追わ…

手巻き寿司

7時就寝,14時ごろ起床? 大晦日なので手巻き寿司を食べる.手巻き寿司とかやったの本当に十年ぶりくらいなんじゃないかという気がする.周囲に反対されながらも「半分は俺が出すから」とゴネて中とろを買ったのだが,これが功を奏してうまかった.けんども…

パネポン > 論文

論文書かなきゃいけないのにパネポンやってしまった.んでそのあと寝て,夕方起床.がっはっは.アブストの修正は投げる. それにしてもパネポン,無限に続けられるな.あんな危険なゲームはないな.連鎖組めなくてもそこそこ面白いからだろうな.一方のぷよ…

2017年を振り返る:9月10月編

さて,はやくしないと年が明けてしまうんので,引き続きどんどん2017 年を振り返ってみよう.この勢いで, 9 月・10 月分. 12/26:1月・2月編 12/27:3月・4月編 12/28:5月・6月編 12/29:7月・8月編 12/30:9月・10月編 12/31:11月・12月編 2017年9月 な…

論文 > スペワ

朝寝て夕方起きる.んで,そのあと論文をひたすらかく.まずはアブスト.どうでもいいけど,「アブスト」と聞くと,中学生の頃,アウストラロピテクスの図に似ていたので「アウスト」と呼ばれていた知り合いを思い出す.なんて名前かは忘れた. んで,スペワ…

2017年を振り返る:7月8月編

さて,はやくしないと年が明けてしまうんので,どんどん2017 年を振り返ってみよう.論文書かなきゃいけないんだけど.今日 (といってもだいぶ投稿は遅刻してるけど) は 7 月・8 月分. 12/26:1月・2月編 12/27:3月・4月編 12/28:5月・6月編 12/29:7月・…

2017年を振り返る:5月6月編

昨日に続き,2017 年を振り返ってみよう.今日は 5 月・6 月分. 12/26:1月・2月編 12/27:3月・4月編 12/28:5月・6月編 12/29:7月・8月編 12/30:9月・10月編 12/31:11月・12月編 ここから 8 月頃までは Twitter による記録がほとんどないので,かなり…

歌い納め

7:00就寝,16:00頃起床.んで,家で若干ダラダラした後研究室に行くと,おそらく年内最後であろうカラオケに誘われるので喜んで行く.カラオケは論文書きながら歌うのにちょうどいいから.んまあ,年末料金高いけんども…. んで,K 君が unravel を数キー上…