2006-08-27 [長年日記]
λ. CPOと始代数
sumiiさんのエントリ「Haskellの「代数的」データ型は代数的か？」や、直接お聞きした話によると、関数型言語畑でこの辺りのことについて直接考えて(いる|いた)人というのは非常に少なそうな気がする。
ちょっと調べたところでは、M.M. Fokkinga and E. Meijer. Program calculation properties of continuous algebras. には、CPOでは始代数になっていない場合があるということが書いてあって、以降の論文ではこれを念頭に「CPO⊥で始代数」といった書き方をしているように思える。この論文で参照されている論文のうち以下の論文も後でチェックした方が良さそうかな?
- J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright. Initial algebra semantics and continuous algebras. Journal of the ACM, 24(1):68-95, January 1977. <URL:http://portal.acm.org/citation.cfm?id=321997>
- J.C. Reynolds. Semantics of the domain of flow diagrams. Journal of the ACM, 24(3):484-503, July 1977. <URL:http://portal.acm.org/citation.cfm?id=322028>
それから、私が20040731#p07の定理2で書いた「Ffが常に正格なら、CPOでもFの始代数と終余代数が一致する」という話なんかも、「証明は簡単だし、どうせ知ってる人は知ってるだろ」と思ってたんだけど、ちょっと探してみた限りでは似たようなことをしている人はいなかった。どうせなので、証明を晒してみる。
λ. 富士総合火力演習
毎年終わってから気づく。一度行ってみたいものだ。
[ツッコミを入れる]
