克纳斯特－塔斯基定理

在有序和格子理论的数学领域，以 Bronisław Knaster 和 Alfred Tarski 命名的克纳斯特－塔斯基定理陈述如下：

令 (L, ≤) 为完备格，令 f : L → L 为单调函数 (w.r.t. ≤ )。 则f在L中的不动点集也构成≤ 下的完备格。

塔斯基以最一般的形式陈述了结果，因此该定理通常被称为塔斯基不动点定理。 早些时候，Knaster 和 Tarski 建立了 L 是集合子集的格的特殊情况的结果，即幂集格。

该定理在程序设计语言的形式语义和抽象解释中有重要的应用。

Anne C. Davis 证明了该定理的一种逆：如果格 L 上的每个保序函数 f : L → L 都有一个不动点，则 L 是一个完备格。

由于完全格不可能是空的（它们必须包含空集的上确界和下界），该定理特别保证了 f 的至少一个不动点的存在，甚至最小不动点（或xxx不动点）的存在 ). 在许多实际情况中，这是该定理最重要的含义。

f 的最小不动点是最小元素 x 使得 f(x) = x，或者等价地，使得 f(x) ≤ x； 对偶适用于xxx不动点，即满足 f(x) = x 的xxx元素 x。

如果对于所有升序序列 xn，f(lim xn) = lim f(xn)，则 f 的最小不动点是 lim f n(0)，其中 0 是 L 的最小元素，从而给出定理的更具建设性的版本。 （参见：Kleene 不动点定理。）更一般地，如果 f 是单调的，则 f 的最小不动点是 f α(0) 的固定极限，在序数上采用 α，其中 f α 由超限归纳法定义： f α+1 = f (f α) 并且对于极限序数 γ 的 f γ 是所有小于 γ 的 β 序数的 f β 的最小上界。 对偶定理适用于xxx不动点。

例如，在理论计算机科学中，单调函数的最小不动点用于定义程序语义。 通常使用该定理的更专门版本，其中 L 被假定为某个集合的所有子集的格，这些子集按子集包含排序。 这反映了这样一个事实，即在许多应用中只考虑这样的格子。 人们通常会寻找具有作为函数 f 的不动点的属性的最小集合。 抽象解释充分利用了克纳斯特－塔斯基定理和给出最小和xxx不动点的公式。

克纳斯特－塔斯定理可以用来给出康托-伯恩斯坦-施罗德定理的简单证明。

可以为有序集制定克纳斯特－塔斯基础理论的较弱版本，但涉及更复杂的假设。 例如：

令 L 为具有最小元素的偏序集合（底部），令 f : L → L 为单调函数。 此外，假设 L 中存在 u 使得 f(u) ≤ u 并且子集中的任何链 { x ∈ L ∠ x ≤ f ( x ) , x ≤ u } {\displaystyle \{x\in L\mid x\leq f(x),x\leq u\}} 有一个上界。 那么 f 承认一个最小不动点。

这可以应用于获得不变集的各种定理，例如 Ok 定理：

对于单调映射 F : P(X ) → P(X ) 在 X 的（封闭）非空子集族上，以下是等价的： (o) F 在 P(X ) s.t. 中接纳 A。 A ⊆ F ( A ) {\displaystyle A\subseteq F(A)} , (i) F 承认 P(X ) 中的不变集 A，即 A = F ( A ) {\displaystyle A=F(A) } , (ii) F 承认xxx不变集 A, (iii) F 承认xxx不变集 A.

特别是，使用 Knaster-Tarski 原理可以发展非收缩不连续（多值）迭代函数系统的全局吸引子理论。 对于弱收缩迭代函数系统，Kantorovitch 不动点定理（也称为 Tarski-Kantorovitch 不动点原理）就足够了。

定点原理对有序集的其他应用来自微分、积分和算子方程理论。

让我们重述这个定理。

对于完整格子 ⟨ L ，≤ ⟩ {\displaystyle \langle L,\leq \rangle } 和单调函数 f : L → L {\displaystyle f\colon L\rightarrow L} 在 L ，f 的所有不动点的集合也是一个完整格 ⟨ P , ≤ ⟩ {\displaystyle \langle P,\leq \rangle } ，其中：

• ⋁ P = ⋁ { x ∈ L ‖ x ≤ f ( x ) } {\displaystyle \bigvee P=\bigvee \{x\in L\mid x\leq f(x) \}} 作为 f 的xxx不动点
• ⋀ P = ⋀ { x ∈ L ‖ x ≥ f ( x ) } {\displaystyle \bigwedge P=\bigwedge \{x\in L\mid x\geq f(x) \}} 作为 f 的最小不动点。

证明。 我们首先证明 P 既有最小元素又有xxx元素。 让 D = {x | x ≤ f(x)} 且 x ∈ D（我们知道至少 0L 属于 D）。 那么因为 f 是单调的，我们有 f(x) ≤ f(f(x))，即 f(x) ∈ D。