DCPO 与 Scott 连续

形式陈述 ​

在偏序集公理库偏序Partial order · Partially ordered set满足自反、反对称和传递性的关系。 $(D,⊑)$ 中，非空子集 $A\subseteq D$ 称为有向的，若任意 $x,y\in A$ 都存在 $z\in A$ 使 $x⊑z$ 且 $y⊑z$。若每个有向子集 $A$ 都在 $D$ 中有上确界公理库上确界与下确界Supremum and infimum在偏序中分别作为集合最小上界与最大下界的最紧边界元素。 $⨆A$，则 $D$ 是 directed-complete partial order，简称 DCPO。若 DCPO 还有最小元素 $\mathrm{\perp }$，即对所有 $x\in D$ 都有 $\mathrm{\perp }⊑x$，则称为 pointed DCPO。

DCPO 间的映射 $f:D\to E$ 称为 Scott 连续，若它单调，并对每个有向集 $A\subseteq D$ 保持有向上确界：

$$f(⨆A)=\underset{a\in A}{⨆}f(a).$$

单调性保证 $f[A]$ 仍是有向集；保持上确界表示先汇总一列相容近似再计算，与先逐个计算再取信息极限得到同一结果。某些入门语义只要求每条可数递增链有上确界，称 $\omega$-CPO，并只要求保持这类链的上确界；这比完整 DCPO 假设窄，使用时应明确版本。

直觉 ​

域论把偏序解释为信息量：$x⊑y$ 表示 $y$ 至少包含 $x$ 已经给出的信息。两个近似未必可比较，但有向集要求其中任意有限进展都能在集合内找到一个共同的更精确阶段，因此它描述的是一条可能分叉、却始终相容的逼近过程。上确界不是额外猜出的答案，而是汇集全部阶段信息的最小上界。

$\mathrm{\perp }$ 表示完全没有结果或尚未定义。Scott 连续函数既不能在输入信息增多时撤回旧结论，也不能只在无限极限处凭空产生任何有限阶段都看不到的新信息。正是这个“有限可观察结果必在某个有限近似中出现”的性质，使递归程序可以由逐层展开来解释。

例子与边界 ​

扁平自然数域

$${\mathbb{N}}_{\mathrm{\perp }}=\{\mathrm{\perp }\}\cup \mathbb{N},\mathrm{\perp }⊑n\text{ 对所有 }n\in \mathbb{N},$$

且不同自然数彼此不可比。它是 pointed DCPO：一个有向子集不可能同时含两个不同自然数，因此其上确界要么是唯一出现的自然数，要么是 $\mathrm{\perp }$。这里 $\mathrm{\perp }$ 可表示计算尚未返回，而某个 $n$ 表示已经得到确定结果；从一个确定自然数再“增长”为另一个自然数会推翻已有信息，所以偏序不允许这样做。

普通自然数按通常的 $\le$ 排序却不是 DCPO。整个 $\mathbb{N}$ 自身是有向集，却在 $\mathbb{N}$ 内没有上确界；只有把适当的无穷元素加入论域，或限制所需链，才能补足该极限。这也说明 DCPO 不是“任意偏序都有”的性质。

DCPO 只要求有向子集有上确界，不要求每个子集都有上确界；完备格公理库完备格Complete lattice · Complete ordered lattice任意子集都具有上确界和下确界，从而包含顶元、底元并支持任意族合流的格。则要求任意子集都有上、下确界，是更强而用途不同的结构。相应地，Knaster–Tarski 定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。只需完备格上的单调自映射便给出不动点格，却不自动给出 Scott 连续映射从 $\mathrm{\perp }$ 出发的可数逼近公式。

Scott 连续也不是实分析中基于 $\epsilon$–$\delta$ 或度量的连续。它可等价联系到 Scott 拓扑中的拓扑连续性，但不能在没有指定序与拓扑时把两种“连续”直接互换。

推论与应用 ​

pointed DCPO 上的 Scott 连续自映射支持由 $\mathrm{\perp },F(\mathrm{\perp }),F^2(\mathrm{\perp }),\dots$ 形成的递增近似，并由其上确界构造最小不动点语义公理库最小不动点语义Least-fixed-point semantics · Least fixed point semantics · Kleene fixed-point semantics以递归定义的有限展开链之上确界选取不凭空加入行为的最小语义解。。函数空间可按逐点次序构成新的域，使高阶函数与递归函数同样进入这个框架。指称语义公理库指称语义Denotational semantics把程序构造组合地解释为数学对象与函数的语义方法。借此把非终止、部分定义和有限观察统一成数学对象。

静态分析与时序逻辑也使用最小、最大不动点，但常把性质组织成完备格，并通过 Tarski 的单调不动点理论刻画收集语义、数据流方程或模态 $\mu$ 演算。两条路线共享次序图像：DCPO/Scott 连续强调递归含义怎样由相容有限近似逼近，完备格/Tarski 强调性质算子在全体上下确界齐备的空间中有哪些不动点。不能只因都写作 $\mathrm{lfp}$ 就交换假设。

选择 DCPO 时，偏序必须反映语言真正可观察的信息。若把数值大小误当作信息顺序，“最小不动点”就会被错误理解成数值最小解；扁平域通过让不同完成值不可比，明确区分了结果内容与信息是否已经产生。

参考资料

• Samson Abramsky and Achim Jung, “Domain Theory,” in Handbook of Logic in Computer Science, Vol. 3, Oxford University Press, 1994，§§2.1.5–2.1.6。
• Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993，Chs. 5–8，complete partial orders and continuous functions。