日々の流転

λ. Regular Expressions into Finite Automata

天泣記(2002-04-16)を見て、Regular Expressions into Finite Automata を眺めてみる。

λ. 人間と法

休講。寝坊したので急いで行ったのに……

λ. 自然言語論

日本語の文法では、形容動詞を認める学派と、形式名詞+断定の助動詞に過ぎないとする二つの学派があるらしい。

共起制限を含まない形態素解析はわりと単純だ。

λ. 線形の理論

線形の理論のSAも引き受けることに。相方の和田さんはとても行動力のある人で、才色兼備って感じ。履修者が70人以上いて「多いなぁ」と感じた。

λ. 向井研

証明図はλ項と見れるらしい。やはりカリー・ハワードの対応は重要そうだ。

可能世界はモーダリティを扱うグラフ。可能世界はそもそもは様相論理を扱うために考えられたが、現在では主従が逆転してる感じらしい。

チャネル理論のClassificationは情報射を射とする圏をなすようだ。

そういえば、来週は僕も発表する番なので、これから資料とかを用意しなくちゃ…

λ. 多相型とλ計算とHaskell

多相型とλ計算とHaskellについて石原君に簡単に説明してみる。λ計算とHaskellはともかくとして、多相型についてはうまく説明できなかった。言いたかったのは、要は「値をパラメタライズしたのが関数で、型をパラメタライズしたのが多相型」って事だったんだけどね。

λ. ごはん

倉吉というお好み焼き屋さん。

λ. 『天使な小生意気 13』, 西森博之

を読んだ。

λ. GNOME 2.2.1 patches available for test

む、先をこされちまったい。実はこれを見る少し前に、ようやくNautilusのクラッシュの原因を発見して、動作させることに成功したのに……。(ちなみに、CyGNOMEのパッチを見るとその部分は単に無効化されていた)

λ. 買った本

『公共経済学の理論と実際』

中村 慎助, グレーヴァ 香子, 小沢 太郎 [編集]

『社会保障論』

-

λ. CMS班ミーティング

テーマ決め。なんかchikoさんに丸め込まれたような気がするが (・∀・)キニシナイ!!

λ. 『ラバーズ 1』, 犬上 すくね

を読んだ。

λ. 『銭　壱巻』, 鈴木 みそ

を読んだ。

生命の価値の評価といえば、ホフマン方式やライプニッツ方式はプロジェクト評価論でやったなぁ。ホフマン方式もライプニッツ方式も遺失所得をベースとした方法。遺失所得以外の方法もあるけれど、実務で使われることはないのかな。

λ. jhc

jhc is a haskell compiler which aims to produce the most efficient programs possible via whole program analysis and other optimizations.

[Haskell] ANNOUNCE: The jhc Haskell compiler. より。色々と興味深い。

プログラム全体を見た解析による最適化ってのは、局所的な解析による最適化と比べてチョー強力なんだけど、分割コンパイルなんかとの相性の悪さもあって、実用的なコンパイラで使われることは無かったように思う。それを打ち破る何かがあったのだろうか?

λ. 不動産市場分析 (2) — ストック・フロー・アプローチ

4象限モデル(The Dipasquale-Wheaton 4-Quadrant Diagram?)が面白かった。

λ. ICPC過去問: Hanafuda Shuffle

Haskellで瞬殺(HanafudaShuffle.hs)。ICPCじゃ実際にはHaskell使えないので、一応Cでも解いておいた。

λ. 『博士の愛した数式』, 小川 洋子 [原作], くりた 陸 [漫画]

まだ、小説も読んでないし、映画も観ていないのだけど、漫画にもなってたのか。素敵な話ではあると思ったけど、数学とか数学者へのイメージはあまりピンとこなかった。

Quotation

p.66 より。

さあ、どう思う？

みんなバラバラ
あ、それに2だけ偶数だね

その通り
素数の中で偶数は一個だけだ

さびしくないのかな

心配にはおよばない
さびしくなったら、偶数の世界に行けばいいんだ

λ. 人狼のなく頃に 第459話　『強い妖戦士編』

• ログ
• 第459話　『強い妖戦士編』 - ひぐらし人狼まとめサイト

鬼側すごいな。 きっかけこそ偶然だったが、その後の作戦は見事。 「これぞ、スーパーステルス(SS)」という感じで、鮮やかだった。

λ. システム・ソフトウェア #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

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

λ. "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 であることに矛盾。

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

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

λ. EMチャージに乗り換えることにした

AirEdgeをずっと使ってたけど、emobileのEMチャージに乗り換えることにした。 とりあえず、アウトレットでD11LCというのを注文。9980円で5000円分の通信料込み。

佐野さんにEMチャージを教えてもらってからずいぶん経ってしまったが、iPhoneを買ったのと、Willcomが「商品代金込980円/月で使える『AX420Nスペシャルモデル』」というのを始めたのをキッカケに決断。 後者については、現在使ってるAX420Nを買い直すというのも考えたのだけど、それもなんかなぁと思ったので。

• 佐野さんによるemチャージの補足