演員模型的指稱語義

演員模型指稱語義(Denotational semantics of the Actor model)是演員的指稱域理論的研究主題。這個主題的歷史發展參見指稱語義的歷史

演員不動點語義

編輯

計算系統語義的指稱理論關心找到表示系統作為的數學物件。這個理論利用了計算數學。這種計算域的例子是偏函數和演員事件圖場景。

關係 x≤y 意味着 x 可以計算演進為 y。如果指稱是偏序函數,比如 f≤g 可以意味着 f 一致於 gf 在其上定義的所有值上。如果指稱是演員事件圖場景,x≤y 意味着滿足 x 的系統可以演進到滿足 y 的一個系統。

計算域有下列性質:

  1. 底存在。域有最小元素指示為 使得對於所有域中元素 x⊥≤x
  2. 極限存在。隨着計算繼續,指稱應當變得更好並有一個極限,使得如果有    ,則最小上界   應當存在。這個性質叫做 ω-完全性。
  3. 有限元素是可數的。一個元素 x有限的(在域文獻中也叫做孤立的),當且僅當只要 A有向的,∨A 存在並且  ,就存在   有着  。換句話說,x 是有限的,如果必須通過 x 來趕上或通過極限過程來超過 x
  4. 所有元素都是有限元素的可數遞增序列的最小上界。在直覺上這意味着所有元素都可以通過在其中所有進步(progression)都是有限的一個計算過程來到達。
  5. 域是向下閉合的

由系統 S 指示的數學指稱通過構造從叫做 S 的空指稱遞增更好的逼近來找到 ,使用某個逼近定義函數 progressions(進步)如下這樣構造 S 的指稱(意義)的 [Hewitt 2006b]:

Denotes ≡ ∨i∈ω progressionsi(⊥S)

期望值 progressions單調的,就是說,如果 x≤yprogressions(x)≤progressions(y)。更一般的說,我們期望值

如果 ∀i∈ω xi≤xi+1,則 progressions(∨i∈ω xi) = ∨i∈ω progressions(xi)

最後陳述的 progressions 的性質叫做 ω-連續性。

指稱語義的中心問題是刻畫什麼時候可能依據 Denotes 的等式建立指稱(意義)。計算域理論的基本定理就是如果 progressions 是 ω-連續的,則 Denotes 存在。

progressions 的 ω-連續性得出

progressions(Denotes) = Denotes

上述等式引出了術語 Denotesprogressions不動點

進一步的,這個不動點是 progressions最小不動點

在下節中給出函數式程序的指稱語義作為不動點語義的例子。

階乘函數的例子

編輯

考慮如下定義在所有數上的 factorial 函數:

factorial ≡ λ(n)if (n==0)then 1 else n*factorial(n-1)

factorialgraph 是定義了 factorial 的所有有序對的集合,有序對的第一個元素是參數而第二個元素是值,例如: graph(factorial) = {<n, factorial(n)>|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}factorial 程序的指稱(意義) Denotefactorial 被構造如下:

Denotefactorial = graph(factorial) = ∪i∈ω progressionfactoriali({})

這裏的

progressionfactorial(g) ≡ λ(n)if (n==0)then 1 else n*g(n-1)

注意: progressionfactorial 是不動點算子(參見上節中的定義),它的最小不動點是 Denotefactorial,就是

Denotefactorial = progressionfactorial(Denotefactorial)

還有 progressionfactorial 是 ω-連續的(參見上節中的定義)。

從演員語義得出 Scott 連續性

編輯

演員模型為得出 Dana Scott 的函數的指稱語義(在前面章節關於 factorial 的例子所展示的)提供了基礎,Carl HewittHenry Baker [1977] 首次給出了定理證明:

如果一個演員 f 表現得如同數學函數,則 progressionfScott 連續函數,其最小不動點是

graph(f) = ∪i∈ω progressionfi({})

這裏的

progressionf(G)≡{<x, y>|<x, y>∈graph(f) 和 immediate-descendantsf(<x, y>)⊆G}

Hewitt 和 Baker 的論文在定義 immediate-descendantsf 時的缺陷由 Will Clinger [1981] 修正。

程式語言中的複合性

編輯

程式語言的指稱語義的重要方面是複合性,通過它程序的指稱可以從它的各個部分的指稱來構造。例如,考慮表達式 "<expression1> + <expression2>"。在這種情況下複合性是依據 <expression1><expression2> 的意義而為 "<expression1> + <expression2>" 提供意義。

引用

編輯
  • Irene Greif. Semantics of Communicating Parallel Professes MIT EECS Doctoral Dissertation. August 1975.
  • Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
  • 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. (Quoted by permission of author.)
  • Carl Hewitt (2006a). The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
  • Carl Hewitt (2006b) What is Commitment? Physical, Organizational, and Social頁面存檔備份,存於互聯網檔案館) COIN@AAMAS. 2006.