Coherence Space

まだ、Proofs and Types 読んでます。89年の本だから、もう古典なんだよな。何回か読んだけど、Coherence Space の所で挫折してた。今なら理由はわかる。

　　ちゃんと計算しろ

ってことね。証明を追っただけでは足りなくて、実際に集合を作ってみないと。Coherence Space は有限近似、つまり、有限集合だけで話が済むので、実は楽勝でした。 Φ(空集合)が未定義データを表していて、値が決まっていくと、それを∪で足していく感じですね(directed union)。これが、なんでわからなかったのか今では不思議。

もっとも、Stable Function の所で、pull back と filtered limit が保存するとか圏論の言葉で書かれているがするするわかるのは圏論復習したからだな。 Coherence Space を limit のある圏の自己関手として定義して、Stable Function を自然変換と考えれば Agda に載せられると思ったけど、できるかどうかは。

while program とか fixed point semantics とかの方がわかりやすかったんだけど、あれも、やっぱり問題解いていたからだろうな〜　

というわけで、今回は Sysetm F まで読めるようです。しかし、この手の理論は役には立たないのだが。もっとも、System F は Java のGeneric のような型変数の理論だから、珍しく役に立った方ですね。