Recursive types
F : C → C, F(FixF) iso Fix
- the initial algebra gives us a canonical object #think algebra → negative?
Let F: C * C → C (bifunctor). seek a canonical object FixF such that F(FixF, FixF) = FixF any candidate?
Suppose F(X,_) : C -> C exists for all X: C
this induce a functor: F*: C -> C sending X to Fix F(X,_):
F*(X) = F(X,F*(X))
candidate:F(FixF*, FixF*) = F(FixF*,F*(FixF*)) = F*(FixF*) = FixF*
⇒ we can obtain a canonic solution (and an induction principle)
We have a general solution to build muL for arbitrary logic L