Inductive type
Fixed point, 不動点
関数 について、fixed pointとは、
を満たす のこと。これをendofunctorに拡張する。
Endofunctor について、 fixed pointとは、
を満たす のこと。
Initial algebra
のinitial objectのこと。
Lambek's theorem
- initial algebraはfixed point
証明は簡単。
Inductive type
Initial algebraはleast fixed pointと考えられる。 これでinductive typeを定義できる。たとえば、
から、 を次のように定義できる。
Initial algebraの存在の証明は手間がかかる(模様)。
Catamorphism
Initial algebraのmediating morphismのこと。
参考文献
*1:mediating morphismの取り出し