指稱語義檢視原始碼討論檢視歷史
指稱語義（英語：Denotational semantics）主要是指在計算機科學中，通過構造表達其語義的(叫做指稱(denotation)或意義的)數學對象來形式化計算機系統的語義的一種方法。編程語言的形式語義的其他方法包括公理語義和操作語義。指稱語義方式最初開發來處理一個單一計算機程序定義的系統。後來領域擴展到了由多於一個程序構成的系統，比如網絡和並發系統。[1]
目錄
簡介
在計算機科學中，指稱語義（英語：Denotational semantics）是通過構造表達其語義的(叫做指稱(denotation)或意義的)數學對象來形式化計算機系統的語義的一種方法。編程語言的形式語義的其他方法包括公理語義和操作語義。指稱語義方式最初開發來處理一個單一計算機程序定義的系統。後來領域擴展到了由多於一個程序構成的系統，比如網絡和並發系統。
指稱語義起源於克里斯托弗·斯特雷奇和Dana Scott在1960年代的工作。在 Strachey 和 Scott 最初開發的時候，指稱語義把計算機程序的指稱(意義)解釋為映射輸入到輸出的函數。後來證明對於允許包含遞歸定義的函數和數據結構，這樣的元素的程序的指稱(意義)定義太受限制了。為了解決這個困難，Scott 介入了基於域的指稱語義的一般性方法(Abramsky and Jung 1994)。後來的研究者介入了基於冪域的方法，來解決並發系統的語義的問題(Clinger 1981)。
粗略的說，指稱語義關注找到代表程序所做所為的數學對象。這種對象的搜集叫做域。例如，程序(或程序段)可以被偏函數，或演員事件圖想定，或用環境和系統之間的博弈表示: 它們都是域的一般性例子。
指稱語義的一個重要原則是「語義應當是複合性的」: 程序段的指稱應當創建自它的子段的指稱。最簡單的例子是: 「3 + 4」的意義確定自「3」、「4」和「+」的意義。指稱語義最初被開發為把函數式和順序式程序建模為映射輸入到輸出的數學函數的框架。本文第一節描述在這個框架內開發的指稱語義。後續章節處理多態、並發等問題。
遞歸程序的語義
在本節中我們概覽作為指稱語義的最初主題的函數式遞歸程序的語義。
問題如下。我們需要給予程序如階乘函數的定義以語義：function factorial(n:Nat):Nat ≡ if (n==0)then 1 else n*factorial(n-1)。這個階乘程序的意義應當是在自然數上一個函數，但是由於它的遞歸定義，如何以複合方式理解它是不明白的。
在遞歸的語義中，域典型的是偏序，它可以被理解為已定義性(definedness)的次序。例如，在自然數上的偏函數的集合可以給出為如下次序:給定偏函數 f 和 g，設「f≤g」意味着「在 f 定義的所有值之上 f 一致於 g」。通常假定這個域的某個性質，比如鏈的極限的存在性(參見cpo)和一個底元素。偏函數的偏序有一個底元素，完全未定義函數。它還有鏈的最小上界。各種額外性質經常是合理的和有用的: 在域理論條目中有更詳盡細節。
我們特別感興趣於在域之間的「連續」函數。它們是保持次序結構和保持最小上界的函數。在這種設置下，類型被指示為域，而域的元素粗略的捕獲了類型的元素。給予帶有自由變量的一個程序段的指稱語義，依據它從它的環境類型的指稱到它的類型的指稱的連續函數。例如，段落n*g(n-1)有類型Nat，它有兩個自由變量:Nat類型的n和Nat -> Nat類型的g。所以它的指稱將是連續函數
指稱語義的發展
通過研究編程語言的更精細的構造和不同的計算模型，指稱語義已經發展起來了。
狀態的指稱語義
狀態(比如堆)和命令特徵可以直接用上述指稱語義來建模。下面列出的所有教科書都有詳情。關鍵想法是把命令當作在某個狀態域上的偏函數。「x:=3」的指稱是使一個狀態成為帶有3被賦值給x的狀態。順序算符「;」被指示為函數複合。不動點構造被用來給予循環構造如「while」的語義。
在建模有局部變量的程序的時候事情變得更加困難。一種途徑是不在使用域，轉而把類型解釋為從世界的範疇到域的範疇的函子。程序被指示為在這些函子之間的自然連續函數。
數據類型的指稱
很多編程語言允許用戶定義遞歸數據類型。例如，數的列表的類型可以指定為
datatype list = Cons of (Nat, list) | Empty.
本節只處理不能變更的泛函數據類型。常規編程語言將典型的允許這種遞歸列表的元素被變更。
另一個例子: 無類型 lambda 演算的指稱為
datatype D = (D → D)
「解域方程」問題關注找到建模這類數據類型的域。有一種途徑，粗略的說把所有域的搜集自身當作一個域，並接着在這裡解這個遞歸定義。下面的教科書給出詳情。
多態數據類型是定義時帶有參數的數據類型。比如 αlists 的類型被定義為
datatype α list = Cons of (α, list) | Empty.
數的列表，接着是有類型Nat list，而字符串的列表有類型String list。
一些研究者開發了多態性的域理論模型。其他研究者還在構造性集合論內建模了參數化多態。詳情可見下面列出的教科書。
一個新近研究領域已經涉及了基於編程語言的對象和類的指稱語義。
受限複雜性的程序的指稱語義
隨着基於線性邏輯的編程語言的開發，指稱語義已經被給予了線性使用(參見證明網、一致空間)和多項式時間複雜性的語言。
非確定性程序的指稱語義
要給出非確定性程序順序程序指稱語義，研究者已經開發出了冪域理論。對冪域構造寫上P，域P(D) 是指示為D的類型的非確定性計算的域。
在非確定性域理論模型中在公正性和無界性上有困難。參見非確定性的冪域。
並發性的指稱語義
很多研究者爭論說域理論模型不捕獲並發計算的本質。為此介入各種新模型。在 1980 年代早期，人們開始使用指稱語義的方式給予並發語言以語義。例子包括Will Clinger 關於演員模型的工作；Glynn Winskel 關於事件結構和petri網的工作；和 Francez, Hoare, Lehmann 和 de Roever (1979) 關於CSP的跟蹤語義的工作。對所有這些工作的質詢仍在研究中。
最近，Winskel 和其他人已經提議了profunctor範疇作為並發的域理論。
順序性的指稱語義
順序編程語言PCF的完全抽象問題是在指稱語義中長時間的重要的開放問題。PCF 的困難在它是絕對的順序語言。例如，在 PCF 中無法定義並行或函數。為此如上述介紹的使用域的方式，產生了不是完全抽象的指稱語義。
這個開放問題在1990年代隨着博弈語義和涉及邏輯關係的技術的發展基本解決了。詳情請參見PCF語言。
源到源轉換的指稱語義
把一個程序語言轉換成另一個語言經常是有用的。例如一個並發編程語言可被轉換成進程演算；高級編程語言可以被轉換成字節碼(實際上，常規指稱語義可以被看作把編程語言解釋成域的範疇的內部語言)。
在這個語境中，來自指稱語義的概念，不如完全抽象，有助於滿足安全關注。
完全抽象
完全抽象的概念關心程序的指稱語義是否精確的匹配它的操作語義。完全抽象的關鍵性質有:
抽象性: 指稱語義必須使用獨立於編程語言的表示和操作語義的數學結構來做形式化；
可靠性: 所有觀察有區別的程序必須有不同的語義；
完備性: 有不同指稱的任何兩個程序必須有觀察區別。
我們希望在操作語義和指稱語義之間的額外想要的性質有:
「構造性」: 語義模型應當在只包含在可以直覺上構造的元素的意義上是構造性的。公式化這個性質的一種方式所有元素必須是有限元素的的有向集合的極限。
「累進性」: 對於每個系統S，都有語義的一個progressions函數，使得系統S的指稱(意義)是∨i∈ωprogressions(⊥S)，這裡的⊥S是S的初始格局(configuration)。
完全完備性: 語義模型的所有態射應當是程序的指稱。
在指稱語義中長期存在的重點是完全抽象存在于歸納類型中，特別是自然數的類型，作為接受用做遞歸的一種方法的類型。這個問題的傳統解釋是作為系統PCF語言的語義。在 1990年代成功的用博弈語義為 PCF 提供了完全抽象模型，導致了對指稱語義的工作在方式上的根本改變。
語義與實現
依據Dana Scott:
「語義確定一個實現不是必需的，它應該為證實一個實現是正確的提供標準。」
依據 Clinger :
「常規順序編程語言的形式語義通常自身可以被解釋為提供了一個(不充分)的這個語言的實現。雖然形式語義不必須總是提供這種實現，相信語義必須提供一個實現導致了關於並發語言的形式語義的混淆。當編程語言的語義中的無界非確定性被稱為蘊涵了這個編程語言不可能被實現被提出的時候這種混淆是明顯痛苦的。」
指稱語義的早期歷史
如前面提到過的，這個領域最初由Christopher Strachey和Dana Scott在 1960年代，接着由Joe Stoy在 1970年代於「Oxford University Computing Laboratory」的「Programming Research Group」開發。
Montague文法是英語的理想片段的某種形式的指稱語義。
同其他計算機科學領域的聯繫
某些指稱語義的著作把類型解釋為域理論意義上的域，因而可以被看作模型論的分支，導致了同類型論和範疇論的聯繫。在計算機科學內與抽象釋義、程序驗證和函數式編程有聯繫，參見函數式編程語言中的單子(monad)。特別是，指稱語義使用了續體(continuation)來依據函數式編程語義表達順序編程中的控制流。
視頻
指稱語義 相關視頻
參考文獻
- ↑ [ ], , --