最小不动点语义

形式陈述 ​

设 $(D,⊑,\mathrm{\perp })$ 是 pointed DCPO，$F:D\to D$ 是 Scott 连续映射。由单调性可得递增链

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

Kleene 不动点定理给出

$$\mathrm{lfp}(F)=\underset{n\ge 0}{⨆}{F}^n(\mathrm{\perp }),$$

且该元素满足 $F(\mathrm{lfp}(F))=\mathrm{lfp}(F)$。它还是所有不动点中相对于信息序 $⊑$ 的最小者：若 $F(x)=x$，则由 $\mathrm{\perp }⊑x$ 和单调性归纳得到 $F^n(\mathrm{\perp })⊑x$，取链上确界便有 $\mathrm{lfp}(F)⊑x$。

在指称语义公理库指称语义Denotational semantics把程序构造组合地解释为数学对象与函数的语义方法。中，递归定义或循环先被写成语义泛函 $F$ 的方程 $X=F(X)$。第 $n$ 次迭代只允许递归体展开有限层；所有有限近似的上确界定义整个程序，包括在有限步内始终不给出结果的部分 $\mathrm{\perp }$。

直觉 ​

递归方程常有多个数学解，单凭“把等式两边写成一样”不足以说明程序应该表示哪一个。最小不动点从完全未知的 $\mathrm{\perp }$ 出发，每应用一次 $F$ 就揭示多一层有限行为，最终只收集这些有限展开真正证实的信息。它不把任何没有有限证据支持的终止结果塞进语义，因此契合程序运行的操作直觉。

“最小”说的是信息最少，而非返回数值最小。一个函数在更多输入上终止，通常在函数空间的逐点信息序中更大；最小解保留递归方程强制的终止行为，却把无法由有限展开推出的输入留为未定义。这是选择规范解的原则，不是数值优化。

例子与边界 ​

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

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

其中右侧若调用 $f(n)$ 未定义，结果也未定义。从 $f_{\mathrm{\perp }}$ 开始，$F(f_{\mathrm{\perp }})$ 只在 $0$ 上给出 $1$；$F^2(f_{\mathrm{\perp }})$ 又能在 $1$ 上给出 $1$；继续迭代时，每一轮多确定一个输入。链的上确界在每个自然数上给出通常的阶乘值，正是递归程序所有有限调用深度的汇总。

不动点不必唯一。恒等映射 $F(x)=x$ 的每个元素都是不动点，而最小不动点只是 $\mathrm{\perp }$；因此“Scott 连续函数总有唯一不动点”是错误的。Banach 不动点定理公理库Banach 不动点定理Banach fixed-point theorem · Contraction mapping theorem完备度量空间上的压缩映射具有唯一不动点，且迭代以几何速度收敛。在完备度量空间上要求收缩映射并得到唯一不动点，所用结构与结论均不同。

Knaster–Tarski 定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。在完备格上对单调映射给出不动点格与最小不动点；这里的 Kleene 构造则依赖 pointed DCPO 和保持有向上确界的连续性，才能保证从 $\mathrm{\perp }$ 的可数迭代上确界本身是不动点。只知道单调而没有合适的完备性或连续性，不能直接套用同一公式。

推论与应用 ​

while b do c 的指称可写成状态变换泛函的最小不动点：第零近似处处不终止，后续近似依次容纳至多执行有限轮循环后退出的状态，极限汇集所有有限终止运行。递归函数和递归类型方程沿用这种 DCPO 上的有限展开图景；静态分析则从收集语义公理库收集语义Collecting semantics · Reachability semantics at program points为每个程序点收集所有可达具体状态，作为静态分析需要可靠逼近的具体语义基准。的具体可达状态集合出发，在完备格或抽象域中求解数据流不动点。两者可以由序理论互相参照，却不是同一个语义对象。

当语义抽象到有限高度的格时，迭代会在有限步稳定；在无限域上可能只在上确界处到达不动点。实现静态分析时若加入 widening 加速收敛，得到的往往是安全的后不动点近似，不再等同于精确最小不动点，这一工程折衷应与本页的精确语义构造区分。

参考资料

• Samson Abramsky and Achim Jung, “Domain Theory,” in Handbook of Logic in Computer Science, Vol. 3, Oxford University Press, 1994，fixed-point properties of continuous maps on domains。
• Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993，Chs. 5–8，fixed points, recursion, and denotational semantics。