トップ «前の日記(2005-02-28) 最新 次の日記(2005-03-04)» 月表示 編集

日々の流転


2005-03-03 [長年日記]

λ. Representations of First order function types as terminal coalgebras, Thorsten Altenkirch

たまたま見かけて読んだのだけど、面白かった。α→βという関数型は、αが帰納的(inductive)な型であれば、余帰納的(coinductive)な型として表現できるという話。自然数やリストの場合までは考えたことがあったが、2分木のような線形でない型の場合も nested datatypes を使えば表現出来るというのは気づかなかったなぁ。

例:
自然数
(μX.1+X)→B ≅ νX.B×X
Aのリスト
(μX.1+A×X)→B ≅ νX.B×(A→X)
Aの2分木
(μX.A+X×X)→B ≅ (νF.ΛX.(A→X)×F(F(X)))(B)

証明は、ちょっと良く理解出来ていない所もある。セッティングは bicartesian で ωop-limit と ω-colimit が存在する圏(cartesian-closedである必要はない)。そのままでは構成的関数からなる ω-Set のような圏へ一般化することは出来ないらしい……

関連エントリ
Tags: 論文 圏論