指稱語意
維基百科,自由的 encyclopedia
在電腦科學中,指稱語意(英語:Denotational semantics)是通過構造表達其語意的(叫做指稱(denotation)或意義的)數學對象來形式化電腦系統的語意的一種方法。程式語言的形式語意的其他方法包括公理語意和操作語意。指稱語意方式最初開發來處理一個單一電腦程式定義的系統。後來領域擴充到了由多於一個程式構成的系統,比如網絡和並行系統。
指稱語意起源於 克里斯托弗·斯特雷奇 和 Dana Scott 在1960年代的工作。在 Strachey 和 Scott 最初開發的時候,指稱語意把電腦程式的指稱(意義)解釋為對映輸入到輸出的函數。後來證明對於允許包含遞歸定義的函數和數據結構,這樣的元素的程式的指稱(意義)定義太受限制了。為了解決這個困難,Scott 介入了基於域的指稱語意的一般性方法(Abramsky and Jung 1994)。後來的研究者介入了基於冪域的方法,來解決並行系統的語意的問題(Clinger 1981)。
粗略的說,指稱語意關注找到代表程式所做所為的數學對象。這種對象的搜集叫做域。例如,程式(或程式段)可以被偏函數,或演員事件圖想定,或用環境和系統之間的博弈表示: 它們都是域的一般性例子。
指稱語意的一個重要原則是「語意應當是複合性的」: 程式段的指稱應當建立自它的子段的指稱。最簡單的例子是: 「3 + 4」的意義確定自「3」、「4」和「+」的意義。
指稱語意最初被開發為把函數式和順序式程式建模為對映輸入到輸出的數學函數的框架。本文第一節描述在這個框架內開發的指稱語意。後續章節處理多型、並行等問題。