查看“︁演员模型的指称语义”︁的源代码

{{NoteTA
|G1 = Math
|1=zh-cn:數學對象;zh-tw:數學物件;
}}
'''[[演员模型]]的[[指称语义]]'''（Denotational semantics of the Actor model）是[[演员模型|演员]]的指称[[域理论]]的研究主题。这个主题的历史发展参见[[指称语义的历史]]。

==演员不动点语义==
计算系统语义的指称理论关心找到表示系统作为的[[数学对象]]。这个理论利用了计算数学[[域理论|域]]。这种计算域的例子是偏函数和[[演员模型|演员]]事件图场景。

关系 <tt>x≤y</tt> 意味着 <tt>x</tt> 可以计算演进为 <tt>y</tt>。如果指称是偏序函数，比如 <tt>f≤g</tt> 可以意味着 <tt>f</tt> 一致于 <tt>g</tt> 在 <tt>f</tt> 在其上定义的所有值上。如果指称是[[演员模型|演员]]事件图场景，<tt>x≤y</tt> 意味着满足 <tt>x</tt> 的系统可以演进到满足 <tt>y</tt> 的一个系统。

计算域有下列性质:
#'''底存在'''。域有最小元素指示为 <tt>⊥</tt> 使得对于所有域中元素 <tt>x</tt> 有 <tt>⊥≤x</tt>。
#'''极限存在'''。随着计算继续，指称应当变得更好并有一个极限，使得如果有 <math>\forall i \in \omega</math>   <math>x_i \le x_{i+1}</math>，则[[最小上界]] <math>\vee_{i \in \omega} x_i</math> 应当存在。这个性质叫做 [[序数|ω]]-完全性。
#'''有限元素是可数的'''。一个元素 <tt>x</tt> 是[[紧致元素|有限]]的(在域文献中也叫做孤立的)，当且仅当只要 <tt>A</tt> 是[[有向集合|有向]]的，<tt>∨A</tt> 存在并且 <math>x \le \vee A</math>，就存在 <math>a \in A</math> 有着 <math>x \le a</math>。换句话说，<tt>x</tt> 是有限的，如果必须通过 <tt>x</tt> 来赶上或通过极限过程来超过 <tt>x</tt>。
#'''所有元素都是有限元素的可数递增序列的最小上界'''。在直觉上这意味着所有元素都可以通过在其中所有进步(progression)都是有限的一个计算过程来到达。
#'''域是向下闭合的'''。

由系统 <tt>S</tt> 指示的数学指称通过构造从叫做 <tt>⊥<sub>S</sub></tt> 的空指称递增更好的逼近来找到 ，使用某个逼近定义函数 <tt>'''progression'''<sub>s</sub></tt>(进步)如下这样构造 <tt>S</tt> 的指称(意义)的 [Hewitt 2006b]:
:<tt>'''Denote'''<sub>s</sub> ≡ ∨<sub>i∈ω</sub> '''progression'''<sub>s</sub><sup>i</sup>(⊥<sub>S</sub>)</tt>。

期望 <tt>'''progression'''<sub>s</sub></tt> 是[[单调函数|单调]]的，就是说，如果 <tt>x≤y</tt> 则   <tt>'''progression'''<sub>s</sub>(x)≤'''progression'''<sub>s</sub>(y)</tt>。更一般的说，我们期望
:如果 <tt>∀i∈ω x<sub>i</sub>≤x<sub>i+1</sub></tt>，则 <tt>'''progression'''<sub>s</sub>(∨<sub>i∈ω</sub> x<sub>i</sub>)  = ∨<sub>i∈ω</sub> '''progression'''<sub>s</sub>(x<sub>i</sub>)</tt>
最后陈述的 <tt>'''progression'''<sub>s</sub></tt> 的性质叫做 ω-连续性。

指称语义的中心问题是刻画什么时候可能依据 <tt>'''Denote'''<sub>s</sub></tt> 的等式建立指称(意义)。计算域理论的基本定理就是如果 <tt>'''progression'''<sub>s</sub><tt> 是 ω-连续的，则 <tt>'''Denote'''<sub>s</sub></tt> 存在。

从  <tt>'''progression'''<sub>s</sub></tt> 的 ω-连续性得出
:<tt>'''progression'''<sub>s</sub>('''Denote'''<sub>s</sub>) = '''Denote'''<sub>s</sub></tt>

