日々の流転

λ. 真夜中は別の顔

テレビ欄で気になったので見てみると、やっぱりシドニィ・シェルダン原作か。

λ. Pyrex - a Language for Writing Python Extension Modules

わりと面白いアプローチだと思う。だれかRubyで似たようなのを作らないかな。

Lambda the Ultimate より。

λ. だるい。何やってるんだろ、俺。

λ. 東方妖々夢

久しぶりに遊ぶ。また少し演出が派手になってるし、会話時のグラフィクスも新しくなってる。それから新しい「森羅結界」のシステム面白い。

λ. 萩野服部研

他に特にやりたいようなテーマもないので、今期はBonoboでもいじってみる予定。Gnomeでも邪道編みたいな事出来るようになったら楽しそうだし。

λ. 読書

『バツイチ30ans 2』

小池田 マヤ [著]

λ. "Typing Haskell in Haskell", Mark P. Jones

ふむ。

λ. 鎌倉市議選

今日まで全然候補をチェックしてなかったので、とりあえず選挙公報に数値目標つきの公約を挙げてた人に投票。4年後に目標が達成されているかを確かめるために、後でここに現状と公約をメモしておこう。

λ. C304 裏切りの村 エピローグ

うわーん。負けたー。まあ、これは仕方が無かったかなぁ。

[2005-06-05 追記] 諦めてしまっては成長がないので、敗因をいくつか考えてみる。

• 狂人を吊るべきか否か、そしてランダム勝負をどう考えるかについて理論武装が出来ていなかった。そのために狂人or真占い師のアルビン吊りを回避出来なかった。
  • エピローグでランダム勝負になった村を教えてもらったので、まずそれを読もう。本国587村と本国207村。
• アルビンをそこまで疑っていたわけではなかったが、一度アルビン狂人よりの意見を書いたら、それにひきづられてアルビン狂人と思い込みだしてしまったこと。
• ディーターが突然死することを心のどこかで期待してしまっていたこと。

λ. 確率論について

C304 裏切りの村 のエピローグでの発言を元に、自分の確率論に関する考えを書いておこうと思う。

「人狼BBSは推理と説得のゲームではあって、確率計算のゲームじゃない」と言われることもあるけれど、私は「推理と説得のゲームではあるけど、それだけのゲームじゃない」と思っている。

例えば、ローラー作戦(COした能力者を全部吊る作戦)なんてのも典型的な例だと思うのだけど、こっちが真能力者だという推理はしていても、そうでないリスクというのが無視できないから、念のために両方吊っておくわけだ。そこには「リスクの評価」という、「推理」と「説得」以外の行動が存在している。

そして、確率論と言うのはリスクを評価するための一つの強力な道具なのである。確率が強力なのは、数値とその演算に明確な意味が定義されているからで、それゆえリスクを定量的に評価するにはとても向いてる。

もちろん、私や他のプレイヤーが使っている確率モデルってのは非常に粗っぽいモデルで、現実からは大きな隔たりがある。だから、当然現実には計算した数値通りの結果になるとは限らない。だけど、現実からの隔たりがある程度あったとしても、確率論の「明確な意味」と「定量的評価」という強力さは変らない。だから、それでも現実のリスクを評価するための一種の「尺度」としては十分使えるのである。

(続く)

λ. Haskell on a Shared-Memory Multiprocessor. Tim Harris, Simon Marlow, Simon Peyton Jones

• <URL:http://research.microsoft.com/~simonpj/papers/parallel/>
• <URL:http://jp.citeulike.org/article/342280>

をざっと読んだ。

まず復習(以下ではSTGマシンの知識は仮定)。これまでのGHCのネイティブスレッドへの対応はジャイアントロックを使った対応だった。つまり、外部のコードとかは複数のネイティブスレッドで同時に実行できるけど、同時にHaskellコードを実行するネイティブスレッドはただ一つだけだった*1。これだとSMPでもあまり嬉しくないので、より細粒度のロックにして並列度を上げたい。ただ、各サンクにロックを用意して操作毎にロックすることにすると、無茶苦茶オーバーヘッドがかかる。

で、「どうすんだろな〜」と思ってたんだが、この論文では、割と楽観的な前提に基づいて「そもそもサンクに対して厳密な排他制御は不要」と言っている。私がこの分野についてあまり知らないからかもしれないが、コロンブスの卵みたいで随分感心した。

まず、サンクを評価結果(へのindirection)で上書きする際にポインタを書き込む領域を別に用意することで、サンク上の他のデータが評価結果の書き込みで壊れないようにする。これで複数のスレッドが同時に同一のサンクを実行しても問題なくなる。ただ、複数のスレッドが同時に同じサンクを実行すると、計算を重複して行うことになってしまう。副作用のある計算は複数回実行するとまずいので真面目に排他制御するが、大多数の純粋な計算は何度実行しようと意味論的には問題ない。

もちろん、意味論的に問題なくても計算量的には問題になる。そこで各スレッドは定期的な lazy black-holing のタイミングでサンクを排他的に所有しようとし、それによって重複する計算を検出する。で、検出された重複する計算は捨てる。この処理にはサンクに対する排他制御が必要になるが、lazy black-holing の頻度は通常のサンク操作の頻度よりもずっと低いため、各操作毎に排他制御するよりもオーバーヘッドはずっと低い。また、すぐに計算が終了するようなサンクは排他制御無しで実行できる*2し、計算に時間がかかるようなサンクの場合も無駄な計算は一定時間で破棄できることが保証される。

あとは、複数のスレッドが同時に同じサンクを実行する可能性を極力下げれば良い。そのために、サンクに制御を移す時点での eager black-holing (ここでは grey-holing と呼んでいる) も提案している。これも排他制御無しで行え、これによって複数のスレッドが同時に同じサンクを実行してしまう可能性を限りなく小さく出来る。ただ、このタイミングでのサンクへの書き込みは通常のアクセスパターンから外れているので、キャッシュのスラッシング(cache-thrashing)を引き起こす可能性もあり、これによって逆に性能が低下することも有り得る。

とかとか。

他にもいろんなテクニックを使ってるけど、特に面白かった部分は以上の話。

λ. google:アルキメデスの卵

ふと検索してみたら、2件ひっかかった。

λ. 特急あずさって

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

λ. 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が使えるようになれば良いのに、と思った。 色々難しそうだが。例えば、この路線の場合、ほとんどの利用者は有人の駅と無人の駅の間の移動だろうけど、モノレールの場合には無人駅の間の移動も結構ありそうだし。

λ. “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 がなかったのでパスのデータ型が定義できなかった。

λ. お菓子買いだめ

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

λ. インド料理屋

λ. Functional Programming Meeting 2010

昨日紹介した、Oleg さんや 單中杰（Chung-chieh Shan）さんを交えての会合に参加。