日々の流転

λ. MAD PEOPLE β01: EPISODE 1101 「でかマクロとぷちマクロ」

<URL:http://straws.sakura.ne.jp/madb01/index.cgi?bid=1101> に参加していた。

λ. 入社式

今日から社会人に。 集合時間が朝早かったこともあり、今日は少し疲れた。

λ. 太った

先日の健康診断の結果を昨日の入社式の時に受け取ったのだが、50キロ台後半だった体重が60キロ台後半に増えていた。ついでにコレステロールが……。元々痩せ気味だったので多少の体重増加は悪くなかったが、流石に増えすぎ。気付いてみたら、なんとお腹の肉がつまめるんだよなぁ。

これはM2の荒んだ生活の結果だろう。 色々とまずいので、健康的な生活をしなければと思った。 そして、60キロ台前半くらいに体重を調整しよう。

λ. Scott open filters & Compactness

通勤時間等に位相のお勉強。 4年前くらい前、Scott open filters とコンパクト性が理解できなくて悔しかったのだが、今同じところを見直したら簡単で普通に理解できた。 locale D で ΩD の scott open filters と D の compact saturated sets が対応するという Hofmann–Mislove (Scott Open Filter) Theorem も理解できた。

λ. 正規分布とシックスシグマ

<URL:http://en.wikipedia.org/wiki/Six_Sigma>によると、3.5 DPMO に対応するのは6σではなく4.5σなのか。ふむ。

λ. 研修は続くよどこまでも♪

実際に配属先に配属されるのが6月半ばで、それまで延々と研修やら何やらがあるのは面倒くさすぎる、と最初は思っていた。 しかし、考えてみれば「会社のお金で研修を受けて、しかも給料までもらえる」というのは素晴らしい状況である。 20070404#c06でも書いたが、折角の機会なので、自分に欠けていたものを貪欲に吸収したい。

λ. 薬剤師国家試験

弟が薬剤師国家試験に無事合格していた。めでたい。

λ. チコノフの定理

