域理論

Dana Scott 在 1960 年代後期發起對域的研究的主要動機是為 lambda 演算找尋指稱語義。在這種形式化中，認為“函數”通過在這個語言中的特定項指定。在純粹語法方式下，可以得到從簡單函數到接受其他函數作為它的輸入參數的函數。再次只使用在這種形式化中的可獲得的語法變換，可以獲得所謂的不動點組合子(其中最著名的是 Y 組合子)；通過定義，它們有如下性質，對於所有函數 f 都有 f(Y(f)) = Y(f)。

要公式化這樣一種指稱語義，首先會嘗試為 lambda 演算構造一個模型，在其中為每個 lambda 項關聯上一個真正的(全)函數。這樣一種模型將形式化作為純語法系統的 lambda 演算和作為操縱具體的數學函數的符號系統的 lambda 演算之間的連接。不幸的是，這種模型不能存在，如果存在，它必須包含對應於組合子 Y 的一個真正的全函數，它是計算任意輸入函數 f 的不動點的函數。不能給予 Y 這樣的函數，因為某些函數(比如“後繼函數”)沒有不動點。這個對應於 Y 的真正函數至少必須是偏函數，對於某些輸入必須是未定義的。

Scott 通過形式化"部分"或"不完全"信息的概念來表示仍未返回一個結果的計算來克服這個困難。通過對計算的每個域(比如自然數)考慮一個額外的元素，表示“未定義”輸出，就是永不結束的計算的"結果"來建模。此外，計算的域被裝備了一個“次序關係”，在其中"未定義結果"是最小元素。

為 lambda 演算找到模型的一個重要步驟是隻考慮保證有最小不動點的那些函數(在這種偏序集合上)。這些函數的集合，與適當的排序一起，再次是這個理論意義上的一個"域"。而限制於所有可獲得的函數的一個子集有另一個巨大的好處: 有可能獲得包含它們自己的函數空間的域，就是得到應用於自身的函數。

除了這些需要的性質，域理論還允許吸引人的直覺釋義。同上所述，計算的域總是部分有序的。這種排序表示信息或知識的層次。元素在這個次序上越高，它就更加明確和包含更多的信息。更低的元素表示不完全的知識或中間結果。

接着通過在這個域上重複的應用單調函數來精製出結果。到達一個不動點等價於完成一個計算。域為這些想法提供了優越的設施，因為可以保證單調函數的不動點的存在，並且在額外的限制下，可以從下面逼近。