2004-07-28 [長年日記]
λ. FREYD, P. J. 1990. Recursive Types Reduced to Inductive Types. In Proceedings 5th IEEE Annual Symp. on Logic in Computer Science, LICS'90 (Philadelphia, PA, USA, 4-7 June 1990). IEEE Computer Society Press, Los Alamitos, CA, 498-507.
7月3日に言及した論文だけど、某先生が持っていたのでスキャンして貰うことが出来た。ラッキー。
ここでいう Recursive Types はパラメータが正負両方の位置に現れるようなオペレータの(最小)不動点、Inductive Types は正の位置にしかパラメータが現れないようなオペレータの不動点。ある条件を満たす圏(CPO-Category)では、Recursive Types は Inductive Types に還元できる。このことを T-dialgebra, T-invariant object といった概念を導入して証明してる。なかなか面白かった。
[ツッコミを入れる]
