日々の流転

λ. たまてばこ

またtama.rbが暴走していたらしく、ITCの人に怒られてしまった。ソースを見ても原因は発見できなかったので、とりあえず一定時間内に終わらなかったらexitするようにしておく。

Thread.new{
  sleep(60 * 5)
  exit
}

λ. ruby-gnome

gnome-vfs に手をつけてみたけど、退屈で面倒なので、放置モードに入る。

いい機会なので SWIG/Ruby を使ってみよっかな。

λ. 雨が上がる。読書を中断して晴れ上がった空を見上げると、どこからか蝉の鳴き声が聴こえてくる。じめじめして重苦しかっただけの空気も、いつのまにか照り返すような熱気を伝えてくる。もう梅雨はあけたのだったろうか

λ. (use-syntax (ice-9 syncase))

Guile でdefine-syntaxとかを使うには (use-syntax (ice-9 syncase)) としておかなくてはいけないのか。知らずにちょっとはまった。

λ. どせいさんフォント

メモ。

λ. 今日から一応夏休みか。

λ. Haskellマラソン

.

λ. お昼

純広東家庭料理「嘉賔(KAHIN)」。

λ. Haskellの代数的データ型は始代数ではない

Haskellマラソンで「Haskell の普通の代数的データ型は始代数(initial algebra)になっていないと話したが、例がちょっと間違っていたので、とりあえずここに書き直しておく。

たとえば、「data N = Z | S N」という代数的データ型と、以下のようなダイアグラムを考える。

    Z        S
1 ──→ N ──→ N
│       │       │
│       │       │
│       ↓       ↓
└──→ N ──→ N
    Z        id

これを可換にするような N→N は複数存在し、ユニークには決まらない。例えば以下のh,h'は共にこのダイアグラムを可換にするが、hが正格であるのに対してh'は非正格なので等しくない。

h, h' :: N -> N
 
h Z     = Z
h (S x) = id (h x)
 
h' _ = Z

λ. Haskellの代数的データ型は始代数ではない? (2)

2005-02-25に追記。上記の議論は正しくなかった。代数的データ型の領域を構成するときに使う separated sum A+B は圏論の意味での直和(coproduct)ではないので、h'が上記のダイアグラムを可換にすることからは、下記のダイアグラムを可換にすることは言えない。実際 h' ([Z,S] ⊥) = h' ⊥ = Z は [Z,id] ((1+h') ⊥) = [Z,id] ⊥ = ⊥ と等しくない。したがって、これは反例になっていない。

        [Z,S]
   1+N ───→ N
    │          │
1+h'│          │h'
    ↓          ↓
   1+N ───→ N
        [Z,id]

λ. Haskellの代数的データ型は始代数ではない? (3)

2005-02-26 に追記。横山さんの日記で言及されたのをきっかけに色々と考えてみたのだけど、考えていてだんだん分からなくなってきた。とりあえず、自分が理解していることだけを簡単に書いておこうと思う。

pointed CPOと任意の連続関数からなる圏では、関手F*1の終余代数のinverseは弱始代数(weak initial algebra)ではあるけれど、本物の始代数になっていないことがある。ただし、正格な連続関数だけに制限した部分圏の始代数にはなっている。

簡単な具体例としては恒等関手や(圏論の意味での)直積の場合がある。恒等関手については、対応する型構築子とその不動点となるデータ型をHaskellで実際に定義することが出来る(e.g. newtype I x = I x; type T = Fix I)。一方、(圏論の意味での)直積はCPOとしては存在してもHaskellで定義することは出来ない*2。

それにしても大げさなタイトルをつけてしまったもんだ。例は間違ってるし、タイトルは大げさすぎるしで、恥ずかしいなあ、もう。

λ. Haskellの代数的データ型は始代数ではない? (4)

2005-02-28 追記。もう少しすっきり理解できた。

定理1 (Recursive Types Reduced to Inductive Typesより)

(X,φ) が正格な連続関数だけに制限した部分圏の始代数 ⇔ (X,φ^-1) が終余代数。

定理2 (自分で証明)

任意の A, B, f:A→B について Ff: FA→FB が正格とする。
このとき、(X,φ) が始代数 ⇔ (X,φ^-1) が終余代数。

でも、これじゃ定理2よりHaskellのほとんどのデータ型は始代数と考えて問題なくなっちゃうじゃないか。う〜ん、残念(ぉぃ。

λ. 軍医としての森鷗外

なんとはなしにWikipediaを眺めていて、「森鴎外」の項に以下のような記述をみつけ、「へぇ」と思った。笑い事ではないのだけど、もし中学生や高校生のころにこういったエピソードを知っていれば、単なるブンガクシャとしてではなく、その時代に生きた人間として興味を持つことが出来ただろうな、と思った。

脚気の伝染病説を主張し、のちに海軍軍医総監になる高木兼寛と対立した。あくまで自説に固執し日露戦争でも兵食に麦飯を給するのを拒んだ（自ら短編『妄想』で触れている）ため、陸軍が25万人もの脚気患者を出し、3万名近い兵士の命を犠牲にしたことに責任があるとされる（同時期、高木の指示で兵に麦飯を与えていた海軍では脚気患者は軽症者がわずかに発生したのみで、死者は無しと伝えられる）。「ロシアのどの将軍よりも多くの日本兵を殺した者」との批判すらある。

λ. 4日で学ぶモデル検査: 3日目

LTLについては既に知っているので、軽く読み、問題を解いた。 特に詰まる点は無し。昨日の練習問題は結構やりがいがあったのでちょっと拍子抜け。

λ. 研究会最終発表会など

研究室のadmin会議が朝あり、その後に研究会の最終発表会を聴いた。それから八田で打ち上げ。

λ. ezmlm-idxでメールヘッダにシーケンスナンバーをつける

headerraddファイルに「X-Sequence: <#n#>」という一行を追加すれば良い。

λ. 依存型とcatamorphism

Agda2ことはじめ - ラシウラ の記述を読んで、そういえば依存型を用いた除去規則って、(弱)始代数の普遍性とはどう関係するんだろうか、と思ったので、category with attributes で考えてみた……んだけど、書いてたら混乱してきたので、何回かに分けて書くことにする。

1. Categories with attributes (cwa)
2. cwaでのユニット型の解釈

λ. CLTT の 1.3 Some general examples のノート

CLTT読書会で読んでいる Categorical Logic and Type Theory の、1.3 Some general examples を復習して、練習問題も一通り解いた。

• ノート