茶年 · 中文维基百科

域理论

Wikipedia · 2026-01-25 维基百科 👁 1 阅读

域理论（）是研究通常叫做「域」的特定种类偏序集合的数学分支。因此域理论可以被看作是序理论的分支。这个领域主要应用于计算机科学中，特别是针对函数式编程语言，用它来指定指称语义。域理论以非常一般化的方式形式化了逼近和收敛的直觉概念，并与拓扑学有密切联系。在计算机科学中指称语义的一个可作为替代的方式是度量空间。

动机和直觉
Dana Scott 在 1960 年代后期发起对域的研究的主要动机是为 lambda 演算找寻指称语义。在这种形式化中，认为“函数”通过在这个语言中的特定项指定。在纯粹语法方式下，可以得到从简单函数到接受其他函数作为它的输入参数的函数。再次只使用在这种形式化中的可获得的语法变换，可以获得所谓的不动点组合子(其中最著名的是 Y 组合子)；通过定义，它们有如下性质，对于所有函数 f 都有 f(Y(f)) = Y(f)。

要公式化这样一种指称语义，首先会尝试为 lambda 演算构造一个模型，在其中为每个 lambda 项关联上一个真正的(全)函数。这样一种模型将形式化作为纯语法系统的 lambda 演算和作为操纵具体的数学函数的符号系统的 lambda 演算之间的连接。不幸的是，这种模型不能存在，如果存在，它必须包含对应于组合子 Y 的一个真正的全函数，它是计算任意输入函数 f 的不动点的函数。不能给予 Y 这样的函数，因为某些函数(比如“后继函数”)没有不动点。这个对应于 Y 的真正函数至少必须是偏函数，对于某些输入必须是未定义的。

Scott 通过形式化"部分"或"不完全"信息的概念来表示仍未返回一个结果的计算来克服这个困难。通过对计算的每个域(比如自然数)考虑一个额外的元素，表示“未定义”输出，就是永不结束的计算的"结果"来建模。此外，计算的域被装备了一个“次序关系”，在其中"未定义结果"是最小元素。

为 lambda 演算找到模型的一个重要步骤是只考虑保证有最小不动点的那些函数(在这种偏序集合上)。这些函数的集合，与适当的排序一起，再次是这个理论意义上的一个"域"。而限制于所有可获得的函数的一个子集有另一个巨大的好处: 有可能获得包含它们自己的函数空间的域，就是得到应用于自身的函数。

除了这些需要的性质，域理论还允许吸引人的直觉释义。同上所述，计算的域总是部分有序的。这种排序表示信息或知识的层次。元素在这个次序上越高，它就更加明确和包含更多的信息。更低的元素表示不完全的知识或中间结果。

接着通过在这个域上重复的应用单调函数来精制出结果。到达一个不动点等价于完成一个计算。域为这些想法提供了优越的设施，因为可以保证单调函数的不动点的存在，并且在额外的限制下，可以从下面逼近。

形式定义指南
在本章节中，将介绍域理论的中心概念和定义。强调上述的域为“信息排序”的直觉来引发这个理论的数学形式化。精确的形式定义可以在每个概念的专门文章中找到。包含域理论概念的一般的序理论定义可以在序理论术语表中找到。下面只介绍域理论最重要的概念。

有向集合作为收敛规定
按前面所提及的，域理论处理偏序集合来建模计算的域。目标是把这种次序下的元素解释为“信息片段”或“计算的(部分)结果”，这里的在次序上更高的元素以一种一致性的方式扩展了下面元素的信息。从这个简单直觉例子中，已经明显的看出域经常没有最大元素，因为这将意味着有一个元素包含所有其他元素的信息 - 这是一个非常无趣的情况。

在这个理论中扮演重要角色的概念是一个域的有向子集，就是说在其中每两个元素都有某个上界的次序的非空子集。按我们关于域的直觉看法，这意味着在有向子集内的每两个信息片段都可以被在子集内的某个其他元素所一致性的扩展(extend)。所以我们可以把有向集合看作一致性规定，就是看作在其中没有两个元素有矛盾的“部分结果”的集合。这个解释可以比较于在数学分析中的序列的概念，在这里每个元素都被前面的更加特殊。实际上，在度量空间理论中，序列扮演了在很多方面类似于有向集合在域理论中的角色。

