日々の流転

λ. SFCの近くで火事があった。煙がSFCからも見えたのだけど、残念ながらこういうときに限ってデジカメを持っていなかったので、写真を撮ることが出来なかった。

λ. representable functor

representable functor をやった。Hom(X,Y)が集合だと強調されていたのはこのためだったのか。

λ. least general unifier

Prolog の unification が most general unifier で、そのdualとして least general unifier というのがあるそうだ。例によってカテゴリ論で綺麗に扱えるらしい。……と、どっかで聞いた話だと思ったら、least general unifier は帰納論理プログラミングの授業でやったんだった。

【2006-05-15追記】 least general unifier ではなく least general generalisation が正しい。

λ. 買った本

岩波判例基本六法 平成14年版

-

自然言語処理

石崎俊[著]

Software Design 2002年5月号

-

Linux Magazine 2002年6月号

-

λ. 夕食

katapon(と書いてみるテスト)とサイゼリア。エビとキノコのグラタン、他。

λ. WWW2005 前日

ボランティアのオリエンテーション、電源とネットワークのセットアップなどの各種の準備。

λ. 『リサイクル幻想』, 武田 邦彦

を読んだ。

なんでもリサイクルすれば環境によいというような安易な発想への批判。そのような発想で何でもリサイクルすると、かえってエネルギーを消費し、環境を破壊することにもなる。リサイクルを考えるには、材料工学を初めとする工学的視点が欠かせない。

リサイクルの過程には分離工学の考え方が適用できる。純度が高くまとまっているものはリサイクルが容易だが、純度が低く分散してるものをリサイクルしようとすると高くつく。

金属はリサイクルに向いているが、鉄に混入した銅を取り除くのは不可能といった問題もある。紙をリサイクルするのに(遺産型の資源である)石油を使うのは循環型社会の観点からは本末転倒。プラスチックは素材としては比較的劣化しやすいが、燃やすと石油とほぼ同じ熱量を発生するので、素材として使用した後に燃やして熱量を得るのが良い……

工学的な議論は、ラフな議論ではあるがまあ大体納得がいく。ただ、そこから著者の主張する循環型社会像へは飛躍が過ぎると思った。

参考

• 環境市民　武田邦彦氏著「リサイクルしてはいけない」のおおいなる問題点

λ. RubyKaigi 2006

チケット予約。 一時間かそこらで売り切れたそうなので、間に合って良かった。

λ. 『ビジョメガネ』

みんなメガネ好きだよねー

λ. ディスクトラブル

またもやディスクトラブル。RAID使ってても避けられないトラブルがこう続けてくると、呪われてるんじゃないかという気がしてくる。そして、復旧作業をあまり手伝えずにごめんなさい。

λ. 今日のITシステム

• Matteo Baldoni, Cristina Baroglio, Nicola Henze. Personalization for the Semantic Web. Reasoning Web 2005: 173-212 <URL:http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11526988_5>
• B. Rachlevsky-Reich, I. Ben-Shaul et. al.: GEM: A Global Electronic Market System. In: Information Systems Vol. 24 No. 6, 1999, 495-518 <URL:http://citeseer.ist.psu.edu/rachlevsky-reich99gem.html>
• 自分のやりたいことで、キーとなるテクノロジーは何か?
• 中間発表では、予想される結論は言うべき。

λ. 大分三日目

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

λ. アブ大量発生

アブが大量に発生して、家にも気がついたら20匹くらい侵入してきていた。羽音のする虫は苦手なのでちょー怖かったが、帰ってきた親父が撃退してくれて、親父が頼もしかった。しかし、まだどうも羽音が近くから聞こえるなと思ったら、天井のライトの裏に……

ひぃぃいぃぃいぃぃ