克萊尼不動點定理

在數學中，序理論的克萊尼不動點定理（英語：Kleene fixed-point theorem）指出給定任何完全格 L 和任何具有斯科特連續性的函數

$f:L\to L,$

$f$的最小不動點$fix(f)$存在，如果我們用$\bot$來表示L內的最小元素，那麼$fix(f)=\bigsqcup _{i\geq 0}f^{i}(\bot )$

證明

我們首先定義集合$M=\{\bot ,f(\bot ),f^{2}(\bot ),\ldots \}$，為了方便表示，我們用$m$來表示集合$M$中最大的元素，即$m=\bigsqcup M$。我們想要證明$m$為函數$f$的最小不動點。

首先我們證明$m$為函數$f$的不動點。因為函數$f$是斯科特連續的，所以我們有$f(m)=f(\sqcup M)=\sqcup (f(M)\cup \bot )=\bigsqcup M=m$。

接下來我們證明$m$為函數$f$的最小不動點。假設函數$f$存在另外一個不動點$x$，因為$\bot \sqsubseteq x$, 且函數$f$為單調函數（由於斯科特連續性），所以$f(\bot )\sqsubseteq f(x)=x$。假設$m=f^{k}(\bot ),k\in \mathbb {N}$， 根據數學歸納法，$f^{k}(\bot )\sqsubseteq f^{k}(x)=x$。 即$m$為函數$f$的最小不動點。

參見

• 克納斯特-塔斯基定理
• 其他不動點定理