たぶんあまり一般的な名称ではない

/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という最小不動点を持つということを言っている

bは、最小不動点ではない不動点のこと

常にあるとは限らない

この最小不動点aは以下のように表せる

a = \sqcup\{f^n(\bot)\;|\;n\in\mathbb{N}\}

証明

かんたん

参考