演员模型的指称语义

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

## 演員不動點語義

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

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

計算域有下列性質:

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

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

　
: **Denote**s ≡ ∨i∈ω **progression**si(⊥S)。

期望 **progression**s 是單調的，就是說，如果 x≤y 則 **progression**s(x)≤**progression**s(y)。更一般的說，我們期望

　
: 如果 ∀i∈ω xi≤xi+1，則 **progression**s(∨i∈ω xi) = ∨i∈ω **progression**s(xi)

最後陳述的 **progression**s 的性質叫做 ω- 連續性。

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

從 **progression**s 的 ω- 連續性得出

　
: **progression**s(**Denote**s) = **Denote**s

上述等式引出了術語 **Denote**s 是 **progression**s 的不動點。

進一步的，這個不動點是 **progression**s 的最小不動點。

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

### 階乘函數的例子

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

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

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

　
: **Denote**factorial = **graph**(factorial) = ∪i∈ω **progression**factoriali({})

這裡的

　
: **progression**factorial(g) ≡ λ(n)if (n==0)then 1 else n\*g(n-1)

注意: **progression**factorial 是不動點算子 (參見上節中的定義)，它的最小不動點是 **Denote**factorial，就是

　
: **Denote**factorial = **progression**factorial(**Denote**factorial)

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

### 從演員語義得出 Scott 連續性

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

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

　
: **graph**(f) = ∪i∈ω **progression**fi({})

這裡的

　
: **progression**f(G)≡{<x, y>|<x, y>∈**graph**(f) 和 **immediate-descendants**f(<x, y>)⊆G}

Hewitt 和 Baker 的論文在定義 **immediate-descendants**f 時的缺陷由 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.