以下给出若干基础定义，然后陈述 Knaster–Tarski 不动点定理 与 Kleene 不动点定理。语言尽量保持数学教科书风格，并假设读者具有基本集合论与类型论背景。
1. 基本定义
1.1 偏序集
定义 1.1（偏序集） 设 (P) 为一个集合，(\le) 为 (P) 上的二元关系。若满足：
自反性 [ \forall x\in P,\quad x\le x ]
反对称性 [ x\le y \land y\le x \Rightarrow x=y ]
传递性 [ x\le y \land y\le z \Rightarrow x\le z ]
则称 ((P,\le)) 为一个 偏序集（partially ordered set, poset）。
1.2 上界与上确界
设 ((P,\le)) 为偏序集，(S\subseteq P)。
定义 1.2（上界）
若 [ \forall x\in S,\quad x\le u ] 则称 (u) 是 (S) 的 上界。
定义 1.3（上确界）
若 (u) 是 (S) 的上界，并且对任意上界 (v) 有 [ u\le v ] 则称 (u) 为 (S) 的 上确界（least upper bound），记为
[ u = \sup S ]
1.3 完备格
定义 1.4（格）
偏序集 (L) 称为 格，若任意 (x,y\in L) 都存在
- 上确界 (x\vee y)
- 下确界 (x\wedge y)
定义 1.5（完备格，complete lattice）
偏序集 (L) 称为 完备格，若对任意子集 [ S\subseteq L ] 都存在
[ \sup S \quad\text{和}\quad \inf S ]
特别地：
[ \bot = \inf L,\qquad \top = \sup L ]
分别称为 最小元 与 最大元。
1.4 单调函数
设 ((P,\le)) 为偏序集。
定义 1.6（单调函数）
函数 [ f:P\to P ] 称为 单调的，若
[ x\le y \Rightarrow f(x)\le f(y) ]
1.5 不动点
定义 1.7（不动点）
设 (f:P\to P)。
若
[ f(x)=x ]
则称 (x) 为 (f) 的 不动点。
记
[ \mathrm{Fix}(f)={x\in P\mid f(x)=x} ]
2. Knaster–Tarski 不动点定理
定理 2.1（Knaster–Tarski 不动点定理）
设 ((L,\le)) 为 完备格， (f:L\to L) 为 单调函数。
则：
- (f) 至少存在一个不动点。
- 所有不动点构成一个完备格。
- 特别地存在
最小不动点 [ \mathrm{lfp}(f)=\inf{x\in L\mid f(x)\le x} ]
最大不动点 [ \mathrm{gfp}(f)=\sup{x\in L\mid x\le f(x)} ]
并且满足
[ f(\mathrm{lfp}(f))=\mathrm{lfp}(f) ]
[ f(\mathrm{gfp}(f))=\mathrm{gfp}(f) ]
其中：
- (x) 满足 (f(x)\le x) 称为 前不动点 (pre-fixed point)
- (x) 满足 (x\le f(x)) 称为 后不动点 (post-fixed point)
3. 有向集与 DCPO
Kleene 定理需要更弱的结构。
3.1 有向集
定义 3.1（有向集，directed set）
设 (D\subseteq P)。
若满足
- (D\neq\varnothing)
- 对任意 (x,y\in D)，存在 (z\in D) 使得 [ x\le z \quad\text{且}\quad y\le z ]
则称 (D) 为 有向集。
3.2 DCPO
定义 3.2（DCPO）
偏序集 (P) 称为 DCPO（directed complete partial order），若
对任意 有向集
[ D\subseteq P ]
其上确界
[ \sup D ]
存在于 (P) 中。
3.3 序列链
定义 3.3（链）
集合 (C\subseteq P) 称为 链，若
[ \forall x,y\in C,\quad x\le y \ \text{或}\ y\le x ]
链是有向集的一种特殊情况。
3.4 连续函数（ω-连续）
定义 3.4
设 (P) 为 DCPO。函数 (f:P\to P) 称为 连续的，若对任意有向集 (D)
[ f(\sup D) = \sup_{x\in D} f(x) ]
在程序语义中通常只要求对 ω-链 成立。
4. Kleene 不动点定理
定理 4.1（Kleene 不动点定理）
设
- (P) 为具有最小元 (\bot) 的 DCPO
- (f:P\to P) 为 连续函数
定义序列
[ x_0=\bot ]
[ x_{n+1}=f(x_n) ]
则
[ \bot \le f(\bot) \le f^2(\bot) \le \cdots ]
构成一个递增链，并且
[ \mathrm{lfp}(f)=\sup_{n\in\mathbb{N}} f^n(\bot) ]
即：
[ \mathrm{lfp}(f)=\sup { \bot, f(\bot), f^2(\bot),\dots } ]
并满足
[ f(\mathrm{lfp}(f))=\mathrm{lfp}(f) ]
因此最小不动点可以通过 迭代极限 构造。
5. 两个定理的关系
结构要求从强到弱：
| 定理 | 偏序结构 | 函数条件 | 不动点构造 |
|---|---|---|---|
| Knaster–Tarski | complete lattice | 单调 | 通过所有前不动点/后不动点 |
| Kleene | DCPO + bottom | 连续 | 通过迭代极限 |
直观上：
- Knaster–Tarski 是最一般的不动点存在定理。
- Kleene 给出一种 构造最小不动点的方法。
如果需要，我可以继续给出：
- Bourbaki–Witt 不动点定理的严格表述
- 三个定理之间的 严格蕴含关系
- 以及 在 denotational semantics 中的具体应用。