查看“︁克莱尼不动点定理”︁的源代码

{{unreferenced|time=2010-1-1}}

在[[数学]]中，[[序理论]]的'''克萊尼不動點定理'''（{{lang-en|Kleene fixed-point theorem}}）指出给定任何[[完全格]] ''L'' 和任何具有[[Scott连续性|斯科特连续性]]的[[函数]] 

:<math>f: L \to L,</math>

<math>f</math>的[[最小不动点]]<math>fix(f)</math>存在，如果我们用<math>\bot</math>来表示''L''内的最小元素，那么<math>fix(f) = \bigsqcup_{i \geq 0}f^{i}(\bot)</math>

== 证明 ==

我们首先定义集合<math>M = \{\bot, f(\bot), f^{2}(\bot), \ldots\}</math>，为了方便表示，我们用<math>m</math>来表示集合<math>M</math>中最大的元素，即<math>m = \bigsqcup M</math>。我们想要证明<math>m</math>为函数<math>f</math>的最小不动点。

首先我们证明<math>m</math>为函数<math>f</math>的不动点。因为函数<math>f</math>是斯科特连续的，所以我们有<math>f(m) = f(\sqcup M) = \sqcup(f(M) \cup \bot) = \bigsqcup M = m</math>。

接下来我们证明<math>m</math>为函数<math>f</math>的最小不动点。假设函数<math>f</math>存在另外一个不动点<math>x</math>，因为<math>\bot \sqsubseteq x</math>, 且函数<math>f</math>为单调函数（由于斯科特连续性），所以<math>f(\bot) \sqsubseteq f(x) = x</math>。假设<math>m = f^{k}(\bot), k \in \mathbb{N}</math>， 根据数学归纳法，<math>f^{k}(\bot) \sqsubseteq f^{k}(x) = x</math>。 即<math>m</math>为函数<math>f</math>的最小不动点。

== 参见 ==
*[[克纳斯特-塔斯基定理]]
* 其他[[不动点定理]]
{{math-stub}}

[[Category:不动点|K]]
[[Category:数学定理|K]]