Knaster–Tarski 不动点定理

最小不动点的证明主线 ​

令 $P=\{x:F(x)\le x\}$，并取 $m=\bigwedge P$。对每个 $x\in P$ 有 $m\le x$；由单调性得到 $F(m)\le F(x)\le x$，故 $F(m)$ 是 $P$ 的下界，于是

这说明 $m\in P$。再由 $F(m)\le m$ 和单调性得 $F(F(m))\le F(m)$，所以 $F(m)\in P$。既然 $m$ 是 $P$ 的最大下界，必有 $m\le F(m)$。两向合并得到 $F(m)=m$。

任取不动点 $x$，它满足 $F(x)=x\le x$，因此属于 $P$，而 $m=\bigwedge P\le x$。所以 $m$ 是最小不动点。最大不动点由对偶论证得到。

证明中，完备性提供前不动点集合的下确界，单调性让这个下确界本身成为不动点。

可达集合的实例 ​

在状态集合 $S$ 上定义

幂集 $(\mathcal{P}(S),\subseteq )$ 是完备格，$F$ 单调。最小不动点 $\mu F$ 恰是从初始集合 $I$ 可达的全部状态：它包含 $I$、对一步后继闭合，并且包含在每个满足这两项的集合中。

最大不动点适合协归纳性质。例如若 $G(X)$ 收集能够继续满足某安全条件并转移回 $X$ 的状态，则 $\nu G$ 表示可以无限维持条件的最大区域。最小不动点从初始状态向外积累可达状态，最大不动点则保留能够持续满足条件的状态。

迭代何时等于定理公式 ​

若 $L$ 有底元，可形成升链

在有限格中，链必于有限步稳定，稳定值就是 $\mu F$。无限格上，取自然数次迭代的上确界未必已是不动点；只有 $F$ 保存相应链的上确界时，才能在第 $\omega$ 阶段闭合。

一般单调算子可能需要超限迭代。Scott 连续性公理库Scott 连续映射Scott-continuous function · Scott continuity保持有向上确界的单调映射，使有限信息逼近与计算相容。会保证有向上确界可交换，从而由Kleene 不动点定理公理库Kleene 不动点定理Kleene fixed-point theorem · Kleene fixed point theorempointed DCPO 上 Scott 连续自映射的最小不动点由底元的有限迭代上确界给出。得到自然数次迭代公式，将存在性结论落实为这条可数迭代链的上确界。

Datalog 与有限最小不动点公理库Datalog 与有限最小不动点Datalog · Positive Datalog · Datalog least model在固定有限活跃域上反复应用正规则，证明所得关系是最小模型，并用有环可达性逐轮推导半朴素求值。给出有限关系上的具体实例：把输入值与程序常量组成有限域，在所有可生成事实的幂集上反复加入规则后承。每次严格变化至少增加一个事实，故有限稳定；再归纳证明每轮结果包含于任意规则模型，就得到最小性。

静态分析中的 widening 用更大的近似值加速升链稳定，得到满足 $F(x)\le x$ 的前不动点，作为包含所有可达状态的可靠上界。其精度取决于加速步骤保留了多少信息。

全部不动点的完备性也可由同一证明得到。给定 $A\subseteq \mathrm{Fix}(F)$，先在母格中取 $q=\underset{L}{\bigvee }A$。单调性给出 $q\le F(q)$，所以 $F$ 将完备区间格 $[q,\mathrm{\top }]$ 映回自身。在该区间上取最小不动点，就得到 $A$ 在不动点集合中的上确界：它恰是所有高于 $A$ 的不动点中最小的一个。下确界由对偶构造得到。因此不动点格的 join/meet 由母格与 $F$ 共同确定。

例如在 $\mathcal{P}(\{1,2,3\})$ 上，令 $F(X)=X\cup \{3\}$ 当 $\{1,2\}\subseteq X$，否则令 $F(X)=X$。它单调，$\{1\}$ 与 $\{2\}$ 都是不动点；两者在母格中的并 $\{1,2\}$ 却不是不动点，在不动点格中的 join 是 $\{1,2,3\}$。继承次序并不意味着直接继承母格的任意 join/meet。

与 Banach 定理的边界 ​

Banach 不动点定理公理库Banach 不动点定理Banach fixed-point theorem · Contraction mapping theorem完备空间中的统一压缩给出唯一不动点；用几何尾和证明收敛，并把后验误差与残差转成停止证书。在完备度量空间上要求压缩映射，得到唯一不动点与几何收敛速率。Knaster–Tarski 在完备格上只要求单调，允许多个不动点，却规范地选出最小和最大者。

例如恒等映射 $F(x)=x$ 在任意非平凡完备格上每个元素都是不动点，完全符合 Tarski，却不满足严格压缩。

概率循环期望界公理库概率循环不变式与期望界Probabilistic loop invariant · Expectation invariant以循环特征函数的不等式证明输出期望界，展示上界归纳、下界反例，以及几乎必停和有界性怎样消除尾项。给出一个定量接口：在可数离散状态上，非负扩展实值函数按逐点序构成完备格，满足 $\mathrm{\Phi }(I)\le I$ 的候选函数因而给循环最小不动点一个上界。在一般可测状态空间上，任意上确界未必仍可测，相关条目改用从零开始的可数迭代和单调收敛证明，避免省略完备格前提。