域理论
维基百科，自由的百科全书
域理论是研究通常叫做域(domain)的特定种类偏序集合的数学分支。因此域理论可以被看作是序理论的分支。这个领域主要应用于计算机科学，在这里用它来指定指称语义，特别是函数式编程语言的形式语义。域理论以非常一般化的方式形式化了逼近和收敛的直觉概念，并与拓扑有密切联系。在计算机科学中指称语义的一个可作为替代的方式是度量空间。
目录 |
[编辑] 动机和直觉
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 证明了任何表现得如同函数的行动者都是连续的。
域理论的一个重要应用是 Will Clinger 用它来开发并发计算的行动者模型的语义(参见指称语义)。
[编辑] 逼近和有限
域理论是建模信息状态的结构的纯粹定性的方式。你可以说某个东西包含更多信息，但是增加信息的数量没有指定。在某些情况下你希望在比给定信息状态更加简单(或更加不完全)的意义下谈论元素。例如，在某个幂集上自然的子集包含次序中，任何无限元素(也是集合)比任何它的有限子集更加富有信息。
如果你希望建模这样一种关联，你首先可能希望考虑带有次序 ≤ 的域的诱导出的严格次序 <。尽管在全序的情况下这是一个有用的概念，在偏序集合情况下它不能告诉我们更多东西。再次考虑集合的包含次序，一个集合已经严格小于另一个(可能无限的)集合，如果它包含的元素只少一个。你可以勉强的同意这捕获了更简单的概念。
更加精致的方式导致了所谓的逼近次序的定义，更推荐叫它为远低于关系。一个元素 x “远低于”(way below)一个元素 y，如果对带有上确界 sup(D)≥y 的所有有向集合 D，在 D 中有某个元素 d 使得 x≤d。那么你还可以称 x “逼近” y 并写为 x << y。这还蕴含了 x≤y，因为单元素集合 {y} 是有向的。例如，注意在一个集合的次序中，无限集合总是远高于(way above)任何它的有限子集。在另一方面，考虑有有限集合 {0}, {0, 1}, {0, 1, 2}, ... 的有向集合(事实上是链)，因为这个链的上确界是所有自然数的集合 N，这证实了没有无限集合远低于 N。
但是，远低于某个元素是个相对概念，并且不揭示更多关于单独元素的事情。例如，你可能喜欢用序理论的方式特征化有限集合，但是即使无限集合也可以远低于某个其他集合。这些有限元素 x 的特殊性质是它们远低于自身就是说 x<<x。有这种性质的元素也叫做紧致的。然而，这种元素在这些术语的其他数学使用中既不必须是有限的也不必须是紧致的。这种概念只是分别由它们在集合论和拓扑中概念的特定相似性而引发的。域的紧致元素有着重要的特殊性质，它不能作为它不在其中出现的一个有向集合的极限而获得。
关于远低于关系有很多其他重要结果支持了这个定义已经高度适合捕获域的很多重要方面的主张。更详细信息请参见远低于关系。
[编辑] 域的基
前面的思考引发了另一个问题: 是否有可能保证一个域的所有元素可以作为这种更简单元素的极限而获得? 这在实践中是非常重要的，因为我们不能计算无限对象但是我们仍然希望任意近的逼近它们。
更一般的说，我们希望限制于足够得到所有其他元素作为最小上界的那些元素的特定子集。因此，你定义偏序集合 P 的基为 P 的子集 B，是的对于 P 中每个 x，B 中远低于 x 的元素的集合包含带有上确界 x 的有向集合。偏序集合 P 是连续偏序集合，如果它有某个基。特别是，P 自身在这种情况下是一个基。在很多应用中，你限制于连续 (d)cpos 作为主要研究对象。
最后，通过要求存在紧致元素的一个基的而给出对偏序集合的一个更强限制。这样一个偏序集合叫做代数的。从指称语义的观点看，代数偏序集合是特别行为良好的，因为它们允许所有元素的逼近，即使限制于有限元素的时候。按前面所提及的，不是所有有限元素在经典意义上是“有限”的 ，有充分的理由这些有限元素可以构成一个不可数集合。
但是在某种意义上，偏序集合的基是可数的。在这种情况下，你称之为 ω-连续偏序集合。 因此，如果如果可数基完全由有限元素组成，我们获得的次序是ω-代数的。
[编辑] 特殊类型的域
域的简单的特殊情况叫做基本域或平坦域。这由不可比较的元素的集合组成，比如整数，同被认为小于所有其他元素的单一的“底”元素在一起。
你可以获得适合作为“域”的一些其他特殊种类的有序结构。我们已经提及了连续偏序集合和代数偏序集合。二者的更加特殊的版本是连续和代数 cpos。增加进一步的完备性性质，你能得到连续格和代数格，它们只是带有各自性质的完全格。在代数情况下，你找到了值得研究的更广泛的偏序集合种类: 历史上，Scott域是在域理论中最先研究的结构。更广阔的域种类由 SFP-域、L-域和双有限域组成。
所有这些种类的次序都可以被掷为各种 dcpos 范畴，使用单调、Scott-连续、甚至更特殊的函数作为态射。最后，术语“域”自身是不精确的，因此只在形式定义被给出之前或细节无关紧要的时候作为简略语来使用。
[编辑] 重要结果
偏序集合 D 是 dcpo，当且仅当在 D 中每个链都有上确界。但是，有向集合严格的比这些链更加强力。
带有一个最小元素的偏序集合 D 是 dcpo，当且仅当在 D 上所有单调函数 f 都有不动点。如果 f 是连续的，则它恰好有一个最小不动点，给出为 f 在最小元素 0 上的所有有限迭代的最小上界: Vn ∈ 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 0521803381
A standard resource on domain theory, which is freely available online:
- S. Abramsky, A. Jung: Domain theory. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, vol. III. Oxford University Press, 1994. (ISBN 019853762X) (download PDF PS.GZ)
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 0521784514
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.
