fbpx
维基百科

演员模型的指称语义

演员模型指称语义(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 Hewitt 和 Henry 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.

演员模型的指称语义, denotational, semantics, actor, model, 是演员的指称域理论的研究主题, 这个主题的历史发展参见指称语义的历史, 目录, 演员不动点语义, 阶乘函数的例子, 从演员语义得出, scott, 连续性, 编程语言中的复合性, 引用演员不动点语义, 编辑计算系统语义的指称理论关心找到表示系统作为的数学对象, 这个理论利用了计算数学域, 这种计算域的例子是偏函数和演员事件图场景, 关系, 意味着, 可以计算演进为, 如果指称是偏序函数, 比如, 可以意味着, 一致于. 演员模型的指称语义 Denotational semantics of the Actor model 是演员的指称域理论的研究主题 这个主题的历史发展参见指称语义的历史 目录 1 演员不动点语义 1 1 阶乘函数的例子 1 2 从演员语义得出 Scott 连续性 1 3 编程语言中的复合性 2 引用演员不动点语义 编辑计算系统语义的指称理论关心找到表示系统作为的数学对象 这个理论利用了计算数学域 这种计算域的例子是偏函数和演员事件图场景 关系 x y 意味着 x 可以计算演进为 y 如果指称是偏序函数 比如 f g 可以意味着 f 一致于 g 在 f 在其上定义的所有值上 如果指称是演员事件图场景 x y 意味着满足 x 的系统可以演进到满足 y 的一个系统 计算域有下列性质 底存在 域有最小元素指示为 使得对于所有域中元素 x 有 x 极限存在 随着计算继续 指称应当变得更好并有一个极限 使得如果有 i w displaystyle forall i in omega nbsp x i x i 1 displaystyle x i leq x i 1 nbsp 则最小上界 i w x i displaystyle vee i in omega x i nbsp 应当存在 这个性质叫做 w 完全性 有限元素是可数的 一个元素 x 是有限的 在域文献中也叫做孤立的 当且仅当只要 A 是有向的 A 存在并且 x A displaystyle x leq vee A nbsp 就存在 a A displaystyle a in A nbsp 有着 x a displaystyle x leq a nbsp 换句话说 x 是有限的 如果必须通过 x 来赶上或通过极限过程来超过 x 所有元素都是有限元素的可数递增序列的最小上界 在直觉上这意味着所有元素都可以通过在其中所有进步 progression 都是有限的一个计算过程来到达 域是向下闭合的 由系统 S 指示的数学指称通过构造从叫做 S 的空指称递增更好的逼近来找到 使用某个逼近定义函数 progressions 进步 如下这样构造 S 的指称 意义 的 Hewitt 2006b Denotes i w progressionsi S 期望 progressions 是单调的 就是说 如果 x y 则 progressions x progressions y 更一般的说 我们期望 如果 i w xi xi 1 则 progressions i w xi i w progressions xi 最后陈述的 progressions 的性质叫做 w 连续性 指称语义的中心问题是刻画什么时候可能依据 Denotes 的等式建立指称 意义 计算域理论的基本定理就是如果 progressions是 w 连续的 则 Denotes 存在 从 progressions 的 w 连续性得出progressions Denotes Denotes上述等式引出了术语 Denotes 是 progressions 的不动点 进一步的 这个不动点是 progressions 的最小不动点 在下节中给出函数式程序的指称语义作为不动点语义的例子 阶乘函数的例子 编辑考虑如下定义在所有数上的 factorial 函数 factorial l n if n 0 then 1 else n factorial n 1 factorial 的 graph 是定义了 factorial 的所有有序对的集合 有序对的第一个元素是参数而第二个元素是值 例如 graph factorial lt n factorial n gt n w lt 0 1 gt lt 1 1 gt lt 2 2 gt lt 3 6 gt lt 4 24 gt factorial 程序的指称 意义 Denotefactorial 被构造如下 Denotefactorial graph factorial i w progressionfactoriali 这里的progressionfactorial g l n if n 0 then 1 else n g n 1 注意 progressionfactorial 是不动点算子 参见上节中的定义 它的最小不动点是 Denotefactorial 就是Denotefactorial progressionfactorial Denotefactorial 还有 progressionfactorial 是 w 连续的 参见上节中的定义 从演员语义得出 Scott 连续性 编辑演员模型为得出 Dana Scott 的函数的指称语义 在前面章节关于 factorial 的例子所展示的 提供了基础 Carl Hewitt 和 Henry Baker 1977 首次给出了定理证明 如果一个演员 f 表现得如同数学函数 则 progressionf 是 Scott 连续函数 其最小不动点是graph f i w progressionfi 这里的progressionf G lt x y gt lt x y gt graph f 和 immediate descendantsf lt x y gt G Hewitt 和 Baker 的论文在定义 immediate descendantsf 时的缺陷由 Will Clinger 1981 修正 编程语言中的复合性 编辑主条目 复合性原理编程语言的指称语义的重要方面是复合性 通过它程序的指称可以从它的各个部分的指称来构造 例如 考虑表达式 lt expression1 gt lt expression2 gt 在这种情况下复合性是依据 lt expression1 gt 和 lt expression2 gt 的意义而为 lt expression1 gt lt expression2 gt 提供意义 引用 编辑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 取自 https zh wikipedia org w index php title 演员模型的指称语义 amp oldid 69600509, 维基百科,wiki,书籍,书籍,图书馆,

文章

,阅读,下载,免费,免费下载,mp3,视频,mp4,3gp, jpg,jpeg,gif,png,图片,音乐,歌曲,电影,书籍,游戏,游戏。