Scott 连续映射

形式陈述 ​

设 $D,E$ 是DCPO公理库有向完备偏序Directed-complete partial order · DCPO · Directed complete poset每个非空有向子集都具有上确界的偏序，用于汇聚相容的信息近似。。映射 $f:D\to E$ 称为 Scott 连续，若它是单调映射公理库偏序集上的单调映射Monotone map on posets · Order-preserving map · Isotone map在偏序之间保持次序的映射，以及它作为单调算子参与不动点迭代时的基本结构。，并且对每个非空有向子集 $A\subseteq D$ 保持上确界：

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

单调性保证 $f[A]$ 仍有向，右侧上确界因而存在。部分文献把单调性从“保持有向上确界”推出，前提是允许单元素或二元素有向集并采用相同约定；本库把两项都显式列出，避免定义差异。

若论域只保证可数递增链的上确界，相应地只要求保持这些链，常称 $\omega$-连续。它足以支持许多可数迭代结论，却不等于保持任意有向上确界。

直觉 ​

Scott 连续性表达“有限可观察结果不能只在无限极限处突然出现”。输入近似不断增加时，函数输出也只能增加；把全部相容输入信息合并后再计算，与先计算每个有限阶段再合并输出，结果一致。

单调性只禁止撤回旧信息，仍允许函数在极限处凭空加入新信息。保持有向上确界排除了这种跳跃，因此是递归语义中比单调更强的条件。

例子与边界 ​

在幂集 DCPO 上，固定关系 $R\subseteq X\times Y$ 的直接像映射

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

保持任意并，因而 Scott 连续。有限规则系统的一步后继算子、把已有事实闭包一次的构造也常具有同样性质。

考虑链 $\mathbb{N}\cup \{\mathrm{\infty }\}$ 及通常次序，定义 $f(n)=0$（有限 $n$）而 $f(\mathrm{\infty })=1$。它单调，却不保持有向集 $\mathbb{N}$ 的上确界：

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

因此单调不推出 Scott 连续。

Scott 连续与实分析中的 $\epsilon$-$\delta$ 连续不是同一概念。给 DCPO 配备 Scott 拓扑后，以上定义可与拓扑连续性对应；若没有指定该拓扑，只因两者都叫“连续”就不能交换定理。

推论与应用 ​

Scott 连续映射对函数复合封闭，恒等映射也 Scott 连续，因此可组合地解释程序构造。pointed DCPO 上的 Scott 连续自映射由Kleene 不动点定理公理库Kleene 不动点定理Kleene fixed-point theorem · Kleene fixed point theorempointed DCPO 上 Scott 连续自映射的最小不动点由底元的有限迭代上确界给出。得到

$$\mathrm{lfp}(f)=\underset{n<\omega }{⨆}{f}^n(\mathrm{\perp }).$$

这使递归程序的整体含义由所有有限展开汇合而成。

在高阶语言中，适当函数空间按逐点次序构成域；只保留连续函数可确保应用与抽象仍兼容极限。实际语义模型还需证明函数空间确实具有所需完备性，不能仅凭“逐点定义”自动得到全部域论性质。

参考资料

• 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.