域理論
域理論（英語：Domain theory）是研究通常叫做「域」的特定種類偏序集合的數學分支。因此域理論可以被看作是序理論的分支。這個領域主要應用於計算機科學中，特別是針對函數式編程語言，用它來指定指稱語義。域理論以非常一般化的方式形式化了逼近和收斂的直覺概念，並與拓撲學有密切聯繫。在計算機科學中指稱語義的一個可作為替代的方式是度量空間。
動機和直覺 編輯
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 用它來開發並發計算的演員模型的語義(參見指稱語義)。
逼近和有限 編輯
域理論是建模信息狀態的結構的純粹定性的方式。你可以說某個東西包含更多信息，但是增加信息的數量沒有指定。在某些情況下你希望在比給定信息狀態更加簡單(或更加不完全)的意義下談論元素。例如，在某個冪集上自然的子集包含次序中，任何無限元素(也是集合)比任何它的有限子集更加富有信息。
如果你希望建模這樣一種關聯，你首先可能希望考慮帶有次序 ≤ 的域的誘導出的嚴格次序 <。儘管在全序的情況下這是一個有用的概念，在偏序集合情況下它不能告訴我們更多東西。再次考慮集合的包含次序，如果一個集合包含的元素比另一個(可能無限的)集合只少一個，從嚴格意義上說這是這個集合比另一個集合小，但這很難說這個集合比另一個集合更簡單。
遠低於關係 編輯
導致所謂「逼近次序」定義的更精細的方式是所謂的遠低於關係。元素 x 遠低於元素 y，如果對於所有有上確界
- y ≤ sup D，
的有向集合 D，有某個 D 中的元素 d 使得
- x ≤ d。
那麼你還可以稱 x「逼近」y 並寫為
- x << y。
這確實蘊涵了
- x ≤ y，
因為單元素集合 {y} 是有向的。例如，在集合的排序中，無限集合總是在任何有限集合的上面。在另一個方面，考慮有限集合的有向集合(事實上是鏈)
- {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 0-521-80338-1
可免費在線獲得的關於域理論的標資源:
- 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 0-19-853762-X) (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 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.