日々の流転

λ. 『圏論による論理学—高階論理とトポス』 清水 義夫

貸してもらったので、ざっと読んだ。 トポスに関しては元々あまり知らなかったこともあり勉強になったが、哲学的な話は正直よくわからなかった。

第一章　関数型高階論理

関数型高階論理 λ-h.o.l. の 定義は、プリミティブを少なくするために工夫している部分以外は普通。 λ-h.o.l は、型の一つとして真理値の型 t を持ち、命題はこの型を持つような項(≠型)であるような論理。 この論理だと命題それ自体は型にならないので、型理論からカリーハワード同型対応で得られる高階論理とは流儀が違う感じ(?)。 そういえば、「言語の意味論」の授業でモンタギュー文法とPTQをやったときに使った内包論理ILもこんな感じの高階論理だった(c.f. 言語の意味論(2006))。

と思ったら、簡易モンタギュー文法の話が出てきた。モンタギュー文法についてもう少し詳しい話を知りたい人は前述の「言語の意味論」の講義資料と、中村さんのノート「UG とPTQ の概要」とを読むと良いと思う。

第二章　トポス

圏論の諸概念とトポスを定義して λ-h.o.l. をトポスで解釈する。

トポスで解釈するといっても任意のトポスではなく、集合圏のトポスでの解釈。 なんだ、一般のトポスで解釈するんじゃないのね。 まあ、第一章で λ-h.o.l. は古典論理として定義されているので、任意のトポスで解釈することは出来ないのは当然だけど……λ-h.o.l.はなんでわざわざ古典論理にしたのかな。

ラムダ式に対する解釈の定義は、あまりフォーマルな定義にはなっていないが言いたいことは分かる。 ただ、論理記号 T, F, ¬, ∧ は略記法として導入していたので、それに対して明示的に定義を与えているのは変。 まあ、略記法に基づいて解釈しても同じものになるはずだけど。

それから、第一章で導入していた λ-h.o.l. の拡張には、確定記述(definite description)と自然数があったが、自然数しかトポスで解釈していないのは何故だろう。 (追記: 確定記述(definite description) - ヒビルテ (2008-04-03)で少し書いたが、確定記述の解釈にはコンテキストないしは継続のような概念が必要になるが、トポスにはそれらに直接対応する概念はないので、直接の翻訳は出来なくて当たり前。)

あと、λh.o.l. の集合圏のトポスでの解釈の健全性を証明していながら、完全性については全く触れていないのはちょっと拍子抜け。 トポスが「われわれの知性にとって普遍性かつ基底的な事態に根ざす言語」であることから、λ-h.o.l.が「われわれの知性にとって普遍性かつ基底的な事態」に係わっていることを主張するためには、単に解釈可能というだけでなく、完全性などのより強い性質を示さなくて良いのだろうか。 トポスはリッチな構造を持っている分、λ-h.o.l. に限らずいろんなものを解釈可能なわけで……

それから、トポスの定義で「始対象」「直和」「プッシュアウト」の存在条件が不要であることについては、証明はややこしいとかではぶかれていたが、どうやるんだろう。 トポスはよく知らないので、すぐにはわからなかった。 後でやってみる。

第三章　トポスの基本定理

著者がトポスの基本定理と呼ぶ以下の定理の証明。

E をトポスとし， B を E の任意の対象とする．このとき， E↓B もトポスである。

また A も E の任意の対象とし、f : A→B を E の矢とするとき、 E↓A と E↓B の間には， f^* : E↓B → E↓A および ∑_f : E↓A → E↓B, ∏_f : E↓A → E↓B なる関手 f^*, ∑_f, ∏_f が存在し，∑_f ⊣ f^* ⊣ ∏_f が成立する。

この本では Locally Cartesian Closed Category (LCCC) については言及されていないが、これは E↓B に subobject classifier が存在することと、E が LCCC であることとを示すことと同じ。

第四章　プルバック関手f^*の右-随伴関手∏_f

前章で一般的に証明していなかった部分のきちんとした証明。 結構面倒くさい。以前にrpfさんから elementary topos は LCCC になっていると聞いていたけど、そのときはこんなに面倒くさいとは思わなかったよ。

partial arrow classifier と singleton の概念をはじめて知った。 面白い。

この章が一番勉強になった。

第五章　リミット、空間性トポス、限量記号

.

結び

「多少比喩的にいえば」と断ってはあったものの、対象でトポスをスライスすることが何故「視座」を設定することになるのか分からなかった。 というか、ここで言っている「視座」が何なのか分からなかった。 LCCCによる型理論の解釈(c.f. On the Interpretation of Type Theory in Locally Cartesian Closed Categories)の場合だと、コンテキストに対応するので理解できないこともないのだけど。

他にも、哲学的なことに関しては、「示された」と書かれていることで、何故言えるのか論理を追うことが出来なかった部分が多い。

関連

