日々の流転

λ. WString

WStringを複数のlocaleを扱えるよう拡張してみた。([ruby-list: 32180])　そういやruby-extに振るべきだったなぁ。あと、WStringベースでIO処理さえ出来ればStringを使わないで済むようになるかも…

λ. libpng.so.2 ステッ

そーいうのってどうかと思うけどなぁ。

λ. ところで、sonameが変わっているって事はABIが変わったって事で、APIが変わらずにABIが変わるって事も考えにくいし、きっとAPIだって変わってると思うんだよね。コンパイルしなおしただけでlibpng.so.3に乗り換えられるものなの?

λ. 読書

『Mr.FULLSWING 6』

鈴木 信也 [著]

『満月(フルムーン)をさがして 1』

『満月(フルムーン)をさがして 2』

種村 有菜 [著]

λ. GentzenのLK, LJ, NK, NJは何の略語?

ふと思って検索してみたらfj.sci.mathで情報を見つけた。(news,blade,Googleグループ)

LK

logistischer klassischer Kalkül

NK

natürlicher klassischer Kalkül

LJ

logistischer intuitionistischer Kalkül

NJ

natürlicher intuitionistischer Kalkül

λ. GPKIおよびLGPKIにおけるルート証明書配布方式の脆弱性と解決策

を読んだ。

λ. The Circulation of Good - Implementation of a cooperative information-gathering agent for Squeak.

未踏のこのプロジェクトの採択者の「Sakai Masahiro (酒井 雅裕)」という名前を見て、一瞬驚いた。

λ. ghc の新しい機能 Generalized Algebraic Data Types (GADT)

かなり今更だが、Inemuri nezumi diary (2004-10-08) よりメモ。言うまでもないけど、これがあると Phantom Types とか普通に使えるようになるし、色々と嬉しそうだ。

詳しくは、"Wobbly types: type inference for generalised algebraic data types" を見ればよさそうか。

あと、モデルとしては dependent types の場合と同じようなものを考えればよいのかな……

関連エントリ

• AVL木でGADTを試してみる
• AVL木でGADTを試してみる (2)
• Ωmega
• Programming with Static Invariants in Ωmega

λ. James Cheney 氏

Phantom Types の James Cheney 氏って AlphaProlog の人でもあったのか。ちょっとビックリ。

λ. アメリカ大統領選

個人的にはどっちかと言えば民主党よりも共和党に勝ってほしいと思ってるけど、さてどうなるやら。それにしてもアメリカの選挙は面白いなぁ。

λ. Last.fm標準クライアントがiPod対応

Last.fmのWindows用標準クライアント(現在バージョン1.3.2.13b)がいつのまにかiPodに対応していたので、iSprogglerを捨てて、こっちに戻した。 iSprogglerは若干動作が変だったので助かった。 さようなら、iSproggler。

λ. derivors

(後で書き直す)

Seven Trees 問題を定理自動証明器を使って解く - ヒビルテ(2008-10-29) でやったことを少し形式的に考えると、

• 指標 Σ1 = {+, T0, T1, …} と
• 公理 E1 = { +の可換/結合則, T1=T0+T2, T2=T1+T3, … }

からなるセオリー (Σ1, E1*) での定理 T1=T7 を、

• 指標 Σ2 = {+, ×, 1, T} と
• 公理 E2 = { +の可換/結合則, ×の可換/結合則, 分配則, 1×x=x, T=1+T×T }

からなるセオリー (Σ2, E2*) での定理 T=T⁷ へと写したことになる。

私は institution の thoery ってのはこういうのを扱うためにあるのかと思ったのだけど、theory morphism は指標射の一種なので演算子を演算子に写すのに対して、ここで使った写像は演算子である Tk を演算子ではなくただの項でしかない T^k に写しているので、theory morphism にはなっていないのだった。

derivors

institutionではこういうのにどう対処しているのかな思って、Joseph A Goguen, Rod M Burstall. Institutions: abstract model theory for specification and programming. J. ACM, Vol. 39, No. 1. (January 1992), pp. 95-146. を読むと、以下のようなことが書いてあった。

For equational logic, there is another category with theories as objects, but with derivors, which map operators in Σ to derived operators in Σ', that is, to Σ'-terms, as morphisms [45]; in fact, this kind of morphism agrees with the usual morphism notion for Lawvere theories [69].

---

• 45. GOGUEN, J., AND BURSTALL, R. Some fundamental algebraic tools for the semantics of computation. Part 1: Comma categories, colimits, signatures, and theories. Theoret. Comput. Sci. 31, 2 (1984), 175-209.
• 69. LAWVERE, F. W. Functorial semantics of algebraic theories, Proc. Nat. A cad. Sci., U.S.A. 50 (1963), 869-872.

普通の theory morphism の代わりにこのderivorというのを使えば扱えそうだ。 ただ特定のinstitutionに依存してしまっているのが嫌な感じではあるけど。

さらに、Burstall, R. M. and Goguen, J. A. (1980): The Semantics of Clear: A Specification Language. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh. には、もう少し詳しいことが書いてあった。

