Kleene 不动点定理

从完全未知的 $\mathrm{\perp }$ 开始，每次应用 $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$ 次迭代对应至多展开有限层，极限收集所有有限终止运行。该结论是“存在规范语义解”和“该解可由有限近似描述”的桥梁。

在有限高度域中，递增链最终稳定，迭代在有限步得到最小不动点。在无限域中，上确界可能只在极限处出现；例如 $[0,1]$ 上 $F(x)=(x+1)/2$ 的有限迭代从零趋向最小不动点一，却没有一步达到一。前述“有限证据给出返回值”的读法适用于平坦结果域，不能要求任意 DCPO 的极限元素都在有限阶段出现。实现静态分析时加入 widening 得到的通常是安全前不动点，而非本公式的精确值。