日々の流転

λ. だるい。

λ. 数学と論理

去年やらなかった話としては、M.V.Glivenkoの定理の話があった。これは古典論理の定理に二重否定(¬¬)を付けてやると直観主義論理の定理になるという話。つまりは、古典論理を直観主義論理に「埋め込む」事が出来る。

λ. ストック経済論

株価のファンダメンタルズ理論の基礎。まあ常識でしょ。

λ. アルゴリズム論

教職を首になる三つのアルゴリズム

1. 入試情報を洩らす
2. セクハラ
3. 論文の剽窃

メフィストフェレスの円舞曲おもろい。

BNFは数学的な意味でのNormal Formでないらしい。ところで、Chomsky標準形やGreibach標準形はNormal Formなのかな?

λ. SWI-PrologとXPCEで遊ぼう!

Webアーカイブ上のもの

λ. バグが僕らを待っている おう!

……

λ. 某所のたこ焼きパーティに期待してたのだけど台風で中止らしい。

λ. 『これから論文を書く若者のために』 酒井聡樹

を借りた。

λ. トゥルークライム

.

λ. tDiary 1.5.7

毎日のようにpstoreのデータファイルが壊れるのにうんざりしたので、tDiaryのバージョンを1.5.7に上げてtDiary2形式にした。データはpstoreのままでRubyを1.8に上げるという手もあったけど、ITCに1.8を入れるようリクエストするのが面倒だったし、1.8.1は[yarv-devel:139]で懲りているので今回は見送り。

λ. デスノート

新登場の死神シドウたん、かわいいよ。

λ. アニメ版「夢使い」

アニメ版の「夢使い」をちょっと見た。これはこれで面白いとは思うが、結構複雑な気分。原作は、倒錯的で妖しい雰囲気とか、オカルティックなところとか、あるいは異様なまでの描き込みによって表現された「異界の歪んだ空気」みたいなものとか、そういった雰囲気が大好きだったのだが、アニメ版はそういう雰囲気は無くて、なんというか無難で健康的な雰囲気になってしまっている。そして、毒が抜けた分元気がないというか……。原作を再現する必要はない*1し、あれをアニメでやるのは不可能だとは思うが、やはり残念。ただ、キャラクターの絵と声は良かったと思う。

• 夢使い★公式サイト

λ. 今日のITシステム

• 「これをやって修論になるのかな」「なるんじゃない、するんだ」
• 絶賛迷走中
• 技術を出発点にすると論文書きにくい。「何が不便か」を出発点にすると比較的書きやすい。
• 組み合わせられるテクノロジーは何か?
• 「これを解決しました」というのが言えるとよい。

λ. Air-Edgeの料金プランを変更

Air-Edgeの料金プランを「つなぎ放題」から「パケコミネット」へと変更申し込み。翌々日から適用されるので6/1から変更するには今日申し込む必要があったのだった。

λ. Lockdown in sector 4

Gmail のメールをバックアップしようと、Thunderbirdを使ってIMAPで「すべてのメール」フォルダをローカルにコピーしようとしたら、途中で「Lockdown in sector 4 (Failure)」といわれてIMAPでのログインが失敗するようになってしまった。 ぐぐってみると、24時間のアカウントロックってやつか。たかだか7万通、400MBたらずのメールで……。しょぼーん。

λ. LL Future チケット購入

帰りに Lightweight Language Future のチケットを購入。 Tシャツの有無は悩んだけど、とりあえずTシャツ付のチケットにしてみた。 以前だったら確実にTシャツ無しのを選んだと思うけど、中途半端にお金があるせいで財布の紐が緩んでしまった……。酔狂だよなぁ……。

λ. 形式手法2.0＆証明付きDSL by tmiyaさん

社内イベント用のLT資料 - Formal Methods Forum | Google グループ より。

形式手法2.0＆証明付きDSL (PDF)