• はてなダイアリー - 「圏論による論理学—高階論理とトポス」を含む日記
• lambda high order logic - 白のカピバラの逆極限 S144-3
  • nucさんによると結構酷い間違いもあったみたいだけど、すごい勢いで斜め読みしてたので気づかなかった……

λ. スライスのスライスはスライス

Γを圏Cの対象とすると、そのスライスである圏C/Γが定義できる。 さらに、σを圏C/Γの対象とすると、そのスライスである圏(C/Γ)/σが定義できる。

さらに、Cにプルバックが存在するとき、σ^* : C/Γ → C/dom(σ) を id_Γ ∈ |C/Γ| に適用すると、σ^* id_Γ ∈ |C/dom(σ)| と dom(σ^* id_Γ) ∈ |C| が得られる。 dom(σ^* id_Γ) を Γ・σ と書くことにすると、(C/Γ)/σ と C/(Γ・σ) は等しい。

LCCC(locally cartesian closed category, 局所デカルト閉圏)の名前は、全てのスライスがCCC(cartesian closed category, デカルト閉圏)であることからきているが、LCCCにはプルバックがあるので、LCCCのスライスはCCCであるだけでなく、それ自体LCCCになっている。

Categories for Everybody のLCCCの話に関係して小ネタ。

λ. 確定記述(definite description)

『圏論による論理学—高階論理とトポス』 に確定記述 ιx(φx) というものが出てきた。 「これは φx を満たす唯一つの x」を表す式で、一階述語論理での解釈はこんな感じになる。

ψ(ιx(φx)) := ∃x(∀y(φy ↔ y = x) ∧ ψx)

「これは部分継続を使って解釈できるじゃん♪」とか一瞬喜んだが、考えてみれば一般化量化子(generalized quantifier)なわけで、解釈できて当たり前だった。 しかも、そういえば hsPTQにも確定記述の the を一般化量化子として実装していたわけで、何をぼけているんだ、私。

関連

• “Continuations in Natural Language” by Chris Barker - ヒビルテ (2008-03-13)
• 『圏論による論理学—高階論理とトポス』 清水 義夫 - ヒビルテ (2008-04-01)

λ. topos の internal language は?

ふと思ったので、調べもせずに書く。

• CCCの internal language は単純型付ラムダ計算
• LCCCの internal language は ∑ と ∏ による依存型を持つ型理論

では topos の internal language は何だろうか?

基本的には、∑ と ∏ による依存型を持つ型理論に対して、subobject classifier に関する項と規則を追加すればよいのだとは思うが、もしmonomorphismの判定(judgement)を入れるとすると、結構大きな拡張になるような気がする。 どう形式化するものなんだろうか……

【2008-04-20追記】 トポス (数学) - Wikipedia に「Kripke-Joyalの意味論とよばれる手続きによって集合論的論理式をトポスの対象と射についての言明として解釈することができる」とあった。 Kripke-Joyalの意味論については知らないのだけど、この意味論はトポスに対して完全なのだろうか?

λ. 女性シンガー･ソングライター ALGEBRAデビュー!!

そのネーミングはどーなんだw

λ. “Polymorphic Delimited Continuations” by Kenichi Asai, Yukiyoshi Kameyama

先日の “Continuations in Natural Language” by Chris Barker - ヒビルテ (2008-03-13) に続いて、今度の Continuation Fest 2008 の予習のために読んだ。

(後で書く)

