維基百科

指稱語意

在電腦科學中，指稱語意（英語：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。所以它的指稱將是連續函數

 。

在這個偏函數的次序下，可以如下這樣給出階乘程式的指稱。首先，我們必須開發基本構造如 if-then-else, ==, 和乘法的指稱。還必須開發函數抽象和應用的指稱語意。程式段

λ n:N. if (n==0)then 1 else n*g(n-1)

可以接着被給予作為在偏函數的域之間的連續函數的一個指稱

 。

階乘程式的指稱被定義為函數 F 的最小不動點。它因此是域   的一個元素。

這種不動點存在的原因是 F 是連續函數。一種版本的Tarski不動點定理聲稱在域上的連續函數有最小不動點。

證明不動點定理的一種方式給出了為什麼以這種方式給出遞歸的語意合適的直覺認識，所有在域 D 的帶有底元素 ⊥ 的連續函數 F:D→D 都有不動點，它給出自

⊔i∈NFi(⊥)。

這裏的符號 Fi 指示 F 的 i 次應用。符號「⊔」意味着「最小上界」。

把這個鏈的構件認為是「迭代」的有益的。在上述階乘的情況下，我們有在偏函數的域上的函數 F。

  • F0(⊥) 是完全未定義偏函數 N→N；
  • F1(⊥) 是定義在 0 上，得到 1，在其他地方未定義的函數；
  • F5(⊥) 是定義直到 4 的階乘函數: F5(⊥)(4) = 24。它對於大於 4 的參數是未定義的。

所以這個鏈的最小上界是完全定義的階乘函數(它湊巧是全函數)。

指稱語意的發展

通過研究程式語言的更精細的構造和不同的計算模型，指稱語意已經發展起來了。

狀態的指稱語意

狀態(比如堆)和命令特徵可以直接用上述指稱語意來建模。下面列出的所有教科書都有詳情。關鍵想法是把命令當作在某個狀態域上的偏函數。「x:=3」的指稱是使一個狀態成為帶有 3 被賦值給 x 的狀態。順序算符「;」被指示為函數複合。不動點構造被用來給予迴圈構造如「while」的語意。

在建模有局部變數的程式的時候事情變得更加困難。一種途徑是不在使用域，轉而把類型解釋為從世界的範疇到域的範疇的函子。程式被指示為在這些函子之間的自然連續函數。[1][2]

資料類型的指稱

很多程式語言允許用戶定義遞歸資料類型。例如，數的列表的類型可以指定為

datatype list = Cons of (Nat, list) | Empty.

本節只處理不能變更的泛函數據類型。常規程式語言將典型的允許這種遞歸列表的元素被變更。

另一個例子: 無類型 lambda 演算的指稱為

datatype D = (D → D)

「解域方程」問題關注找到建模這類資料類型的域。有一種途徑，粗略的說把所有域的搜集自身當作一個域，並接着在這裏解這個遞歸定義。下面的教科書給出詳情。

多型資料類型是定義時帶有參數的資料類型。比如 α lists 的類型被定義為

datatype α list = Cons of (α, list) | Empty.

數的列表，接着是有類型 Nat list，而字串的列表有類型 String list。

一些研究者開發了多型性的域理論模型。其他研究者還在構造性集合論內建模了參數化多型。詳情可見下面列出的教科書。

一個新近研究領域已經涉及了基於程式語言的對象和類的指稱語意。[3]

受限複雜性的程式的指稱語意

隨着基於線性邏輯的程式語言的開發，指稱語意已經被給予了線性使用(參見 證明網、一致空間)和多項式時間複雜性的語言[4]。

非確定性程式的指稱語意

要給出非確定性程式順序程式指稱語意，研究者已經開發出了冪域理論。對冪域構造寫上 P，域 P(D) 是指示為 D 的類型的非確定性計算的域。

在非確定性域理論模型中在公正性和無界性上有困難。[5]參見非確定性的冪域。

並行性的指稱語意

很多研究者爭論說域理論模型不擷取並行計算的本質。為此介入各種新模型。在 1980 年代早期，人們開始使用指稱語意的方式給予並行語言以語意。例子包括Will Clinger 關於演員模型的工作；Glynn Winskel 關於事件結構和petri網的工作 [6]；和 Francez, Hoare, Lehmann 和 de Roever (1979) 關於CSP 的跟蹤語意的工作。對所有這些工作的質詢仍在研究中。

最近，Winskel 和其他人已經提議了 profunctor 範疇作為並行的域理論。[7][8]

順序性的指稱語意

順序程式語言 PCF 的完全抽象問題是在指稱語意中長時間的重要的開放問題。PCF 的困難在它是絕對的順序語言。例如，在 PCF 中無法定義並列或函數。為此如上述介紹的使用域的方式，產生了不是完全抽象的指稱語意。

