日々の流転

λ. 今日も、PM 4時頃まで寝てた。

λ. 内親王誕生

いやー。めでたいねー。

λ. 256円です!(PGの異質な感覚と生態) (from 今日のなんでやねん)

256がキリが良いとは思わないけど、自然数を0から数えるのは結構自然だと思う。ペアノ算術では1からになってたと思うけど、0からにした方が何かとねぇ〜

λ. Varyヘッダ

Comments on AgentGripesというページを見てVaryヘッダについて知ったので、この日記でも試験的に「Vary: User-Agent」を出力するようにしてみる。

λ. 「なお、Amaya の日本語化は来年リリースに向けて頑張りたいね、ということだそうです。Input Method 回りがわからないから、その辺りについては慶應大学 SFC さんよろしくって言ってました。とりあえず期待 age (違)。」

Input Method 回り以外は彼らが何とかしてくれるって事かしら。ソースを読み進む程にやる気を無くしてる人間としては、これほど素晴らしい事は無いねぇ。(苦笑)

λ. コンパイラ構成論

レポート提出。ところで、ゲストに講演を頼むらしいけど一体誰だろう。まつもとさんという噂も……

λ. 企業会計論

が休講で萎え。レミリアさんをいじめて時間を潰す。

λ. ブラックホークダウン

テレビでやっていたので見た。悪くはないけど、少し物足りない。

λ. Firefox 1.5

を入れてみた。全体的に軽くなった印象。これはもう戻れないなぁ。僕が使っている主な拡張機能だと SessionSaver, GreaseMonkey, ScrapBook, XHTML Ruby Support が既に1.5対応済みで、Digger, bbs2chreader が未対応。……早く対応しないかなぁ。

人狼BBSの例のGreasemonkeyスクリプトも動かなくなっていたので修正した。

λ. 株の感想

ほんの小額だけど株を売買してみて思ったこと。

• 財務諸表やその他の情報から投資対象を探すのはむちゃくちゃ面白い。
• サンクコストを無視して合理的判断を下すのは思ったよりも難しい。俺って意志薄弱だなぁ。

λ. Remily the Strange by GenocideKitten

少し前に某画像掲示板で見かけて、衝動的に注文してしまった。 色々と素敵。

λ. 風邪

風邪引いた。 昨日は喉が痛かったのだが、今日それが直ったら、今度は鼻水が止まらん。

λ. 計画停電

今日(12/2)はSFCで計画停電があるため、この日記も止まる予定。それから、それにあわせてこのサーバーのリプレースも行うそうなので、環境が変わって動かなったりとかもあるかも。

• SFC 慶應義塾大学 湘南藤沢キャンパス - 【再掲】: SFC構内停電に関するお知らせ（注意）
• 2007-10-31 構内停電に伴うネットワークの停止について

【2007-12-08追記】 今回の移行で、Linux/x86からLinux/x86_64になったのだけど、GDBMのフォーマットはアーキテクチャ依存なのを忘れていて、w3mlとRuBBSが動かなくなっていた。 以前、WebサーバがSolaris/sparcからLinux/x86になったときにも嵌ったのに、同じ事で二度失敗するとは……

λ. シャガール展

生誕120年記念　色彩のファンタジー　シャガール展　−写真家イジスの撮ったシャガール− というのをやっていたので、見に行ってみた。 「受付にて『シャガール〜大柴！』とくっきりはっきりいった方は100円割り引きます」とのことなので、ちょっと恥ずかしかったけど言ってみた。もっともルー大柴という人のことは良く知らないのだけど。

λ. 石焼ホットックと黒蜜きな粉アイス

土古里(도고리)というところでお昼を食べて、デザートに「石焼ホットックと黒蜜きな粉アイス」というのを食べた。 「ホットック」って何かと思ったら、お米から作ったお菓子らしい。英語では「Korean Ricecake and Brown Sugar Soybean Flour Icecream in Hot Pebbles」という説明で、韓国語では「돌솥　호떡　콩가루　아이스크림」と説明されていた。韓国語でもアイスクリームは「アイスクリーム」なのね。

λ. “A simple propositional S5 tableau system” by Melvin Fitting

• <URL:http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/SimpleSfive.pdf>
• <URL:http://www.ingentaconnect.com/content/els/01680072/1999/00000096/00000001/art00034>

を読んだ。

S5のシーケント計算はcut-admissibleではない(cf. 様相論理のシーケント計算)から、タブローもややこしいのではないかと思い込んでいたが、想像していたよりもずっと簡単なんだな。しかも、TやS4の決定問題がPSPACEなのに対して、S5の決定問題は高々NP完全で済むそうだ。これは、TやS4では(様相を剥がす時の)ブランチの破壊的な変更の順序に意味があったが、S5ではどの順序で行っても結果が同じため。

それから、健全性を示すための議論で、全ての世界の間に到達可能性関係が成り立つような構造だけを考えているのが、ちょっと目から鱗だった。S5の通常の構造では到達可能性関係は任意の同値関係なのだけど、ここでの扱いはこの通常の構造における同値類を取り出してきて一つの構造として扱っていると考えられる。妥当性を考える場合には、任意の構造を考えるので、こうしても実は結果は同じ。

