格与 CPO——不动点栖身之处
上级:order-theory
完备性阶梯
- 格(lattice)——一个 偏序集,其中任意一对元素都有最小上界(并,join,
∨)和最大下界(交,meet,∧)。- 完备格(complete lattice)——任意子集都有并和交(因此存在顶元
⊤和底元⊥)。- CPO / dcpo——一个有最小元
⊥、且所有有向集(或所有链)都有并的偏序集。
为什么恰好是这两种强度: 它们是构造性不动点定理的居所(不需要选择公理):
- 完备格 → Knaster–Tarski 定理:单调映射的不动点构成一整个完备格(有一个最小不动点和一个最大不动点)。
- CPO → Kleene 定理:Scott 连续映射有一个最小不动点
⊔ₙ fⁿ(⊥),通过从⊥逐步爬升而得——这正是递归的语义。
例子: 幂集在 ⊆ 关系下(完备格);n 的因子在整除关系 | 下(一个格);按扩张排序的偏函数,以及"扁平"数据域,都是 CPO(⊥ = "未定义")——这正是指称语义学的设定。