這個開放問題在1990年代隨着博弈語意和涉及邏輯關係的技術的發展基本解決了。[9] 詳情請參見PCF語言。

源到源轉換的指稱語意

把一個程式語言轉換成另一個語言經常是有用的。例如一個並行程式語言可被轉換成行程演算；高階程式語言可以被轉換成位元組碼(實際上，常規指稱語意可以被看作把程式語言解釋成域的範疇的內部語言)。

在這個語境中，來自指稱語意的概念，不如完全抽象，有助於滿足安全關注。[10][11]

完全抽象

完全抽象的概念關心程式的指稱語意是否精確的匹配它的操作語意。完全抽象的關鍵性質有:

  1. 抽象性: 指稱語意必須使用獨立於程式語言的表示和操作語意的數學結構來做形式化；
  2. 可靠性: 所有觀察有區別的程式必須有不同的語意；
  3. 完備性: 有不同指稱的任何兩個程式必須有觀察區別。

我們希望在操作語意和指稱語意之間的額外想要的性質有:

  1. 「構造性」: 語意模型應當在只包含在可以直覺上構造的元素的意義上是構造性的。公式化這個性質的一種方式所有元素必須是有限元素的有向集合的極限。
  2. 「累進性」: 對於每個系統 S，都有語意的一個 progressions 函數，使得系統 S 的指稱(意義)是 ∨i∈ωprogressionsi(⊥S)，這裏的 ⊥S 是 S 的初始格局(configuration)。
  3. 完全完備性: 語意模型的所有態射應當是程式的指稱。

在指稱語意中長期存在的重點是完全抽象存在於歸納類型中，特別是自然數的類型，作為接受用做遞歸的一種方法的類型。這個問題的傳統解釋是作為系統 PCF語言的語意。在 1990年代成功的用博弈語意為 PCF 提供了完全抽象模型，導致了對指稱語意的工作在方式上的根本改變。

語意與實現

依據 Dana Scott [1980]:

「語意確定一個實現不是必需的，它應該為證實一個實現是正確的提供標準。」

依據 Clinger [1981]:

「常規順序程式語言的形式語意通常自身可以被解釋為提供了一個(不充分)的這個語言的實現。雖然形式語意不必須總是提供這種實現，相信語意必須提供一個實現導致了關於並行語言的形式語意的混淆。當程式語言的語意中的無界非確定性被稱為蘊涵了這個程式語言不可能被實現被提出的時候這種混淆是明顯痛苦的。」

指稱語意的早期歷史

如前面提到過的，這個領域最初由 Christopher Strachey 和 Dana Scott 在 1960年代，接着由 Joe Stoy 在 1970年代於「Oxford University Computing Laboratory」的「Programming Research Group」開發。

Montague文法是英語的理想片段的某種形式的指稱語意。

同其他電腦科學領域的聯絡

某些指稱語意的著作把類型解釋為域理論意義上的域，因而可以被看作模型論的分支，導致了同類型論和範疇論的聯絡。在電腦科學內與抽象釋義、程式驗證和函數式程式設計有聯絡，參見函數式程式設計語言中的單子(monad)。特別是，指稱語意使用了續體(continuation)來依據函數式程式設計語意表達順序編程中的控制流。

參照

教科書

  • Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
  • Carl Gunter, "Semantics of Programming Languages: Structures and Techniques". MIT Press, Cambridge, Massachusetts, 1992. (ISBN 978-0262071437)
  • Glynn Winskel, Formal Semantics of Programming Languages. MIT Press, Cambridge, Massachusetts, 1993. (ISBN 978-0262731034)
  • R. D. Tennent, Denotational semantics. Handbook of logic in computer science, vol. 3 pp 169--322. Oxford University Press, 1994. (ISBN 0-19-853762-X)

