日々の流転

λ. 惰眠をたっぷり。

λ. www-amaya@w3.orgとwww-amaya-dev@w3.orgにsubscribe。

λ. 今日のパッチ

[ruby-ext:01988]

Init_gtk_window()がInit_gtk_font_selection()を呼んでて、この時点ではまだInit_gtk_notebook()が呼ばれていないので、初期化されていないgNotebookを参照することになってしまうので。

λ. 陰陽師

映画を見に行こうと思ったら、もう終わってた。トホホ。

λ. 借りた本

『富豪刑事』

筒井康隆[著]

『ブギーポップ・アンバランス　ホーリィ&ゴースト』

上遠野浩平[著] 緒方剛志[イラスト]

λ. デフレ対策は財政政策で行うべきなのか?

フィリップス曲線とオーカンの法則を使って、デフレからの脱出に必要な財政支出の量を推定している。なるほど、オーカンの法則が定量的な分析に使えるというのはこういう意味だったのか。

また、1930年代の大恐慌時のデフレからの脱出に寄与したのは、財政出動よりはむしろ金融緩和政策であった事が明らかになっているそうだ。1930年代の話は人によって言ってることが結構違うので、ちゃんとデータを示して主張しているのが素晴らしい。

λ. ブレスオブファイアⅤ ドラゴンクォーター

カプコンの人が雑誌に「ⅤはⅢのバージョンアップ、もしくは完成形」というような事を書いていた。僕の想像もあながち間違いではなかったのかも知れない。

λ. ポール・クルーグマンのインフレ・ターゲット論は間違っている

.

λ. Template metaprogramming for Haskell

2週間くらい前に印刷してたのを今頃になって読んだ。結構面白いし、かなり強力。

ところで、全然関係ないですけど、テンプレートいえば除数が2の巾乗かどうかで、コンパイル時にシフト演算と除算を使い分けるってのは楽しげですね。

λ. malloc(0)

Glibc vs uClibc Differencesには

4) malloc(0) in glibc returns a valid pointer to something(!?!?) while in uClibc calling malloc(0) returns a NULL. The behavior of malloc(0) is listed as implementation-defined by SuSv3, so both libraries are equally correct. This difference also applies to realloc(NULL, 0). I personally feel glibc's behavior is not particularly safe.

とあるが、何故glibcの振る舞いがsafeでないと感じるのか良く分からなかった。C++のnewは0バイトに対しても有効なポインタを返すことになっているので、mallocがそうであったとしても何の不都合も無いように思える。

λ. GNOME 2.0 プラットフォームへのポーティング

.

λ. チューリングの不動点演算子

