日々の流転

λ. 3時に寝て、6時に起床。

λ. CodeRed

ダイアルアップ接続でも時々来るみたい。

λ. 週刊エコノミー

東京三菱銀行頭取のインタビューが載ってた。読んで呆れた。要するに、ファイナンスのいろはも知らないような経営をこれまでしてたってわけだ。そりゃ、経営が傾くわけだよ。

貸し出し金利について、事務コストさえ取れればいいという考えではなく、その会社のリスクに応じた金利がとれない先は要管理債権と分類し直すなど資産査定の運用を厳格化しました。

λ. Ruby 標準でメモリーブロッククラス

是非欲しいですね。Ruby標準でメモリブロックを表すクラスがあれば、mmapとか、sysvipcのSharedMemoryクラスとかの切ない実装も、継承を使ってもっとシンプルに実装しなおせそうですし。

λ. 今年サンダルはくの初めてかも。夏だねー

λ. MIB2見てきた。

λ. 読書

ドラゴンヘッド (10)

望月 峯太郎 [著]

λ. Optimization Module

This optimization module aims to provide functionality to optimize methods and blocks by reconstructing NODE tree in the distant future.

おもしれー。こんな事まで拡張ライブラリから出来てしまうのかー

λ. Gtk::Plug/Gtk::SocketとDRb

Gtk::Plug/Gtk::SocketとDRbを組み合わせてみるのはどうか? Bonoboの代替にはならないだろうけど、ひょっとしたら割と遊べるんじゃないだろうか。

λ. "Dynamic Linking in Haskell", Hampus Ram

を読んだ。自分にとって興味のある話ではなかった。

λ. モデル検査入門, 高橋孝一

メモ。シンポジウム「システム検証の科学技術」 より。

λ. 人狼審問 : (723)小麦畑の村

また負けたー(T_T)　それにしても色々な意味でアリエナイ村だった。

農夫 グレン

>ユージーン
この人狼審問に、ありえない展開などあんまり無い！
(5ボス戦スタート)

個人的反省点

囁き洩れを素直に囁き洩れと思えずに占ってしまった点

占い師の真偽が人狼に判明して早期に襲撃されるリスクを軽視していた。 囁き洩れと信じきれなくても思い切って吊るべきだった。

委任トラップの過信

4日目の開票結果で白確定への票が残り狼側と同じ数だけあり、投票ミスをしたと名乗り出る村人もいなかったので、それが狼側の票だと思い込んでしまった。そして、委任トラップ先の人への疑いを解いてしまった。(>>4:109 の「おお、委任先はセシリアさんでしたか。実は僕はセシリアさんを疑っていたのですが……考え直すのです……」)
実際には自分の投票ミスに気づいていなかった村人がいて、委任トラップ先の人が人狼だった。

関連リンク

• B1/723村 - 人狼ファンWiki

λ. MAD PEOPLE β01: EPISODE 1007 「憤激の乙女達 〜顔をとりもどせ〜」

数日前から参加していたのが、さきほど決着がつき、現在エピローグ中。 市民の勝利だけど、私個人としては負けた気分。 反省点は色々あるので後で書く。

• <URL:http://straws.sakura.ne.jp/madb01/index.cgi?bid=1007>
• <URL:http://madpeople.gamedb.info/wiki/?EPISODE%201007>

λ. H↔Provable([H]) な H の真偽

不動点定理によって、任意の一変数論理式P(X)に対して、ある論理式Qが存在して ⊢ Q↔P([Q]) が成り立つ。ゲーデル文Gはそうして作った ⊢ G↔¬Provable([G]) を満たす論理式だった。ゲーデル文は直観的には「この文は証明できない」と解釈でき、この意味から(標準モデルで)真であることがわかる。

では、同様に不動点定理を使って作った ⊢ H↔Provable([H]) を満たす論理式 H の真偽はどうなっているだろうか?　直観的には「この文は証明出来る」という解釈できるのだが、別にそこから真偽が決まるわけでもなく……

