Kleene 不动点定理

形式陈述 ​

设 $(D,⊑,\mathrm{\perp })$ 是 pointed DCPO公理库有向完备偏序Directed-complete partial order · DCPO · Directed complete poset每个非空有向子集都具有上确界的偏序，用于汇聚相容的信息近似。，$F:D\to D$ 是Scott 连续公理库Scott 连续映射Scott-continuous function · Scott continuity保持有向上确界的单调映射，使有限信息逼近与计算相容。自映射。则

$$\mathrm{\perp }⊑F(\mathrm{\perp })⊑F^2(\mathrm{\perp })⊑\cdots$$

是一条递增链，并且

$$\mathrm{lfp}(F)=\underset{n<\omega }{⨆}{F}^n(\mathrm{\perp })$$

是 $F$ 的最小不动点。

证明令 $a=\underset{n}{⨆}{F}^n(\mathrm{\perp })$。Scott 连续性给出

$$F(a)=F(\underset{n}{⨆}{F}^n(\mathrm{\perp }))=\underset{n}{⨆}{F}^{n+1}(\mathrm{\perp })=a,$$

最后一个等号来自删除链首项 $\mathrm{\perp }$ 不改变上确界。若 $x$ 是任意前不动点 $F(x)⊑x$，由 $\mathrm{\perp }⊑x$ 和归纳公理库数学归纳法Mathematical induction · Weak induction由基例和从 n 到 n+1 的归纳步推出性质对全部自然数成立。可得 $F^n(\mathrm{\perp })⊑x$，故 $a⊑x$。特别地，它小于每个不动点。

只要求 $\omega$-CPO 与保持递增 $\omega$-链上确界的 $\omega$-连续性，也足以推出该公式；使用一般 DCPO/Scott 连续是更统一的版本。

直觉 ​

从完全未知的 $\mathrm{\perp }$ 开始，每次应用 $F$ 多展开一层递归。第 $n$ 项只含有限深度内可以证明的行为，链的上确界汇总所有有限证据。最小性意味着不凭空加入任何递归方程没有由有限展开强迫的结果。

“最小”相对于信息序，而不是数值大小。一个函数在更多输入上终止，通常在逐点信息序中更大；最小不动点保留必要终止行为，把无有限证据的输入留为未定义。

例子与边界 ​

在部分自然数函数的逐点域中，底函数处处未定义。阶乘泛函满足

$$F(f)(0)=1,F(f)(n+1)=(n+1)f(n),$$

其中右侧调用未定义时结果也未定义。$F^1(\mathrm{\perp })$ 只定义输入 $0$，$F^2(\mathrm{\perp })$ 再定义输入 $1$，第 $k$ 轮覆盖有限前缀；上确界得到通常的总阶乘函数。

不动点不必唯一。恒等映射的每个元素都是不动点，Kleene 构造只选出 $\mathrm{\perp }$。因此本定理没有Banach 不动点定理公理库Banach 不动点定理Banach fixed-point theorem · Contraction mapping theorem完备度量空间上的压缩映射具有唯一不动点，且迭代以几何速度收敛。的唯一性结论。

仅有单调性也不够保证自然数次迭代在 $\omega$ 阶段闭合。完备格上的单调映射由Knaster–Tarski 定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。保证最小不动点存在，但可能需要超限迭代才能从底元到达；Scott 连续性正是把构造压缩到可数有限迭代上确界的额外条件。

推论与应用 ​

最小不动点语义公理库最小不动点语义Least-fixed-point semantics · Least fixed point semantics · Kleene fixed-point semantics以递归定义的有限展开链之上确界选取不凭空加入行为的最小语义解。把递归程序或 while 循环的语义泛函交给本定理：第 $n$ 次迭代对应至多展开有限层，极限收集所有有限终止运行。该结论是“存在规范语义解”和“该解可由有限近似描述”的桥梁。

在有限高度域中，递增链最终稳定，迭代在有限步得到最小不动点。在无限域中，上确界可能只在极限处出现；实现静态分析时加入 widening 得到的通常是安全前不动点，而非本公式的精确值。

参考资料

• Stephen Cole Kleene, Introduction to Metamathematics, North-Holland, 1952, fixed-point theorem for continuous functionals.
• Samson Abramsky and Achim Jung, “Domain Theory,” in Handbook of Logic in Computer Science, Vol. 3, Oxford University Press, 1994.
• Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993, Chapters 5–8.