DCPO 与 Scott 连续：信息极限的结构

形式陈述

有向完备偏序（DCPO）描述一种能够接纳相容信息极限的偏序结构。设 $(D,\sqsubseteq)$ 为偏序集。非空子集 $A\subseteq D$ 若满足

\forall x,y\in A\quad \exists z\in A\quad x\sqsubseteq z\ \land\ y\sqsubseteq z,

就称为有向子集。若每个这样的 $A$ 都有上确界 $\bigsqcup A\in D$ ，则 $D$ 是 DCPO。若还存在最小元素 $\bot$ ，则称为 pointed DCPO。 $\bot$ 常表示没有信息、未返回结果或未定义状态。

Scott 连续映射描述函数怎样与这些极限相容。对 DCPO $D,E$ ，映射 $f:D\to E$ 必须先是单调的，并且对每个非空有向子集 $A\subseteq D$ 满足

f\!\left(\bigsqcup A\right) = \bigsqcup_{a\in A} f(a).

DCPO 是空间的性质，Scott 连续性是映射的性质。前者保证极限存在，后者保证函数保持极限。二者共同出现于域论，却承担不同的证明责任，不能把“某个偏序是 DCPO”与“某个函数 Scott 连续”压成同一个类型判断。

若只要求每条可数递增链具有上确界，常称 $\omega$ -CPO；若函数只保持这些链的上确界，则得到相应的 $\omega$ -连续版本。很多程序语义只需要可数迭代，但使用完整 DCPO 定理时仍应明确更强假设。

直觉

把 $x\sqsubseteq y$ 理解为“ $y$ 至少包含 $x$ 已经揭示的信息”。有向子集允许近似暂时分叉，却要求任意有限批近似都有相容的共同扩展。它的上确界不是从外部猜出的答案，而是把所有阶段已经稳定提供的信息汇在一起。

Scott 连续性则排除两种不合语义的行为。单调性禁止在获得更多输入信息后撤回旧结论；保持有向上确界进一步禁止函数只在无限极限处突然产生一个任何有限阶段都看不到的有限结果。于是，“先把输入近似汇成极限再运行函数”与“先在每个阶段运行函数再汇总结果”得到同一对象。

这给递归定义一幅具体图像。从 $\bot$ 开始反复应用程序算子 $F$ ：第一次展开得到一层可观察行为，第二次再多一层，依此类推。若 $F$ Scott 连续，所有有限展开的上确界就是整体递归含义，而不需要把无限程序执行当作一个预先存在的黑箱。

例子与边界

幂集 $(\mathcal P(X),\subseteq)$ 是 DCPO。有向集合族的上确界就是并集；事实上它还是完备格，因为任意集合族都拥有并与交。对固定关系 $R\subseteq X\times Y$ ，直接像映射

F(S)=\{y\in Y:\exists x\in S,(x,y)\in R\}

保持任意并，因此 Scott 连续。许多规则闭包的一步算子具有同样结构：新事实只能由有限前提触发，因而不会等到极限才凭空出现。

扁平自然数域

\mathbb N_\bot=\{\bot\}\cup\mathbb N, \qquad \bot\sqsubseteq n

也是 pointed DCPO，不同自然数彼此不可比。它把“尚未返回”与“已经返回具体值”排成信息次序，却没有把数值大小误当作信息大小。一个有向子集不能同时包含两个不同的完成值，所以其上确界要么是某个唯一自然数，要么是 $\bot$ 。

普通自然数按通常 $\le$ 排序不是 DCPO，因为整个 $\mathbb N$ 有向，却在自身内部没有上确界。给它补上 $\infty$ 可以修复这一缺口，但也改变了论域。DCPO 只要求有向子集有上确界；它不要求任意不相容分支都有共同上界，更不要求每个子集都有 meet 与 join。

单调也不自动推出 Scott 连续。在链 $\mathbb N\cup\{\infty\}$ 上定义 $f(n)=0$ （有限 $n$ ）而 $f(\infty)=1$ 。该函数单调，却有

f(\sup\mathbb N)=1 \ne 0= \sup_{n<\infty} f(n).

它正是在极限点发生跳跃。这个反例说明，Scott 连续性的核心不是“输出不会下降”，而是“有限可观察输出必须在某个有限阶段已经出现”。

推论与应用

pointed DCPO 上的 Scott 连续自映射满足Kleene 不动点定理：

\operatorname{lfp}(F) = \bigsqcup_{n<\omega}F^n(\bot).

这条公式把结构、映射和定理依次连接起来：DCPO 提供迭代链的上确界，Scott 连续性把 $F$ 推过该上确界，Kleene 定理再证明结果是最小不动点。最小不动点语义据此解释递归程序、递归类型和部分函数。

Knaster–Tarski 定理走的是另一条路线。它要求完备格上的单调自映射，保证不动点集合本身形成完备格，却不自动给出从 $\bot$ 经过可数迭代达到最小不动点的公式。Banach 不动点定理又依赖完备度量空间和压缩性，得到唯一不动点与几何收敛率。三者都谈不动点，但结构假设、构造方式和结论强度不同。

在指称语义中，函数空间通常按逐点次序组织，并限制到连续函数，使应用、抽象和递归都保持信息极限。静态分析也使用序与不动点，不过常在完备格上处理性质集合。选择哪种结构，应由“程序结果如何被有限观察”和“分析状态如何合并”决定，而不是因为公式都写成 $\operatorname{lfp}$ 就交换定理。

参考资料

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.
David A. Schmidt, Denotational Semantics: A Methodology for Language Development, Allyn and Bacon, 1986.

形式陈述 ​

形式陈述