トップ «前の日記(2007-05-08) 最新 次の日記(2007-05-10)» 月表示 編集

日々の流転


2007-05-09 [長年日記]

λ. 大分三日目

10:00〜20:30の勤務は結構長い。 労働っぽい事はまだ何もしていないが、疲れた。 明日・明後日は休みなのでゆっくりしたい。

昨日、Air-Edgeだと Google Maps が結構重いと書いたが、これはFirefoxの場合でIEだと平気だった。Firefoxだとラスタ画像を使うのに対して、IEだとベクトル画像(VML?)を使ってるのか。

shelarcyさんの「Haskellで学ぶ並列プログラミング(その1)」とsoutaroさんの「それPraggerでできるよ! - Ruby版Plagger登場」を読んだ。

そういえば、浮世ではGaucheNight第7回仮想化実装技術勉強会が行われている頃か。羨ましいものだ。

アイぶんぶん広場

λ. Chapter 9 の練習問題2

D を spectral locale とすると、

  1. Dのスコット開フィルタはKΩDのフィルタに対応し、
  2. Dの点はKΩDの素フィルタに対応する。

証明

P = KΩD とおくと ΩD=Idl(P) となるので、練習問題1 の対応を利用する。

Idl(P)のスコット開集合Fと、Pのupper-closedな部分集合Gが対応しているとする。 1を示すためには、FがフィルタであることとGがフィルタであることが同値であることを示せばよい。

  • Fがフィルタだとする。 T⊆Gが有限集合ならば S={↓y | y∈T}⊆F も有限集合であり、Fはフィルタなので ⋀S∈F 。↓⋀T=⋀S∈F=ψ(G) より ∃x∈G. ↓x≦↓⋀T で ∃x∈G. x≦⋀T 。Gはupper-closedなので ⋀T∈G 。よってGはフィルタ。
  • Gがフィルタだとする。 S⊆Fが有限集合ならば、T={c | ↓c∈S}⊆G も有限集合であり、Gはフィルタなので ⋀T∈G 。⋀T∈G=φ(F) より ↓⋀T∈F で、 ↓⋀T=⋀Sなので ⋀S∈F 。よってFはフィルタ。

2を示すのは簡単。 pt D ≅ Frames(Idl(P), 2) ≅ DistributiveLattices(P, |2|) なので、分配束の準同型射 P→2 について考えればよい。

  • 分配束の準同型射 f: P→2 の true-kernel F={x∈P | f(x)=true} が素フィルタに対応することを示す。束の準同型であることから、有限集合 S⊆P について f(⋁S)=⋁{f(x) | x∈S} 。各x∈Sについてf(x)=falseであれば、f(⋁S)=falseなので、Fは素。
  • 逆に素フィルタFが与えられたとき、f(x) = if x∈F then true else false が分配束の準同型になっていることを示す。S⊆Pを有限集合として:
    • Fは素フィルタなので f(⋁S)=true ならば ∃x∈S. f(x)=true 。
    • フィルタはupper-closedなので、∃x∈S. f(x)=true ならば f(⋁S)=true 。
    • フィルタはfinite-meetについて閉じているので、∀x∈S. f(x)=true ならば f(⋀S)=true
    • フィルタはupper-closedなので、f(⋀S)=true ならば ∀x∈S. f(x)=true
本日のツッコミ(全2件) [ツッコミを入れる]
ψ takot (2007-06-10 13:51)

VMLが使える環境だとVMLを送ってきて,使えない環境だと画像を送ってくるようにフォールバックするんだっけな.<br>3年か4年前の木曜研究会で見たような覚えが(^^;

ψ さかい (2007-06-14 00:25)

そういえば、そんな話を聞いたことがあるような (汗<br># 3,4年前だと初代SeMapだったのかな……懐かしい。