Conway不動点のμ表現

1. 不動点：f^† = <f^†, A>;f -- μx.f(x, a) = f(μx.f(x, a), a)
2. 自然性：[(g×X);f]^† = g;f^† -- μx.(f(x, g(b)) = (μx.f(x, a))[g(b)/a]
3. 対角自然性：(f;g)^† = [(A×g);f]^† -- μx.g(f(x, a)) = μt.f(g(t), a)
4. 対角性（ダブルダガー）：(f^†)^† = [(A×Δ);f]^† -- μx.(μx'.f(x', x, a)) = μx.f(x, x, a)

μで書くと、また違った味わい。

ちなみに、Conwayのdouble iteration identities, composition identitiesは、t = t(x, y, z1, ...), s = s(x, z1, ...), r=r(x, z1, ...) として、

1. μx.(μy.t) = μz.(t[z/x, z/y]) （ダブルダガー）
2. μx.(s[r/x]) = s[μx.(r[s/x])/x] （対角自然＋不動点性）

（http://citeseer.ist.psu.edu/bloom00iteration.htmlより。）

普通の自然性はどうなっているんだ？

それはそうと、λ記法やμ記法を使うと簡単になるのかな？ 圏論にあわせると、なんだか風変わりなラムダになってしまう気もする。Katyだって、まーラムダみたいなもんだしな。