日々の流転

λ. 風邪を移されたらしい。喉が痛いし悪寒がする。しんど。

λ. Ruby/GTK vs GTK-2.0

一応、こんなバータリーなパッチを当てて「GTK_CONFIG="pkg-config gtk+-x11-2.0" ruby extconf.rb && make」でコンパイルは通っているのですが、シグナル関係がまずいらしくマトモに動作しなくなってます。

λ. 論文読み会

まあ大丈夫だろうと思って気軽に出かけてしまったが、やっぱまずかった。家に帰りつくときには既に意識朦朧。

論文は The Design and Implementation of Distributed Smalltalkだったのだけど、発表はイマイチだった。論文を読むことが目的であって、論文を翻訳するのが目的じゃないでしょうに。

とりあえず「報告書は水増しするためにある」と「発表者は、質問する隙を与えてはならない」だけは覚えておく。

λ. 四十九日の法会と納骨。

λ. まさきたんかわゆい。

λ. CHISE Symposium 2003 と RHG読書会にも興味はあったんですけどね。

λ. ORBit2-2.6.0

性懲りもなく挑戦してみる。Steven O'Brien 氏のORBit1用のパッチはenumのサイズが2バイトである事を想定しているのだけど、少なくとも現在のgcc-3.2は4バイトだったので、彼のパッチは使わなかった。で、結果、一応は動くのだけど、クライアント(例えばtest/echo-client)の終了時に「** ERROR **: file orbit-object.c: line 146 (do_unref): assertion failed: (robj->refs < ORBIT_REFCOUNT_MAX && robj->refs > 0)」と言われる(サーバ側は言われない)。

少し追いかけてみると、main()の最初の「CORBA_ORB orb = CORBA_ORB_init(&argc, argv, "orbit-local-orb", &ev);」でORBへの参照を得て、この時点でrefs=4。内訳は

1. このorb変数からの参照
2. _ORBit_orbからの参照
3. "RootPOA"との相互参照
4. "POACurrent"との相互参照

main()の最後の「CORBA_Object_release((CORBA_Object)orb, &ev);」で(1)が解放されrefs=3

main()からリターンすると、g_atexit()で登録された corba-orb.cのshutdown_orb()が呼ばれて、 そこからCORBA_ORB_destroy()が呼ばれる。

CORBA_ORB_destroy()の中程でorb->initial_refsの中身を開放するので、 (3)と(4)の参照が解放され、refsが3から1に減る。 (ただしサーバ側だとここで減るのは1だけ。 サーバ側ではきっと"RootPOA"か"POACurrent"のどっちかが まだどこからかまだ参照されていて、そのため参照が減らないのかも)

CORBA_ORB_destroy()の最後の方の ORBit_RootObject_release (orb); でrefsが1から0に減る(解放されているのは(2)?)。(A)

正しそうだ。 しかし、直後に 「At this stage there shouldbe 1 ref left in the system - on the ORB」 というコメントがあり、この時点でrefsは1でなくてはいけないようだ。おかしいぞ。

CORBA_ORB_destroy()からリターンした後、 shutdown_orbでこのORBをもう一回 ORBit_RootObject_release (orb); している(解放されているのは(2)?)。(B)

AかBのいずれかが間違い? あるいは……

λ. GConf-2.2.0

同じくSteven O'Brien氏のパッチを適当に編集してあてる。結果は、test/testpersistenceが「*** FAILED: float values nan and 8.3 are not equal (epsilon 13.4)」で通らない事以外は、一応動いているようだ。ただ、ロックファイルの扱いがなんだかおかしい気がする。

λ. Ruby/Gtk2備忘録

む。

λ. 花粉症?

このところ目が何か変な感じ。これって、ひょっとして、ひょっとすると、花粉症ってやつ?

λ. Parametricty and Mulry's Strong Dinaturality - A. Eppendahl

20061013#p03 を参照。

λ. Free Theorems in the Presence of seq - P. Johann and J. Voigtländer

スライド

The Impact of seq on Free Theorems-Based Program Transformations, Janis Voigtländer

seqが存在すると、関係を連続かつ正格なものに制限してもパラメトリシティは成り立たない。

foldr c n (build g) = g c n の反例

• g = seq, c = ⊥, n = 0
• g = λc n → seq n (c ⊥ ⊥), c = (:), n = ⊥

そこで、関係にさらに制約を加えることが考えられるが、 この論文では等式的な論理関係(equational logical relation)ではなく、不等号的な論理関係(inequational logical relation)にしている。 foldr/build に関する新しい定理は次にようになる。

• foldr c n (build g) ≧ g c n
• if c ⊥ ⊥ ≠ ⊥ and n ≠ ⊥, then: foldr c n (build g) = g c n

関係に対する幾つかの概念:

正格性(strictness)

(⊥,⊥)∈R

連続性(continuity)

∀i.(x_i,y_i)∈R ⇒ (∨x_i,∨y_i)∈R

全域性(totality)

∀(x,y)∈R. x≠⊥ ⇒ y≠⊥

left-closedness

≦;R = R

λ. (co)free でない代数的データ型

• 難しい点
  • word problem (語の問題)
  • (co)induction に証明が必要

λ. 蔵王で遭難の韓国人一行、捜索費用の支払い拒む

（・Д・）ポカーン・・・　　（⊇⊆）ゴシゴシ　　（・Д・）ポカーン・・・

「文化、国民性の違い」ってのはいいとしても、何でそこで「竹島」が出てくるんだか。

λ. 某カードの限度額引き下げ

某クレジットカードの限度額が無駄に大きかったので、デスクに電話して引き下げてもらった。引き上げの申請はWeb上で出来るのに、引き下げは電話する必要があるのがなんとも。

λ. TAPLの日本語訳出版します

すっかり書きそびれていたのですが、Benjamin C. Pierce の Types and Programming Languages (TAPL) の翻訳(共訳)をここしばらくしていたのですが、それがようやくこの3月に出版されることになりました。

• 型システム入門 プログラミング言語と型の理論 - オーム社開発部
• 型システム入門 プログラミング言語と型の理論｜Ohmsha

しかもトークイベントなるものがあるので、何を喋るのか謎だけれど(^^;、興味のある方がいましたら、是非ご参加ください。

• 『型システム入門 プログラミング言語と型の理論』ジュンク堂池袋店トークイベントのお知らせ - オーム社開発部

記憶が正しければ、原著について知ったのは、出版されたときに Benjamin C. Pierce のメールを向井先生に見せてもらって知ったのだったと思う。 当時はまさかそれを自分が翻訳することになるとは思っておらず、今更ながら驚いている*1。

ただ、当時はTAPLについて特に興味を持つこともなかったし、その後、型理論系の論文を読むようになった後も、何かの機会に買ってはみたものの、結局積読になってしまっていた。TAPLに書いてあるようなことはある程度は知っているつもりだったので、あまり読む必要性を感じていなかったというのもある。が、今回自分たちで翻訳してみて、これはすごく勿体ないことをしてたなぁ、と思った。 今となっては当然知っていることが多いのだけれど、知っていることについてもすごくしっかり書いてあるし、知らないこともそれなりにあった。 TAPL一冊読めば相当力が付くだろうし、TAPLを読まずにいたことで、昔の自分はずいぶん遠回りをしていたなぁと。