CPS変換に関しては、以前に読んだ Final Shift for Call/cc: Direct Implementation of Shift and Reset (cf. 20030503#c04) では、shift/reset をCPS変換する際には二重に変換して meta continuation なんてものがでてくるややこしいものだったが、ここで定義しているCPS変換だとそんなことはないんだな。 違いはどこにあるのだろう。

【2008-04-14追記】 継続フェスタの時に亀山先生に直接教えてもらってしまった。 昔から二通りの変換があり、ここで使っているCPS変換だと変換結果が末尾呼び出しの形になっておらず、call-by-valueとcall-by-nameで結果が変わったりと良い性質を満たさないそうだ。 ただ、単純かつこの論文の目的には十分なのでこちらを使用したらしい。

λ. 京都 (1)

清水寺

京都御苑

銀閣寺は工事中の上に人が大杉。侘びも寂びもあったもんじゃないね。

哲学の道も人が多過ぎで、散策どころではなかった。

南禅寺

λ. 記号モデル検査の並行ソフトウェアシステムへの応用について by 土屋達弘

を読んだ。記号モデル検査の非常に分かりやすい紹介と、並行ソフトウェアシステムへの応用についての話。

T よりも T^ を使ったほうが高速なのは何でだろう。

λ. 京都 (2)

お茶の入ったお風呂。

八坂神社と円山公園。

知恩院

野宮神社

落柿舎

竹林と嵯峨野トロッコ列車

天竜寺

渡月橋でお花見舟。

金閣寺

λ. 「テレビの前で、国民に真摯に謝罪すべきではないでしょうか」

年金の名寄せが完了しなかったことに関して、 民主党の議員が国会で 「テレビの前で、国民に真摯に謝罪すべきではないでしょうか」 と言っていた。 そっか、謝罪というのはテレビの前ですべきものなのか。 「国会で」とかではなく「テレビの前で」なんだな。 これは面白い発想だと思った。皮肉ではなく。

λ. 日本語の文法における限定継続?

継続フェスタ2008 (Continuation Fest 2008) のプログラムが公開されていた。 先日読んだ“Continuations in Natural Language”(c.f. ヒビルテ (2008-03-13))が面白かったので、自然言語系の話を期待していたのだけど、大竹塁氏の「Delimited continuation in the grammar of Japanese (日本語の文法における限定継続)」という講演があった。

A natural language expression can be represented as a kind of program. Any such program, if well-formed, can be evaluated in different domains such as orthography, phonology, and semantics. The resulting values are the spelling, pronunciation and meaning, respectively, of the grammatical expression of the language the program represents.

From this viewpoint, I will illustrate the use of delimited continuation in analyzing sentences in Japanese. In particular, the meaning of question words such as 誰 (dare) and 何 (nani) involve shift operator, and that of も (mo) and か (ka) function as reset.

面白そう。 「誰」とか「何」といった疑問詞(question words)が出てくるけど、これは疑問文の意味論の話なのだろうか。

疑問文の話だとすると、どんな話か私にはさっぱり予想がつかないけど、もし平叙文の話だとすると、

• [[ 誰か ]] := λP. [[か]] ([[誰]] P)
• [[ 誰 ]] := λP. P (shift (λk. k))
• [[ か ]] := λP. ∃x. (reset P) x
• [[ も ]] := λP. ∀x. (reset P) x

として、

[[ 誰かが歩く ]]
= [[誰か]] [[歩く]]
= (λP. [[か]] ([[誰]] P)) [[歩く]]
= [[か]] ([[誰]] [[歩く]])
= (λP. ∃x. (reset P) x) ((λP. P (shift (λk. k))) walk)
= ∃x. (reset (walk (shift (λk. k)))) x
= ∃x. (λx. (walk x)) x
= ∃x. walk x

みたいな解釈をするとか、そんな感じかなのかなぁ、と妄想。 (この形式化だとちょっとコジツケくさいけど)

λ. “Co-limits in topoi” by Robert Paré

Given a cartesian closed category E with subobject classifier t:l→Ω, it is shown that the functor Ω^{( )} : E^op→E is tripleable. Standard results from the theory of triples are then used to show that E has I-colimits if and only if it has I^op-limits. This gives a new proof of Mikkelsen's theorem which states that E has all finite colimits.

『圏論による論理学—高階論理とトポス』 清水 義夫 - ヒビルテ (2008-04-01) で、colimitの存在をtoposの定義から取り除けることについて「どうやるか分からなかった」と書いたけど、証明がこれに書いてあるらしいということをbonotakeさんに教えてもらった。

べき対象関手 Ω^{( )} : E^op→E は、自然同型 E(A, Ω^B) ≅ E(A×B, Ω) ≅ E(B×A, Ω) ≅ E(B, Ω^A) ≅ E^op(Ω^A, B) によって、自分自身を左随伴として持つ。 さらに、Ω^{( )} は tripleable (もしくはmonadic) 、すなわちE^opはこの随伴から定まるモナドの Eilenberg-Moore 代数の圏に等しい。 tripleableな関手に関するよく知られた結果(tripleable functor create limits)により、E における I^op-limit を E^op における I^op-limit に持ち上げられて、これは当然 E における I-colimit になってると。

流れは分かったが、tripleableであることの証明に使っている定理(Barr-Beck “crude tripleableness theorem” もしくは Beck's monadicity theorem)と、「tripleable functor create limits」をまだ理解できていないので、これを読んだだけではあまり分かった気になれず。 その辺りの話は Toposes, Triples and Theories の「3.3. Tripleability」「3.4. Properties of Tripleable Functors」あたりに超詳しく載っているみたいだけど。

λ. nobsunが生徒になってくれる人を募集している

• 生徒になってくれる人募集 - HaHaHa! - haskell

nobsunが生徒になってくれる人を募集している。 nobsunに対面で直接教えてもらえるなんて、多分すごくラッキーなことだと思うので、Haskellプログラミングに興味のある入門者の方は応募してみてはいかがでしょうか。

λ. みんなの論文サイト Sesame!

「みんなの論文サイト Sesame!」というサイトを知った。CiteULikeに似ているけど、CiteULikeと違ってPubMedに特化したサービスみたい。 私は生命医学系の研究をしているわけではないので、今のところ関係ないか。 ただ、「公開レベルの設定」で「全公開」「グループ内公開」「非公開」が分けられるのはCiteULikeよりも便利そう。

Sesame(セサミ)は、元生物学系研究者がその研究経験を生かし『研究者にもっと研究に専念できる環境を！』というコンセプトに基に活動をしている団体です。

その中で、本HP「みんなの論文サイト Sesame!」は研究活動に欠かせない論文「情報収集→整理→共有」をらくらく快適にすることを目的に、研究者視点から開発した、研究者のための情報管理サイトです。2007年2月からサービスをスタートしています。

λ. PPL2008のカテゴリ1論文が公開

PPL2008のプログラムのページで、カテゴリ1の論文が公開されてました。 非常に面白い話が多かったので、参加されなかった方で興味のある方は見てみると良いのではないかと思います。 ちなみに、私のも載ってます(ぼそっ

あと、カテゴリ1の論文と出版済みのカテゴリ2の論文は私のCiteULikeのブックマークにも登録してあるので、CiteULike使っている人は、よかったらこちらもどうぞ。CiteULike: msakai ppl2008

λ. スライスがCCCのときのプルバックの右随伴

メモ。

圏Cの全てのスライスがCCCであるとき、C上の射 F: A→B からプルバックによって定義される関手 F^*: C/B→C/A が右随伴 ∏_F: C/A→C/B を持つことを示す。

p∈|C/A| とすると、pはCにおける dom(p)→Aという射で、C/Bの(F∘p)→Fという射でもある。

また、F∈|C/B| で C/B はCCCなので (-)^F : C/B → C/B という関手が出来、これを適用すると p^F : (F∘p)^F → F^F が得られる。 そこで、これと curry(π₂) : 1 → F^F とのプルバックで ∏_F(p)∈|C/B| を定義する。 (C/B にプルバックが存在することは、この間の「スライスのスライスはスライス」から言える)

そうすると、以下が自然な対応になる。

• X→∏_F(p) in C/B
• f : X→(F∘p)^F in C/B such that p^F∘f = curry(π₂)∘!
• g : X×F→(F∘p) in C/B such that p∘g = π₂
• g : (F∘F^*X)→(F∘p) in C/B such that p∘g = F^*X
• g : F^*X→p in C/A

λ. coarbitrary と双対を表す“co-”の由来

shelarcyさんの連載「本物のプログラマはHaskellを使う」の第18回　QuickCheckを使ってできることとできないことっで、coarbitraryについて以下のように説明されていた。

coarbitraryとは何でしょうか？「coarbitraryメソッドが第1引数として型変数aの値を取って最終的に型変数b（またはc）の値を返す」という関係と「arbitraryクラスのインスタンスであるa -> bが型変数aの値を取って型変数bの値を返す」という関係は同じものです。つまり，「ある部分から見て*と共通の関係を持つもの」を「co*」と呼ぶのです。関係が逆になる場合には「contra*」と呼びます。この関係を覚えておけば，coやcontraといった接頭辞が付く名前を見たときに戸惑わずに済むでしょう。

けど、coarbitraryの“co-”ってその“co-”なんでしょうか(ソース希望)。

私は、arbitrary が乱数から値を生成するgeneratorなのに対して、coarbitraryは「引数を使って乱数に作用する(ようgeneratorを変換する)」というある種の双対的な機能を持っているからだと思っていました。 本人らに聞いたわけではないので、あくまで憶測ですが。

あと、双対を表す“co-”を通常の“co-”の意味から説明しようとする のはやめておいた方が良いでしょう。 categoriesメーリングリストでの話<URL:http://www.mta.ca/~cat-dist/catlist/1999/co-prefix>を読むと、ややこしいことになってるのが分かると思います。

λ. 定期を忘れた

朝、定期を家に忘れて出てきてしまった。 途中で気づいたのだけど、そこから戻ると40分くらいロスしてしまうこともあり、そのまま切符を買って行った。 色々合計して約1500円の損失。 しょぼーん。

反省点:

• JRは切符を買ってしまったけど、Suica定期券を再発行してもらうという手もあった。手数料500円とデポジット500円をとられるが、後で忘れたSuica定期券を返還してデポジット500円を取り返せば、500円の損失だけで済んだはず。
• バスは現金で払ってしまったけど、その場で運転手さんからバスカードを買えばよかった。バスカードの割引率(15%)分だけもったいないことをした。

λ. 第三十九回圏論勉強会

今日は圏論勉強会。

The Haskell Programmer's Guide to the IO Monad — Don't Panic を読む三回目で、モナドから。

λ. 継続フェスタ2008 (Continuation Fest 2008)

遅れていったら、会場が既にでびっくり。

田中裕一さんに久しぶりに会えて懐かしかったのと、田中さんの師匠の渡部卓雄先生にお会いできて良かった。 しかし、 higeponさんやlethevertさんも来ていたのね。 いつものRHGっぽいメンバでつるんでいたら、挨拶しそこねてしまった。 もったいないことをした。

(後で書く)

Typing printf (継続を使った printf の型付け) by 浅井 健一

遅れていった＆資料を会場に忘れてきてしまったので、内容を把握していないのだけど、タイトルからすると“Polymorphic Delimited Continuations”(c.f. ヒビルテ (2008-04-05)) で例として使われていた話だと思う。

Demo of persistent delimited continuations in OCaml for nested web transactions (入れ子になった web トランザクションのための永続的限定継続のデモ) by Oleg Kiselyov

キャプチャした部分継続をディスクに書き出すというのが、Kahuaとかと違う点か。 実装については良く分からず。

Various use of continuations in Kahua - Application in practical web programming experience - (Kahuaにおける継続の様々な使い方 - プラクティカルな webプログラミングの経験 -) by 伊東 勝利

.

Delimited continuation in the grammar of Japanese (日本語の文法における限定継続) by 大竹 塁

日本語の文法における限定継続? - ヒビルテ (2008-04-07) では「誰か」「誰も」の「か」「も」を直接 reset に対応させるためにコジツケっぽいことをしたけど、実際には「誰も」を単に「shift k. ∀x. k x」で解釈するような解釈だった。 Chris Barker の “Continuations in Natural Language”(c.f. ヒビルテ (2008-03-13)) ではCPSで書かれていたけど、shift/reset を使って書けばこうなるかという感じ。

Focusや疑問文の話もあった。

「太郎が誰を褒めましたか?」は「Q λx. praised(taro, x)」で解釈するのか。 疑問文を扱うためのオペレータQを関数に対して適用することで疑問文を扱うのね。面白い。 ただ、Qの意味論はどうなっているんだろう。

Continuations for video decoding and scrubbing (ビデオのデコードとスクラビングのための継続) by Conrad Parker

.

Continuing from the past: An approach to building dynamically upgradable applications (過去からの継続: 動的に更新可能なアプリケーションを構築するアプローチ) by 渡部 卓雄 and 田中 裕一

.

How to implement continuation only language in gcc 4.x (gcc4.x を使った「継続オンリーな言語」の実装法) by 河野 真治

Implementing Continuation based language in GCC に資料あり。

懇親会で聞いた話が面白かった。

Ruby Continuation (Ruby における継続) by 笹田 耕一

前田さん犯罪者扱いヒドスwww

callccメソッドの名前を call_with_current_continuation__if_you_call_this_method__we_cant_guarantee_normal_execution とかに変えるというアイディア。

Ruby's Full Continuation Considered Harmful

dynamic-wind の話が出ていたので、「Why ruby lacks dynamic-wind? Is there any difficulties that are specific to ruby?」とか質問してみたら、「No one proposed it.」とのこと。 rubyでcall/ccを真面目に使っている人なんか誰もいないことの一つの証左かと思う。

【2009-02-14追記】 ku-ma-meさんによる dynamic-wind の実装: Ruby に callcc を公式にサポートさせよう - まめめも

λ. Mozyを使い始めた

オンラインバックアップサービス「Mozy」を使ってみた − ＠IT で紹介されていたオンラインバックアップサービスの Mozy を使い始めた。

詳しい説明は＠ITにあるけど、無料で2GBまで使えるというのは素晴らしいし、非常に手軽で便利。また、自宅の別ハードディスクにバックアップするのに比べて、オンラインバックアップサービスは地理的なリスクを分散出来て良さそうだ。 暗号化に用いる鍵はMozyの用意する鍵を使うことも出来るかが、念のため自分で鍵を用意して使うことにした*1。

ちなみに、紹介システムがあって、以下のリンクから Mozy のホームページに行って登録すると、登録者と紹介者(私)が二人とも256MBの容量を余分にもらえるみたい。

• <URL:https://mozy.com/?ref=ZKLCNC>

λ. GADTに対するexhaustiveなパターンマッチ

exhaustive な switch - まめめも で思い出したが、GADTに対してパターンマッチするとき、型による制約から実際にはexhaustiveなパターンマッチなのに、GHCがそれを認識してくれなくて悲しいことがある。 例えば、こんな感じのコードの場合。

data T a where
    Foo :: T Bool
    Bar :: T Int

f :: T Bool -> Int
f Foo = 0

これってGHCの実装が不十分なため?　 それとも本質的に判定不可能なものなのだろうか。

λ. 研究室ページがリニューアル

萩野・服部研のトップページがリニューアルされていた。 何かかっこいいぞ。 SilverStripeかぁ。

ちなみに、このスクリーンショットの撮影にはFireShotを使用。

λ. 萩野・服部研の新歓

萩野・服部研の新歓に参加してきた。

λ. 『日経ビジネス』ビジネス世論アンケートでプレゼントにあたった

『日経ビジネス』　ビジネス世論アンケート でプレゼントにあたった。わーい。

λ. "Scott is not always sober” by Peter T. Johnstone

20050310#p04 で知ってからずっと読みたかったものをようやく読んだ 。 私の持っている位相の知識が偏っていることもあり、理解するのに結構苦労した。 何しろ、私の位相の知識は Topology via Logic (Cambridge Tracts in Theoretical Computer Science)(Steven Vickers) と 位相と論理 (日評数学選書)(田中 俊一) で得た知識なので……

(以下、書きかけメモ)

Topology via logic から予備知識

Sober空間の specialization ordering が directed complete であることと、開集合が“inaccessible by directed joins”であることにについては、Topology via Logic では p.94 Theorem 7.2.3 で示されている。 また、Sober空間の開集合は“inaccessible by directed joins”なので、specialization ordering の上のスコット位相の開集合にもなっている。

irreducible の定義は、Topology via Logic では p.66 。 irreducible な閉集合は素な開集合の補集合。

X上のSoberな位相Ωが存在しないことを示す部分

aの反例の最後のところので、何故そのような位相Ωが存在しないか最初わからなかったが、しばらく考えて納得した。

XはSober空間の irreducible な閉集合なので、対応する generic point x が存在して、任意の開集合Uについて x∈U ⇔ U∩X≠∅ 。ということは、空でない開集合は x を含む。そのような x は存在すれば最大元だけど、X には最大元はないので、そんな位相は存在し得ない。

⋃{ cl{y} | y∈F, y≰x } は 閉集合

一応示してみたが、イマイチ。

M := F∩(N×{∞}) とおく。 properな閉集合Fの補集合であるところの空でない開集合Uは、あるnについて {(m', ∞) | m'≧n} を含むので、Mの要素は {(m', ∞) | m' < n} に含まれ有限個。

Fの極大元 x について L=⋃{ cl{y} | y∈F, y≰x } ⊆ F を考え、これは閉集合になっていることを示す。

Lがlower-closedであることは明らか。

Lがdirected-join について閉じていること。 与えられた有向部分集合が最大元を含む場合には明らか。 最大元を含まない有向部分集合 D⊆L は {m}×(N ∪ {∞}) ⊆ F に含まれる無限集合の場合。 このDの上限 (m, ∞) は F に含まれる(Fはスコット閉集合でdirected-joinに閉じているので)。 ここで (m, ∞) = x とすると、D が L に含まれることに矛盾してしまう(Mが有限個なのでDの有限個の要素しかしかカバーできない)ので、(m, ∞) ≠ x 。(m, ∞) ≰ x なので、(m, ∞) ∈ cl{(m, ∞)} ⊆ L 。

irreducible な F が generic point を持つ

これも一応示せはしたけど、イマイチ。

M≠∅ の場合、F ⊆ ⋃{cl{m} | m∈M} ∪ ⋂{⋃{cl{y} | y∈F, ¬(y≦m)} | m∈M} で、Mは有限集合なのとFがirreducibleであることから、(∃m∈M. F ⊆ cl{m}) ∨ (F ⊆ ⋂{⋃{cl{y} | y∈F, ¬(y≦m)} | m∈M}) 。

• ∃m∈M. F⊆cl{m} の時、Fは{m}を含む閉集合なので F⊇cl{m} で F=cl{m} 。 m≠m' ならば cl{m}≠cl{m'} なのでmの一意性は明らか。
• F ⊆ ⋂{⋃{cl{y} | y∈F, y≰m} | m∈M} の時 ∀m∈M. F ⊆ ⋃{cl{y} | y∈F, y≰m} で M≠∅なので ∃m∈M⊆F. ∃y∈F. m∈cl{y} ∧ m≠y で、これは矛盾

M=∅ の場合: F_n := F∩({n}×N) とおくと、空でない F_n は最大元を持つ閉集合。 F_n = F for some n∈N である場合 F = cl{∨F_n} 。 そうでない場合、F_n≠∅ と G := ⋃{F_n' | n'≠n} ≠ ∅ は閉集合で、FをF_nとGに分割できるので、irreducible であることに矛盾。

λ. パイレーツオブカリビアン

テレビでやっていたので観た。 アンデッドがガシガシ動くのが楽しい。

λ. hsPTQ 0.0.2

hsPTQは一年以上前に作ったまま、ずっとソースコードを公開するのを忘れていたのだけど、ようやく公開した。公開にあたっては一応Cabal化してみた。

PTQというのは R.Montague の論文「The Proper Treatment of Quantification in Ordinary English」からきていて、英語の平叙文のサブセットに対して形式言語と同様の形式的な意味論を与えるものです。 hsPTQはそのPTQをHaskellで実装したもの。 ちょっとしたオモチャだけど、なかなか面白いものだと思うので、向井先生の言語の意味論(2006)の講義資料などを参照しながら、遊んでみてください。

なお、PTQの意義とかは郡司先生の「モンタギュー (Richard Montague 1930–1971) — 自然言語に対する形式意味論の実現者」が分かりやすいです。

λ. ステルス

テレビでやっていたので観た。 映像は良かったけど、なんとも能天気かつご都合主義のストーリー。 あと、死にそうだと思っていたキャラが速攻で死んでうけた。

λ. 『宇宙に知的生命体は存在するのか』 佐藤 勝彦 (編)

を読んだ。 帯に「われわれがETに出会う日は近い！」と痛いことが書いてあった*1のだけど、中身はまともで宇宙に関する各分野の研究者が最近の研究について語っている。 ただ、彼らが面白いと感じているのは分かるのだけど、その面白さがイマイチ伝わってこない感じ。Simon Singh とまでは言わないけど、もう少し何とかならなかったのかなぁ、と少し残念。

λ. “The Essense of the Iterator Pattern” by Jeremy Gibbons and Bruno C. d. S. Oliveira

The Iterator pattern gives a clean interface for element-by-element access to a collection, independent of the collection's shape. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating. Various existing functional models of iteration capture one or other of these aspects, but not both simultaneously. We argue that McBride and Paterson's applicative functors, and in particular the corresponding traverse operator, do exactly this, and therefore capture the essence of the Iterator pattern. Moreover, they do so in a way that nicely supports modular programming.We present some axioms for traversal, discuss modularity concerns, and illustrate with a simple example, the wordcount problem.

を読んだ。

Applicative Programming with Effects (c.f. ヒビルテ(2006-12-07)) の applicative functor を使ってイテレータパターンの本質を解き明かす。 HaskellのData.Traversableモジュール辺りはこの論文に基づいている。

関連

• <URL:http://lambda-the-ultimate.org/node/1410>

λ. マルバツゲーム Haskellで どう書く？org

初めてどう書く？orgに書いてみた。

λ. “The Path Category in ALF and AGDA” by Ilya Beylin

We compare different definitions of the path category in type theory and two of its implementations, ALF and AGDA. For our purposes, both ALF and AGDA implement the logical framework of [NPS90], but support two different versions of inductive definitions. It appears that in ALF we can define the path category in a natural way, and in AGDA it is not possible.

を読んだ。

圏を型理論で形式化するときには、以下の二つの流儀がある。

1. Obj, Arr ∈ Set と src, target ∈ Arr → Obj で扱う方法
2. Obj ∈ Set と Hom ∈ Obj → Obj → Set で扱う方法

が、後者の流儀でHomをSetoidにした E-category が、色々な概念を自然に形式化することが出来て良いそうだ。

それで、Path category (有向グラフから自由生成される圏で、元のグラフの頂点が対象、元のグラフのパスが射になる) を Alf と Agda で書くとどうなるかという話。 当時の Agda には inductive families がなかったのでパスのデータ型が定義できなかった。

λ. お菓子買いだめ

買いだめというほどではなくなってしまったけど。

λ. 連休前に

連休前に色々片付けたかったが、あんまし片付かなかった。

λ. RHG読書会::東京 Practical Common Lisp

第11章 コレクション から。

しかし、common lisp では一つ一つの関数が異様に高機能だな。 大クラス主義ならぬ大関数主義?

λ. “Checking Race Freedom via Linear Programming” by Tachio Terauchi

We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to (rational) linear programming. Unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. We achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying an implementation to real world C programs.

を読んだ。先日のPPL2008で発表されていたもの。そのときはちょっと良く分からなかったのだけど、改めて読んでみるとやっぱり面白いなぁ。線形計画法(linear programming)をこんなことに使えるなんて思いもよらなかった。

リファレンスにアクセスする権限をスレッド間で分け合ったり受け渡したりする。権限を少しでも持っていれば読み込みが出来て、権限を全部持っていると書き込みが出来る。それで、権限を非負の有理数で、制約を不等式で表現して、線形計画法のソルバを使って制約を充足するような割り当てが存在するかをチェックする。

C言語とpthreadで書かれたプログラムを検証するためのプロトタイプが実装済み。フロントエンドしてCILを使い、線形計画法のソルバにはGLPK (GNU Linear Programming Kit)を使っている。

ちょうど半年前くらいにGLPKとGLPKで楽しく最適化しよう！というページを知人に教えてもらったんだけど、それにしてもこんなことに使えるとは……

λ. パニックルーム

テレビでやっていたので見た。 こんな狭い舞台でどんな話が展開するのかと思ったが、結構面白かった。

λ. 正規表現にマッチする文字列をAlloyで生成する

• 正規表現からその正規表現にマッチするような例を生成する - soutaro#nikki()
• 正規表現にマッチする例 - d.y.d.
• 大人げ - sumiiの日記

辺りの話を思い出し、そういえばこれってモデル生成の話だから、Alloy Analyzer で出来そうだなと思ってやってみた。 結果としては特に面白くもなかったけど。 Regex.als

まず、文字列を表すための指標を用意。 個々の文字はCharをextendsする指標として定義する。

abstract sig Char {}

abstract sig String {}
one sig Nil extends String {}
sig Cons extends String {
　 head : one Char,
   tail : one String
}
fact {
   all s : Cons | not (s in s.^tail)
}

でもって、正規表現を文字列に関する論理式に変換するのだけど、DCG方式で差分リストに対する述語として定義する。 そうすると、大体以下のような感じで解釈することになる。

• [[ ]](x,y) = (x==y)
• [[ . ]](x,y) = (x.tail==y)
• [[ c ]](x,y) = (x.tail==y && x.head==c)
• [[ e1 e2 ]](x,y) = some z : String | [[ e1 ]](x,z) && [[ e2 ]](z,y)
• [[ e1|e2 ]](x,y) = ([[ e1 ]](x,y) || [[ e2 ]](x,y))
• [[ e? ]](x,y) = ([[ e ]](x,y) || x==y)
• [[ e* ]](x,y) = some r : String -> String { (all x,y : String | y in x.r <=> [[ e ]](x,y)) && y in x.*r }
• [[ e+ ]](x,y) = some r : String -> String { (all x,y : String | y in x.r <=> [[ e ]](x,y)) && y in x.^r }
• [[ [ab...] ]](x,y) = (x.tail==y && x.head in a+b+...)

Alloyでは述語の帰納的な定義が出来ないので、繰り返しはreifyした関係の(反射)推移閉包を使って表現するのがポイント。 というか、それをしたかったので差分リストに対する述語として形式化したんだけどね。 なお、今回は否定や補集合は扱っていないけど、それらを扱う際には関係rの量化と定義を否定の内側ではなく一番外側に持ってくる必要があるので注意。

そうすると、例えば「goo+gle」という正規表現は以下のようになる。

pred google(x : String) { google[x, Nil] }
pred google(x, y : String) {  
  some a, b, c, d, e : String {
    x.head==C_g
    x.tail==a
    a.head==C_o
    a.tail==b
    many1_o[b,c]
    c.head==C_g
    c.tail==d
    d.head==C_l
    d.tail==e
    e.head==C_e
    e.tail==y
  }
}

-- o+
pred many1_o(x, y : String) {
  some r : String -> String {
    all x, y : String | y in x.r <=> x.head==C_o && x.tail==y
    y in x.^r
  }
}

でもって、テスト。

pred test_google() {
  some x : String {
    google[x]
    all y : String | y in x.*tail
  }
}

run test_google for 10

runすると、それっぽい結果が出てくる。

お題の正規表現についても同様。

λ. 世にも奇妙な物語 — SMAPの特別編

懐かしいなぁ。 最初の「エキストラ」の話は以前は見逃していた気がする。

λ. 「形式的体系の定理証明支援系上での実現法」資料

を読んだ。 AgdaによるHoare論理の形式化と、whileプログラムの遷移系での解釈に対するHoare論理の健全性の証明の話。 ところで、「ホア論理」という呼び方は初めて見た……

λ. ACミラングッズ プレゼントキャンペーン

住信SBIネット銀行が「ACミラングッズ プレゼントキャンペーン」なるものをやっていたので、定期で5万円預けてみた。

λ. 黄泉比良坂(よもつひらさか)の岩戸

ディスコミュニケーションの第9話「まなつのよるのゆめ」に「千年ぶりに黄泉への岩戸が開く瞬間を……」というセリフがあったのだけど、古事記の舞台は千年前よりもずっと昔の話だし、ここで千年前に岩戸が開いたと言っているのは何を指しているのだろう?

λ. A Bisimulation for Type Abstraction and Recursion by Eijiro Sumii and Benjamin C. Pierce

住井さんが第７回船井情報科学奨励賞という賞を受賞した*1とのことで、よい機会なので、記事で関連論文としてあがっていた A Bisimulation for Type Abstraction and Recursion のPOP2006のときのスライドを眺めてみる。 以前に少し伺ったこともあったけど、これは想像以上に面白そう。

λ. NEXT

観てきた。ちょっと前に某所で「可能世界だ」とか「様相論理だ」とか面白がってた映画。結構アホっぽい感じの娯楽映画で、伏線も謎もあったもんじゃないけど、ニコラス・ケイジが能力を駆使して活躍する様はそれなりに楽しめた。

【追記】 2008-05-01の毎日新聞夕刊の「シネマの週末」では「よほどおおらかな気分で見ないと、主人公の分身シーンなど、キテレツな場面の連続にあぜんとさせられるだろう」と書いてあったけど、個人的には分身等の表現は「有界モデル検査(bounded model checking)をこう視覚化したか」という感じで、結構面白かったんだが。

λ. CPLのHaskell版パッケージをCabal化

CPLのHaskell版パッケージをCabal化した。 もうコードを書いたのが昔過ぎて、コードを見返すのが面倒くさかった。