最小不动点语义

递归方程可能有多个数学解。仅仅验证“代回方程仍成立”，不能决定程序应该采用哪一个解。最小不动点从完全未知的 $\mathrm{\perp }$ 开始，每应用一次 $F$，只加入一层由程序体明确支持的新信息；极限中不会凭空出现缺少有限计算证据的终止结果。

“最小”指信息序中的信息最少，而不是返回值在数值上最小。对部分函数而言，在更多输入上终止的函数通常更大；两个函数在同一输入上返回不同数值时，往往根本不可比较。最小不动点保留递归方程强制得到的结果，同时把其余输入留在未定义状态。

这也解释了为什么从底元迭代具有操作意义。一次迭代对应允许一次递归调用展开，两次迭代对应允许两层展开。上确界不是把一个“无限运行”当作完成了的运行，而是把所有有限深度已经完成的运行合并起来。只有某个结果在有限阶段出现，它才进入最终语义。

把部分自然数函数按逐点信息序排列，底元素 $f_{\mathrm{\perp }}$ 在每个输入上都未定义。阶乘递归可由泛函 $F$ 表示：

其中若 $f(n)$ 未定义，右侧也未定义。于是 $F(f_{\mathrm{\perp }})$ 只知道 $0!$，$F^2(f_{\mathrm{\perp }})$ 又知道 $1!$，随后每轮多确定一个输入。链的上确界在每个自然数上给出通常的阶乘值，正好汇总了所有有限递归深度。

另一种递归可能永远无法产生新信息。若

则每个元素都是不动点，而从 $\mathrm{\perp }$ 开始的 Kleene 链始终停在 $\mathrm{\perp }$。最小不动点选择完全未定义的语义，因为方程本身没有提供任何有限证据去支持更丰富的结果。这一例子也说明 Scott 连续并不保证不动点唯一。

考虑命令 while true do skip。它的有限展开从来没有退出分支，因此每个近似在所有状态上都表示不终止，上确界仍是 $\mathrm{\perp }$。相比之下，while x>0 do x:=x-1 的第 $n$ 个近似能够处理至多需要 $n$ 轮的初始状态；所有近似的上确界覆盖每个自然数初值，却不会把一个实际无限循环的状态误判为终止。

Knaster–Tarski 定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。在完备格上只要求单调性，并给出全部不动点组成的完备格。Kleene 公式则依赖带底元的 DCPO 与 Scott 连续性，才能保证可数迭代链的上确界已经到达最小不动点。若只有单调性，达到最小不动点可能需要超越 $\omega$ 的迭代。

Banach 不动点定理公理库Banach 不动点定理Banach fixed-point theorem · Contraction mapping theorem完备度量空间上的压缩映射具有唯一不动点，且迭代以几何速度收敛。使用完备度量空间和收缩映射，结论是不动点唯一，并给出度量意义下的收敛速度。它与这里的信息序、底元和有限展开没有同一套假设，不能把“最小不动点”与“唯一不动点”混为一谈。

循环 while b do c 的指称可写成状态变换泛函的最小不动点。第零近似处处不终止，后续近似依次加入“执行至多有限轮后退出”的状态。这个构造把操作语义中的有限运行与指称语义中的序极限连接起来，也是证明两种语义一致时的关键接口。

递归函数、递归过程和某些递归类型方程沿用同一图景，但它们所处的语义域并不相同。部分函数域按定义域信息排序，状态变换域按终止行为排序，类型方程可能需要更丰富的域构造。统一之处是：递归体诱导连续泛函，有限展开形成递增近似，最小不动点选出不额外承诺行为的解。

静态分析也求解不动点，但目标常是收集语义公理库收集语义Collecting semantics · Reachability semantics at program points为每个程序点收集所有可达具体状态，作为静态分析需要可靠逼近的具体语义基准。或抽象域中的可达状态。有限高度格上的迭代会在有限步稳定；无限抽象域中则可能使用 widening 强制终止。widening 通常得到安全的后不动点近似，而非精确最小不动点，因此工程算法的终止保证不能被误写成语义等式。

最小不动点语义还支持固定点归纳：要证明 $\mathrm{lfp}(F)⊑a$，常可证明 $F(a)⊑a$，再利用最小性得到结论。程序验证中的不变式正是这种前不动点思想的具体表现；语义构造负责定义程序，归纳原理则把该定义转化为可用的证明规则。