2006-06-24 [長年日記]
λ. Functional pearl: i am not a number -- i am a free variable. Conor McBride, James McKinna
を読んだ。 しかし、変数とか束縛ってのは毎度悩ましいものだね。
λ. Re: 推移的崩壊とAFA
<URL:http://evariste.jp/kagami/diary/0000/200606.html#20060624-1>
かがみさん、はじめまして。集合論雑記は以前から時々読んでいました(^^ 集合論をきちんと勉強していないものにとっては非常にありがたかったです。今回も詳しい説明ありがとうございます。おかげで、推移的崩壊と Mostowski's collapsing lemma についてはだいぶよく理解できました。
で、AFAについてですが…… 等号の検証はそういう形で書くと難しそうに見えるかもしれませんが、実際にはそれほど難しく感じたことはないです。coinduction proof principle では x = y を証明するために xRy が成り立つような bisimulation R が存在することを証明しますが、coinductipn proof principle はある意味 ∈-induction の双対みたいなものなので、こっちだけがそんなに難しいことはないとも思いますし。
また、decoration や AFA はたとえ正則性の公理や推移的崩壊の概念がなくとも、余代数方面のアイディアから生まれたのではないか、と個人的には思っています。というのも、集合全体を余帰納的に定めようとすると、つまり集合全体のクラスが冪集合関手(をクラスに拡張したもの)の終余代数(final coalgebra)になるようにしようとすると、結局 decoration や AFA のような概念は自然に出てきそうな気がするので。
……最初にも書いたように集合論についてはまったくの素人なので、変なことを書いていたら済みません。
追記 (2006-06-26)
<URL:http://evariste.jp/kagami/diary/0000/200606.html#20060624-1>
coalgebra等の簡単な解説は近いうちに書こうと思いますが、別に圏論の深い理解が必要とかそんなことはなくて、結構簡単な話です。とりあえず、coalgebraとcoinductionのチュートリアルとしては、B. Jacobs と J. Rutten の A Tutorial on (Co)Algebras and (Co)Induction. (<URL:http://www.cs.ru.nl/~bart/PAPERS/index.html>) あたりになるのかなぁ……
それから、私もくるるさんに集合論の中で推移的崩壊がどう使われるかを教えてもらえるのを楽しみにしています :-)
