域理論是研究通常叫做域(domain)的特定種類偏序集合的數學分支。因此域理論可以被看作是序理論的分支。這個領域主要套用於計算機科學中，特別是針對函式式程式語言，用它來指定指稱語義。域理論以非常一般化的方式形式化了逼近和收斂的直覺概念，並與拓撲學有密切聯繫。在計算機科學中指稱語義的一個可作為替代的方式是度量空間。
基本介紹
- 中文名：域理論
- 類屬：偏序集合的數學分支
- 提出人：Dana Scott
- 提出年代：1960 年代後期
特徵,公式介紹,
特徵
Dana Scott 在 1960 年代後期發起對域的研究的主要動機是為 lambda 演算找尋指稱語義。在這種形式化中，認為“函式”通過在這個語言中的特定項指定。在純粹語法方式下，可以得到從簡單函式到接受其他函式作為它的輸入參數的函式。再次只使用在這種形式化中的可獲得的語法變換，可以獲得所謂的不動點組合子(其中最著名的是 Y 組合子)；通過定義，它們有如下性質，對於所有函式 f 都有 f(Y(f)) = Y(f)。
公式介紹
要公式化這樣一種指稱語義，首先會嘗試為 lambda 演算構造一個模型，在其中為每個 lambda 項關聯上一個真正的(全)函式。這樣一種模型將形式化作為純語法系統的 lambda 演算和作為操縱具體的數學函式的符號系統的 lambda 演算之間的連線。不幸的是，這種模型不能存在，如果存在，它必須包含對應於組合子 Y 的一個真正的全函式，它是計算任意輸入函式 f 的不動點的函式。不能給予 Y 這樣的函式，因為某些函式(比如“後繼函式”)沒有不動點。這個對應於 Y 的真正函式至少必須是偏函式，對於某些輸入必須是未定義的。
Scott 通過形式化"部分"或"不完全"信息的概念來表示仍未返回一個結果的計算來克服這個困難。通過對計算的每個域(比如自然數)考慮一個額外的元素，表示“未定義”輸出，就是永不結束的計算的"結果"來建模。此外，計算的域被裝備了一個“次序關係”，在其中"未定義結果"是最小元素。
為 lambda 演算找到模型的一個重要步驟是只考慮保證有最小不動點的那些函式(在這種偏序集合上)。這些函式的集合，與適當的排序一起，再次是這個理論意義上的一個"域"。而限制於所有可獲得的函式的一個子集有另一個巨大的好處: 有可能獲得包含它們自己的函式空間的域，就是得到套用於自身的函式。
除了這些需要的性質，域理論還允許吸引人的直覺釋義。同上所述，計算的域總是部分有序的。這種排序表示信息或知識的層次。元素在這個次序上越高，它就更加明確和包含更多的信息。更低的元素表示不完全的知識或中間結果。
接著通過在這個域上重複的套用單調函式來精製出結果。到達一個不動點等價於完成一個計算。域為這些想法提供了優越的設施，因為可以保證單調函式的不動點的存在，並且在額外的限制下，可以從下面逼近。