最近知って、ちょっと面白かった話(答えは知ってます→20070916#p01)。

λ. length (filter p xs) ≦ length xs の証明

syd_sydさんの「Coqでクイックソート (未完)」を見て、length (filter p xs) ≦ length xs をAgdaで証明してみた(Filter.agda)。 ここから以下の2つを示すことが出来、クイックソートでの再帰呼び出しで引数が小さくなっていることを示すことが出来る。

• length (filter (\y -> y < x) xs) ≦ length xs < length (x:xs)
• length (filter (\y -> x <= y) xs) ≦ length xs < length (x:xs)

λ. 首の痛み

湿布をはって一晩寝たら、首の痛みはだいぶ良くなって、普通の寝違えくらいになった。ので、とりあえず病院へは行かないことに。良かった、良かった。でも、色々疲れていたのか、目が覚めたのはもうお昼ごろだった。午後は圏論勉強会へ。

λ. 第四十三回圏論勉強会

今日は圏論勉強会。 板書の写真

Abramskyの"Temperley-Lieb algebra: From knot theory to logic and computation via quantum mechanics"の3回目で、今回は 4 Factorization and Idempotents と、5 Categorical Quantum Mechanics の 5.1 Outline of the approach まで。

私は遅れていったので、4 Factorization and Idempotents のところは聞き逃してしまった。(後で書く)

5 Categorical Quantum Mechanics は記法が紛らわくて、少し混乱してしまった。▽がstateでbra、△がcostateでket。 特に混乱させられたのが「we also need to consider diamonds which arise by post-composing a state with a matching costate」という部分で、postが意味的な「後」なのか π∘ψ と書いた時の構文的な「後」なのかと、どっちにどっちをくっつけるのかが……(涙

今回の個人的な収穫は、Bob Coecke の Introducing categories to the practicing physicist (c.f. ヒビルテ(2007-05-15))への理解を深められたこと。

• 一つ目は、ベル状態 1 ↦ |0〉 ⊗ |0〉 + |1〉 ⊗ |1〉 のような書き方の意味が分かり、その性質もちょっと分かったこと。といっても、こないだ20080630#p01で読んだQMLの話で、有限次元のヒルベルト空間についてちょっとだけ理解出来ていたのを、再確認したという感じだけど。
• 二つ目は、最後の量子テレポーテーションの図が物理的にどんな現象を表しているのかを知ることが出来たこと。
  

それと、Christopher Isham という人がコンパクト閉圏のような圏ではなくトポスを使おうとしているという話を教えてもらった。

二次会はお好み焼き。

λ. 数学基礎論サマースクール 2009 一日目

「夏は夏らしく夏じみたことを」ということで、数学基礎論サマースクール2009に参加。

masahiro_sakaiによる数学基礎論サマースクール実況まとめ - yoriyukiの日記

後で書く。

λ. ICFPC2010のゲートの関数を他のソルバで求める

今年の The ICFP Programming Contest 2010 に参加したとき には、ゲートの関数を求めるのに Alloy Analyzer を使った。 Alloy を使った本質的な理由はあまりなくて、たまたま使い慣れていていたことで、解を列挙する機能があったことが大きい。 なので、正直どのソルバーを使っても似たようなものだろうと思っていた。

そこで、どうせなので他のソルバーでも試してみることに。 まず、SMTソルバーのYices(1.0.28)とCVC3(2010-07-11)に以下をそれぞれ食わせてみたところ……結果はいずれもunknownだった。 関係・関数も量化も有限領域上に対してしか使っていないので、最悪でも全部を基礎化(grounding)して、bit blasting すれば解けるはずなのに……これはかなりガッカリ。

• solve-op.ys
• solve-op2.ys
• solve-op.cvc
• solve-op2.cvc

(追加するかも)