Kleene fixed-point theorem
準備
$ Xと$ X'をdcpo（cf. 束) とする。関数$ f:X\to X'がスコット連続 (Scott-continuous; または単に連続) であるとは、任意の有向部分集合$ C\subseteq Xについて、$ \{f(x)\mid x\in C\}に上限が存在し、$ f(\vee C)=\bigvee\left\{f(x)\mid x\in C\right\}が成り立つことを言う。 $ fが連続のとき$ fは単調。
主張
$ Xを最小元$ \botを持つdcpoとする。$ X上の連続関数$ f: X\to Xは最小不動点$ \mu fを持ち、$ \mu f=\bigvee\{f^n(\bot)\mid n\in\mathbb N\}。
証明
プログラム意味論（横内）定理3.3.1
その他
条件を弱めて、$ fが単調であれば$ fの最小不動点の存在が構成的に示せる。
最大不動点の存在も同様に示す
プログラム意味論（横内）命題3.4.11
プログラム意味論（横内）定理6.3.5
他の定義