Y' = (λx.λf.f(x x f)) (λx.λf.f(x x f))
   = λf.f((λx.λf.f(x x f)) (λx.λf.f(x x f)) f)
   = λf.f(Y' f)

この Y' をチューリングの不動点演算子というそうだ。

【2006-04-23】 ちなみに、Haskellではこれは以下のように定義することが出来る。 こうして表現するとカリーの不動点演算子(Y-Combinator)と比較し易いな。

newtype T a = PsiInv{ psi :: T a -> a }
 
fix :: (a -> a) -> a
fix = g (PsiInv g)
  where g :: T ((a->a)->a) -> (a->a) -> a
        g x f = f (psi x x f)

λ. 小人のパズル (関心空間)

百人の小人が怪獣に捕まってしまいました。 小人たちが怪獣に命乞いをしたところ、条件を出されました。

怪獣が小人たちを縦に一列に並べ、それぞれの小人の頭に 赤か黄色か青のうちのどれか一色の帽子を被せます。 小人たちは自分より前に並んでいる小人の帽子の色はすべてわかりますが、 自分を含め、後ろに並んでいる小人の帽子の色は全くわかりません。 （前から50番目に並んでいる小人は、49人分の帽子の色がすべてわかる）

小人たちはひとりずつ赤か青か黄色の色を一回だけ答えることができ、 それが自分の帽子の色と同じだった場合は命が助かるというものです。 答える順番はどの小人からでも構いません。

このような条件が与えられ、小人たちには作戦タイムが与えられました。 小人たちは少しでも数多く生き残れるような戦術をとるものとします。 たとえば、一番後ろの小人が目の前の小人の帽子の色を答え、 その小人は食べられてしまうとしても、次に後ろから二番目の小人が 今と同じ答えを言えば、その小人は助かります。 これを繰り返していけば、最低50人の小人は助かることとなります。

さて、小人たちは何人助かるでしょうか？ また、そのときの戦略は？

なお、被らされる帽子の順番に特徴的なもの （赤、青、黄色が順番にならんでいるとか） はないものとします。

大切なページ(2003-11-21)より。2,3分で解けた。人数の答えが書かれていなかったらもっと時間がかかったかも。\

λ. VD - Virtual Desktop for Win32

こないだ太田さんに紹介してもらった、Windows用の仮想画面ソフト。

λ. トランプの手品

同じく大切なページ(2003-11-21)より。小人のパズルよりもこっちの方が難しく感じた。いちおう自分なりの答えは考えたのだけど、いまいち自信がない。\

λ. ByteCodeRuby 0.2.0

だいありー(2003-11-19)より。ByteCodeRubyってだいぶ前に開発が止まってるのかと思ってましたが、0.2.0が出たんですね。試してみようと思ったら、ruth-0.10 が落とせないや。誰かこのファイル持ってませんかぁ〜?

λ. hyperset

以前にRubyで実装したコードを、最近Haskellで書き直すために見返していたのだけど、自分がとんでもなく愚かだったことに気付いてしまった。コンセプトを反映していない識別子名とかアルゴリズムの効率の悪さは置いておくとしても、bisimilarかどうかの判定を誤っているってのは致命的。こんなんで正しく判定できるわけないじゃん。しかも、それを一年近く気付いてなかったとは……俺のバカバカバカ。恥ずかしすぎる。ああ、多分今年一番の恥ずかしさじゃなかろうか。orz

λ. 「勝間和代の日本を変えよう」

読了。

λ. True Intensionality in Higher Order Logic

Logic and Engineering of Natural Language Semantics 6 (LENLS VI) での Reinhard Muskens 氏によるチュートリアル。 昨日の Haskell Night で紹介したMontagueのPTQのように自然言語の意味を形式的に考えることは形式的意味論と呼ばれて研究されていて、PTQはその最初期のものになる。 昨日PTQについて紹介して、今日このチュートリアルってのは偶然なのだけど、形式意味論の研究で僕がちゃんと知っているのはPTQくらいなので、最近はどんな感じなのかと思い、聞きに行ってきた。

タイトルの「Intensionality」というのは「内包」のことで、「内包」の取り扱いは形式的意味論を考える際のポイントの一つ。例えば、「明けの明星」と「宵の明星」はどちらも金星を指す、すなわち同じ外延を持つ言葉であるにも関わらず、「古代人は宵の明星を宵の明星だと信じていた」と「古代人は宵の明星を明けの明星と信じていた」は明らかに異なる意味を持っているので、「明けの明星」と「宵の明星」は異なる内包を持っていると言える。

チュートリアルのメモ

チュートリアルの最初の話は、PTQで〈s,t〉という型だった命題をprimitiveな型pとして扱う話。PTQだと「Mary believes that the cat is out if the dog is in.」と「Mary believes that the cat is in. 」から、「Mary believes that the dog is out.」を導出出来てしまうが、Maryは論理的に含意されることを全て推論可能とは限らない(imperfect reasoner)ので、これは一般には正しくない。そこで、命題の型としてpという型を導入して、必要に応じて〈s,t〉に変換する。それによって、前述のような誤った導出を出来なくする。

次の話はMoschovakisの「Fregeのsenseをalgorithms、Fregeのreferenceをvaluesと同一視する」というアイ ディアに基づいて、論理プログラムとして解釈する話。これまで、命題から可能世界の集合への関数を使って意味を形式化していたが、関数の代わりに、部分関数を表すニ項関係にする。 そして、意味公準(Meaning Postulates)を論理プログラム、命題をクエリーとして、Refutationをによって可能世界の集合を求める。自己言及的な命題ではRefutationが発散する。論理プログラムのRefutationの形で、実際の推論過程を取り込んでいるのが興味深い。

次は、命題をprimitiveとして扱うアプローチと似ているけど異なるアプローチの話。命題をprimitiveとして扱うのではなく、論理的に可能な世界を表す述語Ωを導入して、and/or/notなどの非論理定数はそれらの世界でのみ標準的な解釈をするようにする。

最後が、関係に基づいた高階の型理論の話。型として基本型とn≧0個のタプル型があって、関係に対してラムダ抽象とか適用とか出来て、解釈は内包と外延をうまく使い分けて定義されている。で、型〈〉で命題を、型〈〈〉〉で可能世界を扱ったりする。この論理は結構キモいけど面白かった。

α型の項の内包はD_αの要素とするのだけど、D_{〈α1, …, αn〉}の要素には外延というのがあって、これはD_α1×…×D_αnの部分集合になる。 命題の型〈〉の内包の領域はD_〈〉で、その外延の領域は一点集合のベキ集合になるので二点集合となり、これは{true, false}とみなせる。 可能世界の型〈〈〉〉の内包の領域はD_〈〈〉〉、外延の領域は命題の領域D_〈〉のベキ集合となる。

その他

@MoCo7さんに久しぶりにお会いし、また@kaleidotheaterさん、@zoeaiさん、@bon_jaさんといった方々に知りあうことが出来て良かった。 どうせなので、昨日の Haskell Night でのPTQの話についても紹介してみた。ただ、これは時間他の制約からかなりいい加減な紹介になっているので、専門の研究者に見られるのは恥ずかしいものがあるけど (^^;

それから、Combinatory Categorial Grammar (CCG) という範疇文法の一種を教えてもらった。