(Note that this category of theories has certain signature morphisms as its morphisms, another category with the same objects would have as its morphisms derivors which map operators in Σ to derived operators in Σ' i.e. terms in Σ' with a binding sequence for their variables; but we shall not need this more complicated category. For a discussion of derivors see Goguen and Burstall [1978].)

---

• Goguen, J.A. and Burstall, R.M. (1978) Some fundamental properties of algebraic theories: a tool for semantics of computation. DAI Research Report No. 53, Dept. of Artificial Intelligence, University of Edinburgh.

え? 「shall not need this more complicated category」ということはderivorは結局不要なの?　Goguen and Burstall [1978] は入手できなかったので、仕方ないので自分で考えてみた。

考えてみた

I=(Sig,Sen,Mod,|=) を単一ソートの代数セオリーのinstitutionとする。

まず、signature morphism の拡張として derivor を定義する。 derivor f : Σ1→Σ2 は、Σ1のn引数演算子σをΣ2のn引数の派生演算子(λx1,…,xn. …)へと写すものとする。 また、文e∈Sen(Σ1)についてe中の演算子σをf(σ)で置き換え正規化したものを f(e)とする。f(e)にはラムダ式は現れないのでf(e)∈Sen(Σ2)になっている。 また、E⊆Sen(Σ1)に対して f(E) = {f(e) | e∈E} と定義する。

Sigの射をderivorに拡張した institution I' を考えることが出来る。 そして、この I' で derivor f : Σ1→Σ2 がセオリー Th1=(Σ1,E1^・) からセオリー Th2=(Σ2,E2^・) への theory morphism になっている、すなわち f(E1)⊆E2^・ が成り立っているとする。 このとき φがTh1の定理(φ∈E1^・)ならばf(φ)はTh2の定理(f(φ)∈E2^・)になるのだけど、これをI'やderivorを直接使わずに言いたい。

そこで、以下からなるセオリーTh3=(Σ3, E3^・)を新たに考える。

• Σ3 = Σ1 + Σ2
• E3 = in2(E2) ∪ Ef
• where Ef = { in1(σ)(x1,…,xn)=in2(f(σ))(x1,…,xn) | σ∈Σ1 }

in2は明らかに Th2→Th3 の theory morphism になっていて in2(E2)⊆E3^・ が成り立つ。 また、fの条件から f(E1)⊆E2^・ なので、in2(f(E1))⊆in2(E2^・)⊆in2(E2)^・⊆E3^・ 。 ここで、Efより in1(φ)∈E3^・ ⇔ in2(f(φ))∈E3^・ なので in1(E1)⊆E3^・ となり、in1はTh1からTh2への theory morphism 。

次に、忘却関手 Mod(in2) : Mod(Th3)→Mod(Th2) には逆 F : Mod(Th2)→Mod(Th3) が存在するので、 in2(φ)∈E3^・ ⇔ ∀M3∈Mod(Th3). M3|=in2(φ) ⇔ ∀M2∈Mod(Th2). F(M2)|=in2(φ) ⇔ ∀M2∈Mod(Th2). Mod(in2)(F(M2))|=φ ⇔ ∀M2∈Mod(Th2). M2|=φ ⇔ φ∈E2^・ 。

これらを使うと、φ∈E1^・ から

• まず in1 : Th1→Th3 によって Th3 に移動して in1(φ)∈E3^・ を得て
• Th3 でそこから in2(f(φ))∈E3^・ を得て、
• 最後に in2 を逆に辿って f(φ)∈E2^・ を得る

という流れで考えることが出来る。

結局、トートロジーみたいなことしか言っていないのだけど、derivorを考える代わりに、Th2を拡張したセオリーTh3と theory morphism Th1→Th3 を考えれば、同様の推論は出来ると。

Seven Trees の場合

最初の問題を考えると、Th3=(Σ3, E3^・) は以下のようになる。

• Σ3 = {in1(+), in1(T0), in1(T1), …} ∪ {in2(+), in2(×), in2(1), in2(T)}
• E3 = { in2(+)の可換/結合則, in2(×)の可換/結合則, 分配則, in2(1)in2(×)x=x, in2(T)=in2(1)in2(+)in2(T)in2(×)in2(T) } ∪ {x in1(+) y = x in2(+) y, in1(T0)=in2(1), in1(T1)=in2(T), …}

そして、以下のように推論することが出来る。

• T1=T7 ∈ E1^・
• ⇒ in1(T1)=in1(T7) ∈ E3^・
• ⇔ in2(T)=in2(T⁷) ∈ E3^・
• ⇔ T=T⁷ ∈ E2^・

λ. PLDIr #3

PLDIの論文を読む PLDIr の第三回に参加。 今回はPLDI99の論文が対象で、私は以下の3本の論文を紹介した。 今回は準備不足だったなぁ。

• Whole Program Paths
• What is a Recursive Module?
• Efficient Incremental Run-Time Specialization for Free

自分の発表資料(PDF, PPT):

前回は15:00開始で21時くらいまでやっていたけど、今回は18:30くらいで終了。

その後、筑波大の川島 英之さんにお会いし、DataLogがオーバーレイ・ネットワークの記述やネットワークの検証の分野で見直されているという話*1や Data Intensive Computing / Data Centric Computing 、徳永隆治先生の話など、色々面白い話教えてもらった。