ちなみに、何故これを読んだかというと、例によって知識論理を使って論理パズルを解くため。 先日のSPASSで知識の論理を使って論理パズルを解く?では定理証明機SPASSを使ってみたが、S5は決定可能なはずなのに、正しくない結論を与えたときに止まらなくなってしまうようで、どうもよろしくない。 それならば、S5の決定手続きを調べてみよう、という事で読んだのだった。 実際に論理パズルを解くために使うのはまた今度挑戦してみる予定。

【2007-12-04追記】 あれれ!?　この場合のタブローってシーケント計算とほぼ同じで、しかもカットに対応するようなものは入っていないように見えるんだよな。シーケント計算がcut-admissibleでないのに対して、これが完全なのは、一体何が原因?

【2007-12-06追記】 Deep Inference and the Calculus of Structures - Modal Logic 見つけた A Deep Inference System for the Modal Logic S5 という論文には以下のように書いてあったのだが、具体的に何が問題なのか良くわからない……

The failure of the sequent calculus to accommodate cut-admissible systems for the important modal logic S5 (e.g. in Ohnishi and Matsumoto [21]) has led to the development of a variety of new systems and calculi. A partial solution to this problem has been presented in Shvarts [25] and Fitting [5], where theorems of S5 are embedded into theorems of cut-free systems for K45. These systems provide proof search procedures for S5, they are, however, systems of a weaker logic.

λ. PLDIr #4

PLDIの論文を読む PLDIr の第四回に参加。 今回はPLDI2000の論文が対象で、私は以下の2本の論文を紹介した。

• Symbolic bounds analysis of pointers, array indices, and accessed memory regions (著者版)
• Translation validation for an optimizing compiler (著者版)

前者の論文は手続きがアクセスするポインタ・配列の範囲を解析するアルゴリズムの話で、競合の検出、自動並列化、範囲外アクセスの検出、範囲チェックの省略とかに使える。特徴は不動点計算を使わずに線形計画問題に還元して解くこと。

後者の論文はコンパイラの最適化の前後で意味が変わらないことを検証する話。等価性の定義として simulation relation というのを使っている。最適化器がevidenceとして simulation relation を出力すれば意味が変わらないことは容易に確認できるけど、最適化器が simulation relation を出力してくれなくても、多くの場合には simulation relation を推論できるとか。

発表資料 (PDF):

関連リンク

• [compeg:00109] PLDI report
• PLDIr #04 に参加した - まめめも(2009-12-05)

λ. 単純オートマトンの型について (HIMA' の補足)

先日のHIMA'で、

data Auto i o = A{ unA :: i → (o, Auto i o) }

という型*1が何故オートマトンの型なのかという話が少しあったので、簡単に補足しておく。 まず、入出力を扱う基本的なオートマトンとして、ミーリ・マシン（Mealy Machine）とムーア・マシン（Moore Machine）というものがある。

ミーリ・マシンは以下の組で定義される。

• 入力アルファベット集合 I
• 出力アルファベット集合 O
• 状態空間 S
• 初期状態 s0
• 遷移関数 δ: S×I→S×O

同様にムーア・マシンは以下の組で定義される。

• 入力アルファベット集合 I
• 出力アルファベット集合 O
• 状態空間 S
• 初期状態 s0
• 遷移関数 δ: S×I→S
• 出力関数 v: S→O

普通は入出力のアルファベットは固定したうえで、様々なオートマトンを考えると思うので、ここでは入出力のアルファベットはi,oに固定されているとする。すると、これらのオートマトンの初期状態を除いた構造は、

type T1 i o s = i → (o, s)
type T2 i o s = (o, i → s)

という型を定義して、ミーリ・マシンでは型S と 関数 S → T1 i o S の組によって、ムーア・マシンでは型Sと関数 S → T2 i o S の組によって表現できる。

T1 i o と T2 i o はともに関手になっていて、このような関手Tが与えれたときに、集合Xと関数 X → T X の組はT余代数(T-coalgebra)とも呼ばれる。そして、オートマトンの状態というのはこういう構造(=演算)を持った集合Sの要素であると考えることができる。

ただ、個々のオートマトン毎に型Sは異なっているので、いろんなオートマトンをシミュレーションしようと思うと、Haskellの型システム的には面倒くさい。それに、あるオートマトン(S1,δ1)の状態s1∈S1と、(S2,δ2)の状態s2∈S2は振る舞いが全く同じでも、値としては違う値であるかもしれなくて、これもよろしくない場合がある。

そこでS1やS2に相当する状態をすべて含んだ上で、かつ同じ振る舞いをする状態は同じ値になるような、そういう特別なオートマトンを考える。ミーリ・マシンの場合には (Auto i o, unA) がそれである。そして、以下のような関数 unfold phi によって、任意の (s, phi :: s → T1 i o s) の状態から、対応する (Auto i o, unA) の状態へと変換することができる。

unfold :: (s → T1 i o s) → s → Auto i o
unfold phi s = Auto $ \i →
  case phi s i of
    (o, s) → (o, unfold phi s)

余代数の言葉でいえば (Auto i o, unA) は T1 i o の終余代数(final (T1 i o)-coalgebra) で、unfold phi は (s, phi :: s → T1 i o s) から (Auto i o, unA) への一意な準同型射である。

このように、(Auto i o, unA) はある意味であらゆるオートマトンを表現できるような特別なオートマトンなので、これをオートマトンの型として扱っていると。