现在在序列的情况下，我们感兴趣于有向集合的极限。依据上面所述，这将是扩展这个有向集合的所有元素的信息的最一般性的信息片段，就是说包含在这个有向集合中出现的“全部的”信息的唯一的元素 - 而没有东西有更多的信息。在序理论的形式化中，这叫做有向集合的最小上界。在序列的极限的情况下，有向集合的最小上界总是存在的。

自然的，你会特别感兴趣于在其中所有一致性规定都收敛的计算域，就是说，它有着所有有向集合都有一个最小上界的次序。这个性质定义了有向完全偏序，简写为 dcpo。实际上，域理论的多数考虑都只考虑至少是有向完全的次序。

从部分指定的结果表示不完全的知识的根基性想法，你能得出另一个需要的性质: 存在最小元素。这样的一个元素建模了没有信息的状态 - 这是大多数计算开始的地方。它也可以被当作根本不返回任何结果的计算的输出。由于它对于这个理论的重要性，带有最小元素的 dcpos 被叫做完全偏序或简写为 cpos。

计算和域
现在我们有了计算的域应当是什么样的基本形式描述，我们可以转到计算自身。明显的，它们必须是函数，从某个计算域接受输入并返回在某个(可能不同的)域中的输出。但是，你还希望在输入的信息内容增加的时候函数的输出包含更多的信息。形式上，这意味着我们希望一个函数是单调的。

在处理 dcpos 的时候，你还可能希望计算兼容于有向集合的极限的公式化。形式的说，这意味着对于某个函数 f，有向集合 D 的像 f(D)(就是 D 的每个元素的像的集合)再次是有向的并且有一个最小上界，就是 D 的最小上界的像。你还可以称 f“保持了有向上确界”。还要注意，通过考虑两个元素的有向集合，这样的函数也必须是单调的。这些性质引发了 Scott-连续函数的概念。因为经常是没有歧义的，你也可以称它为连续函数。Henry Baker 和 Carl Hewitt 证明了任何表现得如同函数的演员(actor)都是连续的。

域理论的一个重要应用是 Will Clinger 用它来开发并发计算的演员模型的语义(参见指称语义)。

逼近和有限
域理论是建模信息状态的结构的纯粹定性的方式。你可以说某个东西包含更多信息，但是增加信息的数量没有指定。在某些情况下你希望在比给定信息状态更加简单(或更加不完全)的意义下谈论元素。例如，在某个幂集上自然的子集包含次序中，任何无限元素(也是集合)比任何它的有限子集更加富有信息。

如果你希望建模这样一种关联，你首先可能希望考虑带有次序 ≤ 的域的诱导出的严格次序 n ∈ N f n(0)。

当然，有很多其他重要的结果，依赖于域理论所应用的领域。请参阅下面列出的文献。

文献
Probably one of the most recommendable books on domain theory today, giving a very clear and detailed view on many parts of the basic theory:

  • G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott, Continuous Lattices and Domains, In Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge University Press, 2003. ISBN 0-521-80338-1

可免费在线获得的关于域理论的标资源:

One of Scott's classical papers:

  • D. S. Scott. Data types as lattices. In G. Muller et al., editors, Proceedings of the International Summer Institute and Logic Colloquium, Kiel, volume 499 of Lecture Notes in Mathematics, pages 579-651, Springer-Verlag, 1975.

A general, easy-to-read account of order theory, including an introduction to domain theory as well:

  • B. A. Davey and H. A. Priestley, Introduction to Lattices and Order, 2nd edition, Cambridge University Press, 2002. ISBN 0-521-78451-4

A readable account of the Laws for Actor systems and how they can be used to prove Scott's continuity criterion:

  • Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1-5, 1977.

A general, easy-to-read account of the Actor model of concurrent computation, using only elementary domain theory:
W. Clinger. Foundations of Actor Semantics* MIT Mathematics Doctoral Dissertation. June 1981.

参见
*类型论
*范畴论

#序理论 #域理论

评论 (0)

  • 还没有评论，来抢沙发吧。