トップ «前の日記(2004-07-27) 最新 次の日記(2004-07-29)» 月表示 編集

日々の流転


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 といった概念を導入して証明してる。なかなか面白かった。

Tags: 論文 圏論