コンパクト性を理解できたので、今度はチコノフの定理(Tychonoff's Theorem)。今読んでいる Topology via Logic には有限個の直積の場合の証明しか載っていないが、それでも証明を追いかけるのに結構苦労した。まだ、コンパクト性の扱いに慣れていないのかも。

それから、位相空間だけでなくLocaleでもチコノフの定理は成り立つそうだ。しかし、両者の一般化である Topological System への一般化は知らないとのこと。何だか少し不思議だ。

λ. ideal completion

Spaciality of products と Local compactness and function spaces はとりあえず飛ばし、Spectral Algebraic Locales の章に突入。

で、標記の ideal completion (イデアル完備化?) で少し混乱。 poset P の ideal completion Idl(P) の順序は ⊆ で与えられ、meet I∧J は I∩J と一致するが、join I∨J は I∪J と一致するとは限らないので注意。 I∪J はイデアルでないかも知れない。

ちなみに、ここで言っているイデアルは環(ring)のイデアルではなく、半順序集合(poset)のイデアルで、lower closed で directed な部分集合の意味。そして、Idl(P)はPのイデアル全体を台集合として⊆で順序をいれたもの。 「イデアル」で順序集合のほうをイメージするのは少数派らしい。 たしかブール環を考えれば両者は一致したはず。

λ. 選挙

神奈川県知事選と神奈川県議員選。投票してきた。

λ. ノイズキャンセラ付ヘッドホンを買ってみた

これまで iPod nano で使っていた ATH-CK32 BK (20061018#p01) が壊れてしまった。左耳の方が断線しているっぽい。またカナル型のイヤホンを買おうかと思ったが、どうせなので今度はノイズキャンセラ付のヘッドホンを買ってみた。買ったのはSE-MJ7NSというやつ*1。

ちょっと使ってみた限りでは、やっぱりカナル型のイヤホンの方が良かったかも、と思った。

• 当然イヤホンよりも音質は良いし、ノイズキャンセラも結構良いが、私はPodcastで音楽以外を聴くのがメインなので、ちゃんと聴ければ音質はどうでも良い。カナル型イヤホンでも電車内で聴くのに困ることは無かった。
• イヤホンに比べて持ち運びにかさばる。
• 耳が暑苦しいので、これからの季節、長時間の着用が困難。

λ. 一からホモロジー ― 数学やってない人にも分かるホモロジー入門

を読んだ。 私は「ホモロジーでは図形の不変量を考える」という事だけは聞いた事があったが、具体的にどう考えるのか知らなかったので、面白かった。

λ. 合宿

今日から二泊三日で合宿。

λ. spectral locale と compact coprime opens

Topology via Logic の p.122。「Definition 9.3.3: A spectral locale D is a spectral algebraic locale iff every compact open can be expressed as a finite join of compact, coprime opens.」の後の「It follows that in a spectral locale every open is a join (not necessarily finite) of compact coprimes」に2日くらい悩んでいたのだが、これってひょっとして条件の「spectral locale」が「spectral algebraic locale」の間違いだったというオチ?

λ. ドメイン認証の問題点と解決案

を読んだ。/.J の IPアドレスの最近傍識別を行うSPAM Filter より。

λ. RHG読書会::東京 入門JavaScript 第四回

先月はなかったので二ヶ月ぶり。 RHG読書会みたいな楽しさは久しぶりで、なんだか元気をもらった気がする。

jsthread

牧さんのjsthreadの話が面白かった。jsthreadはプリエンプティブなスレッドを実装したJavaScriptライブラリ。

• <URL:http://sourceforge.net/projects/jsthread/>
• <URL:http://jsthread.sourceforge.net/>

今回の話を聞くまでは「CPS変換して継続呼び出しをsetTimeoutを介するようにすれば良いだけじゃん」とか思っていたのだが、実際に話を聴いたら面白かった。

Function#toStringで取得した関数のソースコードをパースし Trampolined Style に変換する。そして、変換結果をその関数のプロパティに保存しておく。このライブラリは関数を呼ぶ際にこのプロパティが存在するかチェックし、存在しない場合には普通の関数呼び出しを行い、存在する場合にはそれをスケジューラに渡して呼び出す。 このようになっているために、変換されていないコードから変換済みの関数を呼び出す際にも問題が起こらないようになっている。 考えてみればJavaScriptらしい自然な設計ではあるが、細かいところまで良く出来ていると感じた。

本質的な問題は変換対象の関数が自由変数を含む場合。JavaScriptには環境を明示的に操作する機能はないと思うので、自由変数にアクセスできないはず。 ……と思ったが、Firefoxではevalの第二引数を使うことで以下のようにアクセスできた。IEやOperaではダメだったけど。

var f = (function(x){ return function(){ return x } })(10)
eval("x", f) //=> 10
eval("function(z){x=z}", f)(100)

ということは、Firefoxのことだけを考えるのなら jsthread-fv-firefox.diff のようにすれば良い。

それから、JavaScriptのパーサがソースコード中の大きな量を占めている。個人的に「JavaScriptでパーサはあまり書きたくないなぁ」と思っていたが……　なお、パーサはRhinoのコードを翻訳したそうで、拡張構文(?)もそのまま使えるそうだ。

あと、このような変換ではプログラムの意味が変わってしまうので、変換の正当性をどのように定義するかが難しいそうだ。

関連

• ライフ - L'eclat des jours(2007-04-15)
• JavaScript でプリエンプティブなスレッドを - val it : α → α = fun

λ. 日本Ruby会議2007のチケット

今日10:00に発売で13:30頃に売り切れだったとか。 買えなかった……しょぼーん。

というか、そもそも今日発売だったこと自体を知らなかった。 最近アンテナが低すぎな私 orz

そういえば、プログラムをみて気付いたのだが、今回はむとうさんも発表するのだな。むとうさんはあまりこういうイベントには出てこない印象があったので楽しみ。

λ. Trampolined Style by Steven E. Ganz, Daniel P. Friedman and Mitchell Wand

• <URL:http://www.cs.indiana.edu/~sganz/publications/icfp99/paper.pdf>
• <URL:http://citeseer.ist.psu.edu/ganz99trampolined.html>

昨日のRHG読書会のjsthreadの話に出てきていたので、読んでみた。 control operator 系(?)の話は苦手で、読んでもあまり分かった気がしない。

Trampolined style で書かれた階乗のコードは以下。 基本的には末尾呼び出しの形式で、末尾で値を返す部分をreturn関数を介するように、末尾呼び出し部分をbounce関数を介するようにしてある。

(define fact-acc
  (lambda (n acc)
    (if (zero? n)
        (return acc)
        (bounce
         (lambda ()
           (fact-acc
            (sub1 n)
            (* acc n)))))))

(後で書くかも)

モナド等と違って T, return, bounce の満たすべき代数法則が与えられていないのが、何だか不思議。

λ. 風邪気味

先週の疲れが出たのか、体調が悪い。 今日は携帯の機種変更をしに行こうと思っていたが、ゆっくり休むことにする。

今日の研修は座学だったため、少し退屈だったが、体調がまだイマイチだったのでありがたかった。

λ. 「初歩の圏論」富士セミナー

[haskell-jp:87]よりメモ。

λ. システム・ソフトウェア #1 OSの歴史と基本概念

を観た。 見慣れた教室が懐かしくて、見ていて落ち着く(笑

• ビデオ
• 講義資料

λ. An Evaluation of the Ninth SOSP Submissions -or- How (and How Not) to Write a Good Systems Paper by Roy Levin and David D. Redell

システム・ソフトウェアの講義資料にあったので読んだ。 どんな投稿論文が良い論文と評価されるかを、以下の点から述べている。

1. Original Ideas
2. Reality
3. Lessons
4. Choices
5. Context
6. Focus
7. Presentation
8. Writing Style

システム系の論文が主な対象だが、多くの部分はそれ以外の分野にも適用できる。 もっと早くにこういうのを読んでいたかった。

λ. 風邪

また風邪引いたっぽいので、予定を色々取りやめ。 週末毎に体調崩してたら何も出来ないって…… orz

λ. WORLD ECONOMY #1 Introduction

を観た。 ODAの及ぼしうる悪影響の一つとして挙げられていた「ODA資金によって需要が増える一方で供給能力は増えずインフレが発生し、またそれによって国際競争力が低下するため産業が発展しなくなる」という話が面白かった。 というか、熱でぼーっとしていたので、ほとんどそれしか覚えていない(苦笑

λ. 携帯機種変更

これまで約3年使っていたA5403CAからW43CAへと機種変更。

学生時代は携帯はさほど重要ではなかったけど、社会人になって自分のPCに触れられる時間が著しく減ったため、携帯電話が重要になった。赤外線通信とPCサイトビュアーとQRコード読み取り機能が欲しくなったのが機種変更の主な理由。

しかし、慣れない機種に変更して思ったが、携帯のインターフェースって最悪だと思う。

例えば、ニュースフラッシュという機能がある。 勝手に無料でニュースを受信してくれて重宝しそうなのだけど、ニュースを受信するたびにメロディを鳴らされたりバイブを振動させられたりすると結構邪魔。 そこで、設定でメロディを消音にしバイブも無効にした。 マナーモードにしない場合にはこれで邪魔にならなくなるのだが、マナーモード(通常マナー)にしているとバイブが振動してしまう。 これはあまりに馬鹿げた設計だと思う。 ちなみに、FAQ「EZニュースフラッシュ関連　マナーモードで、EZニュースフラッシュの受信時にバイブレータを振動させないようにするには？」によると、マナーモードを「オリジナル」に設定して、個別に設定しなくてはならないとか…… (唖然

λ. 床屋

に行って、さっぱりしてきた。

λ. 古典と現在 #1 ガイダンス

を観た。

λ. 焼肉

合宿のときのチーム「インディジョーンズ」のメンバで焼肉。

λ. 特急あずさって

トラベルミステリーの中だけの存在じゃなくて、ちゃんと実在したのか(ぉ　今日初めて見た。

λ. Algebraic dcpo + 2/3 SFP + Scott位相 ⇒ Spectral algebraic space

Topology Via Logic の Lemma 9.3.7 に一週間くらい悩んでいたのだが、ようやく理解できた……気がする。

問題

この補題の中身は次のようなもの。

Let P be a poset satisfying the 2/3 SFP property of 9.3.6 (ii). Then Idl(P) with its Scott topology is a spectral algebraic space.

ただ、2/3 SFP property を満たすべきなのは P ではなく Idl(P) ではないかと思う。でないと話が繋がらない。

方針

Proposition 9.2.5 の

A topological space is spectral iff

• it is sober (localic),
• any finite intersection of compact open sets is still compact, and
• the compact open sets form a basis.

を使ってspectralであることを示す。

algebraicであることは普通に示す。

↑↓x はスコット開集合

Proposition 9.1.2 より ↓x は Idl(P) のコンパクトな要素で、 Definition 9.1.1 より ↑↓x はスコット開集合。

↑↓x は compact coprime open

↑↓x ⊆ ⋃S と仮定する。 このとき、↓x ∈ ⋃S なので、ある a∈S が存在して ↓x ∈ a 。 a は upper-closed なので、↑↓x ⊆ a 。

よって、↑↓x は compact coprime open 。

{↑↓x | x∈P} はスコット位相の基底

スコット開集合 a が与えられたとする。

b = ⋃{↑↓x | x∈P, ↑↓x⊆a} とおき a=b を示せば良い。 a⊇b は自明なので、a⊆b だけ示す。

y∈a が与えられたとする。 Idl(P)の代数性より S={↓x | x∈P, ↓x⊑y} とおくと y=⨆^↑S 。 スコット開集合 a は directed-join によって到達不能なので、 ある ↓x∈S が存在して ↓x∈a 。 aはupper-closedなので ↑↓x⊆a であり、bの定義から ↑↓x⊆b 。 一方、↓x⊑y より y∈↑↓x なので y∈b となる。

これでコンパクト開集合が基底になっていることが示せた。

コンパクト開集合は有限個の ↑↓x の和集合

コンパクト開集合 c が与えられたとする。 S={↑↓x | x∈P, ↑↓x⊆c} とおくと、 c=⋃S となる。 Sはcの開被覆なので、cのコンパクト性からSの有限部分集合Tが存在して c⊆⋃T。 c⊇⋃T は明らかなので c=⋃T。

コンパクト開集合が有限個の compact coprime open の和集合で表現できたので、この空間が spectral なら spectral algebraic であることが示せた。

コンパクト開集合の有限個のintersectionはコンパクト

まず、binaryな場合について。 コンパクト開集合 a, b が与えられたとする。 このとき有限集合 S, T が存在して、a = ⋃{↑↓x | x∈S}, b = ⋃{↑↓y | y∈T} であり、分配則から a∩b = ⋃{↑↓x∩↑↓y | (x,y)∈S×T} 。 S×T は有限であり、有限個の和集合ではコンパクト性は保存されるので、↑↓x∩↑↓y がコンパクトであることを示せば十分。

S={↓x, ↓y} に 2/3 SFP property を適用して、その complete set of upper bounds M が得られる。 そして、 w∈↑↓x∩↑↓y ⇔ ↓x⊑w and ↓y⊑w ⇔ ∃↓z∈M. ↓z⊑w ⇔ ∃↓z∈M. w∈↑↓z ⇔ w∈⋃{↑↓z | ↓z∈M} なので、↑↓x∩↑↓y = ⋃{ | ↓z∈M} が言える (2/3 SFP と algebraicity よりwがコンパクトでない場合についても問題ない)。 ↑↓x∩↑↓y は、有限個のコンパクト開集合の和集合として表せたので、コンパクト開集合。

この空間はSober

Idl(P) は preorder ではなく poset なので、この空間は T₀ であり、区別不可能な点は存在しない。 後は、この空間をlocalifyした空間の点に対応する点が、Idl(P)に元から含まれていることを示すだけ。

localifyした空間の点zが与えられているとする。 I={x∈P | z ⊨ ↑↓x} が目的の点であることを示す。 イデアルの条件のうち、lower-closedであることは明らかなので、finite-joinに関して閉じていることを示す。

SをIの有限部分集合とし、M⊆PをSのcomplete set of upper boundsとする。 w∈⋃{↑↓x | x∈S} ⇔ ∀x∈S. ↓x⊑w ⇔ ∃y∈M. ↓y⊑w ⇔ ∃y∈M. w∈↑↓y ⇔ w∈⋃{↑↓y | y∈M} より、⋂{↑↓x | x∈S}=⋃{↑↓y | y∈M} 。 z ⊨ ⋃{↑↓x | x∈S}=⋃{↑↓y | y∈M} より、あるy∈Mが存在して、z ⊨ ↑↓y 。よって、Iの定義より y∈I で、また y∈M はSのupper-boundであった。ゆえに、Iはイデアル。

λ. 無人駅とSuica/Pasmo

某駅にこんなのがあった。 無人駅っぽいところでもSuica/Pasmoを使えることに感動。

湘南モノレールもSuica/Pasmoが使えるようになれば良いのに、と思った。 色々難しそうだが。例えば、この路線の場合、ほとんどの利用者は有人の駅と無人の駅の間の移動だろうけど、モノレールの場合には無人駅の間の移動も結構ありそうだし。

λ. 初給料日

というわけで、初給料。 さて、何に使うか。

λ. 2/3 SFP と algebraicity

Topology via Logic では 2/3 SFP を以下のように定義している。

For each finite set S of compact points there is another such M (a complete set of upper bounds for S) such that

• each m∈M is an upper bound for S, and
• if m´ is any compact upper bound for S, then m´ ⊒ m for some m∈M.

この定義はm´はcompactであることを要求しているが、対象となる半順序集合が algebraic dcpo であれば、この条件は外せる。

証明

m´ を S の upper bound とする。 対象となる半順序集合 P が algebraic dcpo なので、T = {c∈KP | c⊑m´} とおいて、 ∀x∈S. x ⊑ m´ = ⨆^↑T 。 xのコンパクト性より、 ∀x∈S. ∃c_x∈T. x ⊑ c_x 。

C = {c_x | x∈S} とおくと、CはTの有限部分集合なので、Cのupper bound c∈T が存在する。

1. c∈Tなので m´ ⊒ c 。
2. 一方、c は Sの compact upper bound なので、2/3 SFP を適用して、ある m∈M について c ⊒ m 。

よって、m´ ⊒ c ⊒ m 。

λ. 5月は大分へ

5月は大分へ行くことに。

これじゃ、5月はRHG読書会も圏論勉強会もGaucheNightも参加できないか。 残念過ぎる。 が、折角なので九州方面での勉強会等に出たり、九州方面の人にお会いできたら良いなと思う。

それと、とりあえずネットワークがないと死ぬので AIR-EDGE か何かを用意せねば……*1

λ. 久しぶりのSFC

久しぶりにSFCへ。 萩野先生・服部先生・向井先生と会ってきた。

さらに、メディアセンターで図書利用券を作った。 で、早速借りたのが……『量子ファイナンス工学入門』(笑

λ. 第二十八回圏論勉強会

今日は圏論勉強会。

会場はいつもの所ではなく、びぎねっと様のトレーニングルーム。大きいディスプレイがあり、ネットワーク環境もあり、便利だった。感謝。

Wikiにあがっていない話では、「braidは環境(ambient)の次元を上げればsymmetryになる」という話が面白かった。

λ. Advanced Topics in Programming Languages Series: Parametric Polymorphism by Phil Gossett

syd_sydさんのらくがきえんじん(2007-04-24)で紹介されていたので観た。Girard-Reynolds Isomorphism と Djinn の簡単な紹介。

Djinn は Reynolds embedding : F2→P2 に基づいている?　扱われている例は単純な命題論理の範囲を超えてないので、普通に直観主義命題論理の決定手続きを応用すれば良いんじゃないかとも思ってしまう。

関連

• Wadler's Blog: Google Tech Talk: Parametric Polymorphism

λ. Messenger が落ちる

最近、Windows Live Messenger が頻繁に落ちる。 メインウィンドウで表示されているFlashが原因のようで、Flashプラグインの内部で落ちているようだが……困った。

• Flash Player が原因で発生した問題

λ. 野球を観てきた

両親と野球を見に行った。 中日対横浜。 野球を球場に見に行くのは、多分初めて。

λ. 古典と現在 #2 ソポクレース『アンティゴネー』を読む（1）

を観た。