日々の流転

λ. 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 のような圏へ一般化することは出来ないらしい……

関連エントリ

• [agda] ストリームの表現