其他參照

  • - S. Abramsky and 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)
  • Irene Greif. Semantics of Communicating Parallel Professes MIT EECS Doctoral Dissertation. August 1975.
  • Gordon Plotkin. A powerdomain construction SIAM Journal of Computing September 1976.
  • Edsger Dijkstra. A Discipline of Programming Prentice Hall. 1976.
  • Krzysztof R. Apt, J. W. de Bakker. Exercises in Denotational Semantics MFCS 1976: 1-11
  • J. W. de Bakker. Least Fixed Points Revisited Theor. Comput. Sci. 2(2): 155-181 (1976)
  • Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1-5, 1977.
  • Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
  • Michael Smyth. Power domains Journal of Computer and System Sciences. 1978.
  • C.A.R. Hoare. Communicating Sequential Processes CACM. August, 1978.
  • George Milne and Robin Milner. Concurrent processes and their syntax JACM. April, 1979.
  • Nissim Francez, C.A.R. Hoare, Daniel Lehmann, and Willem-Paul de Roever. Semantics of nondeterminism, concurrency, and communication Journal of Computer and System Sciences. December 1979.
  • Nancy Lynch and Michael Fischer. On describing the behavior of distributed systems in Semantics of Concurrent Computation. Springer-Verlag. 1979.
  • Jerald Schwartz Denotational semantics of parallelism in Semantics of Concurrent Computation. Springer-Verlag. 1979.
  • William Wadge. An extensional treatment of dataflow deadlock Semantics of Concurrent Computation. Springer-Verlag. 1979.
  • Ralph-Johan Back. Semantics of Unbounded Nondeterminism ICALP 1980.
  • David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlag. 1980.
  • - Will Clinger, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.
  • Lloyd Allison, A Practical Introduction to Denotational Semantics Cambridge University Press. 1987.
  • P. America, J. de Bakker, J. N. Kok and J. Rutten. Denotational semantics of a parallel object-oriented language Information and Computation, 83(2): 152 - 205 (1989)
  • David A. Schmidt, The Structure of Typed Programming Languages. MIT Press, Cambridge, Massachusetts, 1994. ISBN 0-262-69171-X.
  • M. Korff True concurrency semantics for single pushout graph transformations with applications to actor systems Working papers of the Int. Workshop on Information Systems - Correctness and Reusability. World Scientific. 1995.
  • M. Korff and L. Ribeiro Concurrent derivations as single pushout graph grammar processes Proceedings of the Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation. ENTCS Vol 2, Elsevier. 1995.
  • Thati, Prasanna, Carolyn Talcott, and Gul Agha. Techniques for Executing and Reasoning About Specification Diagrams International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
  • J. C. M. Baeten. A brief history of process algebra Theoretical Computer Science. 2005.
  • J.C.M. Baeten, T. Basten, and M.A. Reniers. Algebra of Communicating Processes Cambridge University Press. 2005.
  • He Jifeng and C.A.R. Hoare. Linking Theories of Concurrency United Nations University International Institute for Software Technology UNU-IIST Report No. 328. July, 2005.
  • Luca Aceto and Andrew D. Gordon (editors). Algebraic Process Calculi: The First Twenty Five Years and Beyond Process Algebra. Bertinoro, Forl`ı, Italy, August 1–5, 2005.
  • Bill Roscoe. The Theory and Practice of Concurrency Prentice-Hall. 2005.
  • Carl Sassenrath (1999) denotational semantics （頁面存檔備份，存於互聯網檔案館） and the Rebol programming language
  • - A. W. Roscoe: The Theory and Practice of Concurrency, Prentice Hall, ISBN 0-13-674409-5. Revised 2005.
  • Carl Hewitt (2006) What is Commitment? Physical, Organizational, and Social （頁面存檔備份，存於互聯網檔案館） COIN@AAMAS. 2006.

外部連結

註釋

  1. ^ Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama: Syntactic control of interference revisited. Electr. Notes Theor. Comput. Sci. 1. 1995.
  2. ^ Frank J. Oles: A Category-Theoretic Approach to the Semanics of Programming. PhD thesis, Syracuse University. 1982.
  3. ^ Bernhard Reus, Thomas Streicher: Semantics and logic of object calculi. Theor. Comput. Sci. 316(1): 191-213 (2004)
  4. ^ P. Baillot. Stratified coherence spaces: a denotational semantics for Light Linear Logic ( ps.gz) Theoretical Computer Science , 318 (1-2), pp.29-55, 2004.
  5. ^ Paul Blain Levy: Amb Breaks Well-Pointedness, Ground Amb Doesn't. Electr. Notes Theor. Comput. Sci. 173: 221-239 (2007)
  6. ^ Event Structure Semantics for CCS and Related Languages. DAIMI Research Report, University of Aarhus, 67 pp., April 1983.
  7. ^ Gian Luca Cattani, Glynn Winskel: Profunctors, open maps and bisimulation. Mathematical Structures in Computer Science 15(3): 553-614 (2005)
  8. ^ Mikkel Nygaard, Glynn Winskel: Domain theory for concurrency. Theor. Comput. Sci. 316(1): 153-190 (2004)
  9. ^ P. W. O'Hearn and J. G. Riecke, Kripke Logical Relations and PCF, Information and Computation, Volume 120, Issue 1, July 1995, Pages 107-116.
  10. ^ Martin Abadi. Protection in programming-language translations. Proc. of ICALP'98. LNCS 1443. 1998.
  11. ^ Andrew Kennedy. Securing the .NET programming model. Theoretical Computer Science, 364(3). 2006

參見

取自 "https://zh.wikipedia.org/w/index.php?title=指称语义&oldid=79868238"