有向完备偏序

形式陈述 ​

偏序集 $(D,⊑)$ 称为有向完备偏序（directed-complete partial order，DCPO），若每个非空有向子集公理库有向集Directed set · Directed preorder · 有向预序集以共同后继统一任意有限批进度的非空预序结构。 $A\subseteq D$ 都在 $D$ 中有上确界公理库上确界与下确界Supremum and infimum在偏序中分别作为集合最小上界与最大下界的最紧边界元素。

$$⨆A.$$

“$A$ 有向”沿用 $D$ 的次序：对任意 $x,y\in A$，存在 $z\in A$ 使 $x⊑z$ 且 $y⊑z$。若 $D$ 还有最小元素 $\mathrm{\perp }$，即 $\mathrm{\perp }⊑x$ 对所有 $x\in D$ 成立，则称 pointed DCPO。

本库采用“有向集非空”的约定，因此 DCPO 本身不自动含底元。另有文献把空集也视为有向，从而令其上确界成为 $\mathrm{\perp }$；比较定理时必须先统一约定。若只要求每条可数递增链有上确界，常称 $\omega$-CPO，它弱于一般 DCPO。

直觉 ​

把 $x⊑y$ 解释为“$y$ 至少包含 $x$ 的信息”。有向子集允许分叉，但任意有限批近似都能找到相容的共同扩展；其上确界汇集所有阶段已经稳定提供的信息，而不额外加入任意分支都未支持的结论。

$\mathrm{\perp }$ 表示完全未知、未定义或尚未产生结果。pointed 条件让递归计算可以从零信息开始迭代；DCPO 条件则保证相容近似的极限仍留在语义域内。

例子与边界 ​

幂集 $(\mathcal{P}(X),\subseteq )$ 是 DCPO；任意有向集合族的上确界是其并集。它事实上还是完备格公理库完备格Complete lattice · Complete ordered lattice任意子集都具有上确界和下确界，从而包含顶元、底元并支持任意族合流的格。，因为连非有向集合族也有并与交。

扁平自然数域

$${\mathbb{N}}_{\mathrm{\perp }}=\{\mathrm{\perp }\}\cup \mathbb{N},\mathrm{\perp }⊑n$$

且不同自然数彼此不可比，是 pointed DCPO。一个有向子集不能同时含两个不同自然数，所以其上确界要么是唯一出现的自然数，要么是 $\mathrm{\perp }$。这里“值变大”与“信息变多”被严格区分。

普通自然数按通常 $\le$ 排序不是 DCPO：整个 $\mathbb{N}$ 是有向集，却在 $\mathbb{N}$ 内没有上确界。给它加入 $\mathrm{\infty }$ 可补足这一极限，但会改变论域。

DCPO 不要求每个子集都有上确界或下确界。两个不相容元素可能没有共同上界，这与其作为信息分支的含义并不冲突。完备格则要求任意子集都有 join 和 meet，是更强且用途不同的结构。

推论与应用 ​

Scott 连续映射公理库Scott 连续映射Scott-continuous function · Scott continuity保持有向上确界的单调映射，使有限信息逼近与计算相容。保持有向上确界，使“先取信息极限再计算”与“先逐阶段计算再取极限”一致。pointed DCPO 上的 Scott 连续自映射进一步满足Kleene 不动点定理公理库Kleene 不动点定理Kleene fixed-point theorem · Kleene fixed point theorempointed DCPO 上 Scott 连续自映射的最小不动点由底元的有限迭代上确界给出。，可从 $\mathrm{\perp }$ 的有限迭代构造最小不动点。

指称语义公理库指称语义Denotational semantics把程序构造组合地解释为数学对象与函数的语义方法。借此表示非终止、部分函数和递归定义。静态分析也使用次序与不动点，但经常在完备格上调用 Knaster–Tarski；“都有最小不动点”不表示两种定理的结构假设或迭代结论可以互换。

参考资料

• Samson Abramsky and Achim Jung, “Domain Theory,” in Handbook of Logic in Computer Science, Vol. 3, Oxford University Press, 1994.
• Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993, Chapters 5–8.
• G. Gierz et al., Continuous Lattices and Domains, Cambridge University Press, 2003.