日々の流転

λ. お昼は家族でスカイラーク・グリル。僕は、「岩手鶏のスパイシー・グリル」と「シーフードドリア」を食べた。午後、ビデオで「マスク・オブ・ゾロ」を見た。

λ. 「オブジェクト指向スクリプト言語 Ruby への世代別ごみ集め実装手法の改良とその評価」と「Ruby の VM 化に向けて」を読んだ。後者を読むことで、「VMって結局バイトコードをソースと見ると、 たんなるインタープリタじゃん」という認識を改めた。

λ. RWiki

RWikiをインストールしてみました。動作したのを見た時はちょっと感動しちゃいました。(苦笑)

自動で過去のデータを自動的に保存してはくれないようなので、バックアップにはとりあえずpdumpfsを使う事にする。あと、他にも幾つか不安があるんだけど、どーしよっかなー

λ. 夜まで寝てた。何やっているのだろうね、俺は。

λ. SFCにおける日記間リンク

ふと、SFC Antenna に登録されている日記のURL間のリンク関係を抽出して、ラベル付き有向グラフとしてビジュアライズしてみた(SVG,DOT)。(手元のGraphvizに日本語パッチが当たっていないので、SVGだけでスマソ)

他の日記とのリンクを持たないノードは省略してしまったのだけど、このグラフはちょっと寂しいよなぁ。日記URLかどうかの判定が厳しすぎるのかも知れないけど、ひょっとするとSFC生には日記間でリンクを張り合うような習慣はあまりないのかも知れない。

λ. Ruby-GNOME2-0.1 is released!

まずは一区切りか。後半はあまりコードを書けず、既に「過去の人」状態の私ですが、それでも何か肩の荷が降りたような感じ。

λ. 中間管理職はヴェブレン財

9/24に買った『構造改革論の誤解』に以下のような事が書いてあって、目から鱗だった。そうか!、そうだったのか!!

日本では中間管理職は、意思疏通や意思決定の媒体という「職能」において必要とされているというよりも、仕事へのインセンティブを与えるみせびらかしの(conspicuous)効果をともなう「ヴェブレン財」として機能してきた。

λ. rand

1.7では Mersenne Twister を使うようになっているのか。

λ. ITTでの選択公理

なるほど。ITT₀では選択公理も証明できるのか。

参考

• Agda による選択公理の証明

λ. 理大祭

東京理科大の大学祭に行ってきた。たまたまるりという人のライヴを見たのだけど、なんかすごいキャラクターしてるなぁと思った。話しているときと唄っているときのこのギャップはなんなんだろう……

λ. 読書

『HELLSING 6』

平野 耕太 [著]

『ケロロ軍曹 7』

吉崎 観音 [著]

λ. cpoとか

らくがきえんじん(2004-11-13) でcpoの話を見かけて、cpoという単語は複数の意味で使われていて紛らわしかったのを思い出した。私の知ってるのだとこんな感じだったかな。

有向集合 (directed set)

≦を集合X上の擬順序(preorder)とする。部分集合S⊆Xは、任意の有限部分集合T⊆SがS内に上限を持つ(∨T ∈ S)とき有向集合。(空集合の上限が存在するのでSは空集合ではない)

dcpo (directed complete poset)

任意の有向な部分集合が上限を持つ半順序集合。この上限は ∨^↑ S 等と書かれる事もある。

cpo (complete poset), ipo (inductive partial order)

最小元⊥を持つdcpo。下のcpoと区別するためにipoと呼ばれることも。

cpo (complete poset), pointed cpo

最小元⊥を持ち、任意の無限上昇列(ω-chain)が上限を持つ半順序集合。ω-chainの上限は ∨_i=0^∞x_i 等と書かれる事もある。下の最小元⊥を持たないやつをcpoと呼ぶ場合にはこっちは pointed cpo と呼ぶ。

cpo (complete poset)

任意の無限上昇列(ω-chain)が上限を持つ半順序集合。最小元⊥は持たなくてもよい。

ω-algebraic dcpo

任意の有向な部分集合がω-chainを含んでいて、有向集合の上限とω-chainの上限が一致する algebraic dcpo。

λ. Molle (MOdal Logic Loony Evaluator)

最近様相論理の定理証明器を少し探していて見つけた、タブローによる証明器。 Javaで書かれていて簡単に試せる。 ただ、複数の様相を扱えず、またKでの証明しか扱えないっぽい。

スクリーンショット

□(A→B)→□A→□B を証明させた場合

□(A∨B)→□A∨□B を証明させた場合

□(A∨B)→□A∨□B の反例のクリプキ構造

λ. 慶應義塾大学SFC ORF2009【Gardens for Ingenuity -断面の触感-】

ORFに初めて参加し、今頃になってSFCって実は凄かったんだと感じる。以下、個人的に印象に残っている話をいくつかメモ。

個人的に面白かった展示のひとつが、「SF-KEY: 鍵盤楽器奏者のための譜めくり支援システム」で、演奏がどれだけ進んだかを自動認識して自動的に譜めくりしてくれるシステムを目指していた。現時点では自動認識の部分はできていて、画面上で楽譜の表示を切り替えることはできてるが、将来的には紙の楽譜をめくるようにしたいそうだ。

それから、ARのために目のまえに走っているクルマとデータを対応付けるために、どうするかという話なんかも面白かった。 ナンバープレートを画像認識して、そこから同定良いかと思ったのだけど、それは難しいらしく、代わりにテールライトの点灯タイミングを元に同定する方法を考えた、という話。

我らが萩野服部研の展示は、「どこでもIRプラグ」「S3」 「Acti-on」 「RIO」。

• 「どこでもIrプラグ」はSheevaPlugみたいなものをコンセントに指しておいくことで、赤外線リモコンで操作可能な家電を、外出先からWeb操作可能にするという話。デモとして、ORF会場から研究室の照明を操作するというデモをしていたが、元々研究室の照明は赤外線で操作なんて出来ないので電子工作を頑張っていて、むしろそっちの方が凄かったかも。
• S3 (Simple Sound Streamer) は、リスナーの選択した色をもとにメタデータのマッチングを行って、プレイリストをつくると言うもの。
• Acti-on は AR っぽい話だった。
• RIOについては何も言うまい(笑)。なんでも、今の萩野服部研には「お絵かき部」があるとか……

熊坂研のコミュニティ分析系の話で「声優偏愛マップ」「我輩は童貞である。まだやったことはない。」「リア充のリアリティ」とかあって、題材が狙いすぎな感じだけど、結構面白い結果が出ていて面白かった。

他にも、最適な量子通信路の決定の話とかみたいな話とか、触手がウネウネ動いてるやつとか、相変わらず随分色々やっているな、という感じ。

他にも面白い展示が沢山あった。