最小不動点定理
たぶんあまり一般的な名称ではないmrsekut.icon
/mrsekut-book-4320026578/088の中で使われていた
cpo上のスコット連続関数$ fは最小不動点を持つ、という定理のことをこう呼んでいる
定理
$ Dをcpo
$ fを連続関数$ D\to D
とする
ある$ a\in Dが存在して、以下の2つを満たす
$ f(a) =a
$ f(b)=bならば、$ a\sqsubseteq b
↑これは、$ aという最小不動点を持つということを言っているmrsekut.icon
$ bは、最小不動点ではない不動点のこと
常にあるとは限らない
この最小不動点$ aは以下のように表せる
$ a = \sqcup\{f^n(\bot)\;|\;n\in\mathbb{N}\}
f^nは関数fのn回適用したもの
証明
/mrsekut-book-4320026578/088
かんたんmrsekut.icon
最小不動点定理をfactを用いて確認する
参考
/mrsekut-book-4320026578/088