上述等式引出了术语 <tt>'''Denote'''<sub>s</sub></tt> 是 <tt>'''progression'''<sub>s</sub></tt> 的[[不动点]]。

进一步的，这个不动点是 <tt>'''progression'''<sub>s</sub></tt> 的[[最小不动点]]。

在下节中给出函数式程序的指称语义作为不动点语义的例子。

===阶乘函数的例子===

考虑如下定义在所有数上的 <tt>factorial</tt> 函数:
:<tt>factorial ≡  λ(n)if (n==0)then 1 else n*factorial(n-1)</tt>
<tt>factorial</tt> 的 '''<tt>graph</tt>''' 是定义了 factorial 的所有有序对的集合，有序对的第一个元素是参数而第二个元素是值，例如: <tt>'''graph'''(factorial) = {<n, factorial(n)>|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}</tt>，
<tt>factorial</tt> 程序的指称(意义) <tt>'''Denote'''<sub>factorial</sub></tt> 被构造如下:
:<tt>'''Denote'''<sub>factorial</sub> = '''graph'''(factorial) = ∪<sub>i∈ω</sub> '''progression'''<sub>factorial</sub><sup>i</sup>({})</tt>
这里的
:<tt>'''progression'''<sub>factorial</sub>(g) ≡  λ(n)if (n==0)then 1 else n*g(n-1)</tt>

注意: <tt>'''progression'''<sub>factorial</sub></tt> 是不动点算子(参见上节中的定义)，它的最小不动点是 <tt>'''Denote'''<sub>factorial</sub></tt>，就是
:<tt>'''Denote'''<sub>factorial</sub> = '''progression'''<sub>factorial</sub>('''Denote'''<sub>factorial</sub>)</tt>
还有 <tt>'''progression'''<sub>factorial</sub></tt> 是 ω-连续的(参见上节中的定义)。

===从演员语义得出 Scott 连续性===
[[演员模型]]为得出 [[Dana Scott]] 的函数的指称语义(在前面章节关于 <tt>factorial</tt> 的例子所展示的)提供了基础，[[Carl Hewitt]] 和 [[Henry Baker (computer scientist)|Henry Baker]] [1977] 首次给出了定理证明:

如果一个演员 <tt>f</tt> 表现得如同数学函数，则 <tt>'''progression'''<sub>f</sub></tt> 是 [[Scott连续性|Scott 连续函数]]，其最小不动点是
:<tt>'''graph'''(f) = ∪<sub>i∈ω</sub> '''progression'''<sub>f</sub><sup>i</sup>({})</tt></tt>
这里的
:<tt>'''progression'''<sub>f</sub>(G)≡{<x, y>|<x, y>∈'''graph'''(f) 和 '''immediate-descendants'''<sub>f</sub>(<x, y>)⊆G}</tt>
Hewitt 和 Baker 的论文在定义 <tt>'''immediate-descendants'''<sub>f</sub></tt> 时的缺陷由 Will Clinger [1981] 修正。
===编程语言中的复合性===
{{main|复合性原理}}

编程语言的指称语义的重要方面是复合性，通过它程序的指称可以从它的各个部分的指称来构造。例如，考虑表达式 "<tt><expression<sub>1</sub>> + <expression<sub>2</sub>></tt>"。在这种情况下复合性是依据  <tt><expression<sub>1</sub>></tt> 和 <tt><expression<sub>2</sub>></tt> 的意义而为 "<tt><expression<sub>1</sub>> + <expression<sub>2</sub>></tt>" 提供意义。

==引用==
*Irene Greif.  ''Semantics of Communicating Parallel Professes'' MIT EECS Doctoral Dissertation.  August 1975.
*[[Joe Stoy|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 (computer scientist)|Henry Baker]] ''Actors and Continuous Functionals''  Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1–5, 1977.
*[[Henry Baker (computer scientist)|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]]'' [[Communications of the ACM|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 Science+Business Media|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) [http://www.pcs.usp.br/~coin-aamas06/10_commitment-43_16pages.pdf What is Commitment? Physical, Organizational, and Social] {{Wayback|url=http://www.pcs.usp.br/~coin-aamas06/10_commitment-43_16pages.pdf |date=20210211011938 }}  COIN@AAMAS.  2006.



[[Category:編程語言語義]]