Knaster–Tarski 不动点定理

定理与两个规范公式 ​

设 $(L,\le )$ 是完备格公理库完备格Complete lattice · Complete ordered lattice任意子集都具有上确界和下确界，从而包含顶元、底元并支持任意族合流的格。，$F:L\to L$ 是单调自映射公理库偏序集上的单调映射Monotone map on posets · Order-preserving map · Isotone map在偏序之间保持次序的映射，以及它作为单调算子参与不动点迭代时的基本结构。。Knaster–Tarski 定理断言

$$\mathrm{Fix}(F)=\{x\in L:F(x)=x\}$$

在继承次序下自身构成完备格。特别地，$F$ 至少有一个不动点，并有最小、最大不动点

$$\mu F=\bigwedge \{x\in L:F(x)\le x\},$$$$\nu F=\bigvee \{x\in L:x\le F(x)\}.$$

第一式在全部前不动点中取下确界，第二式在全部后不动点中取上确界。它们不是从任意初值运行有限次迭代得到的算法定义。

最小不动点的证明主线 ​

令 $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$ 的下界，于是

$$F(m)\le m.$$

这说明 $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$ 是最小不动点。最大不动点由对偶论证得到。

证明只使用任意 meet/join 与单调性。没有距离、导数、紧致性或概率假设，也没有证明不动点唯一。

可达集合的实例 ​

在状态集合 $S$ 上定义

$$F(X)=I\cup \mathrm{post}(X),X\subseteq S.$$

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

最大不动点适合协归纳性质。例如若 $G(X)$ 收集能够继续满足某安全条件并转移回 $X$ 的状态，则 $\nu G$ 表示可以无限维持条件的最大区域。最小与最大不动点回答不同量词，不能因都满足 $F(x)=x$ 就互换。

迭代何时等于定理公式 ​

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

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

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

一般单调算子可能需要超限迭代。Scott 连续性会保证有向上确界可交换，从而得到更强的 Kleene 迭代结论，但那不是 Knaster–Tarski 的假设。

因此“定理保证存在”与“工作队列能快速算出”属于两个证明责任。静态分析用 widening 获得终止时，结果通常是某个前不动点，不保证等于最小不动点。

还要区分“全部不动点在 $L$ 中有任意上、下确界”和“直接沿用 $L$ 的 join/meet 就封闭”。不动点子集的上确界需先在 $L$ 中合流，再由定理构造相应不动点；它不一定等于候选不动点在母格中的裸 join。只证明最小、最大不动点存在，也尚未覆盖“全部不动点构成完备格”这一完整结论。

与 Banach 定理的边界 ​

Banach 不动点定理公理库Banach 不动点定理Banach fixed-point theorem · Contraction mapping theorem完备度量空间上的压缩映射具有唯一不动点，且迭代以几何速度收敛。在完备度量空间上要求压缩映射，得到唯一不动点与几何收敛速率。Knaster–Tarski 在完备格上只要求单调，允许多个不动点，却规范地选出最小和最大者。

例如恒等映射 $F(x)=x$ 在任意非平凡完备格上每个元素都是不动点，完全符合 Tarski，却不满足严格压缩。反过来，压缩映射的证明依赖距离收缩，不应改写成未验证的序单调论证。

二者可以在同一问题中分别适用，但所得结论必须各自追溯假设。

参考资料

• Alfred Tarski, “A Lattice-Theoretical Fixpoint Theorem and Its Applications,” Pacific Journal of Mathematics 5(2), 1955, pp. 285–309。
• B. A. Davey and H. A. Priestley, Introduction to Lattices and Order, 2nd ed., Cambridge University Press, 2002, §8.2。
• Patrick Cousot and Radhia Cousot, “Constructive Versions of Tarski's Fixed Point Theorems,” Pacific Journal of Mathematics 82(1), 1979, pp. 43–57。