演员模型的指称语义

✍ dations ◷ 2025-12-08 15:19:12 #编程语言语义

演员模型的指称语义(Denotational semantics of the Actor model)是演员的指称域理论的研究主题。这个主题的历史发展参见指称语义的历史。

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

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

计算域有下列性质:

由系统 S 指示的数学指称通过构造从叫做 S 的空指称递增更好的逼近来找到 ,使用某个逼近定义函数 progressions(进步)如下这样构造 S 的指称(意义)的 :

期望 progressions 是单调的,就是说,如果 x≤yprogressions(x)≤progressions(y)。更一般的说,我们期望

最后陈述的 progressions 的性质叫做 ω-连续性。

指称语义的中心问题是刻画什么时候可能依据 Denotes 的等式建立指称(意义)。计算域理论的基本定理就是如果 progressions 是 ω-连续的,则 Denotes 存在。

progressions 的 ω-连续性得出

上述等式引出了术语 Denotesprogressions 的不动点。

进一步的,这个不动点是 progressions 的最小不动点。

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

考虑如下定义在所有数上的 factorial 函数:

factorialgraph 是定义了 factorial 的所有有序对的集合,有序对的第一个元素是参数而第二个元素是值,例如: graph(factorial) = {<n, factorial(n)>|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}factorial 程序的指称(意义) Denotefactorial 被构造如下:

这里的

注意: progressionfactorial 是不动点算子(参见上节中的定义),它的最小不动点是 Denotefactorial,就是

还有 progressionfactorial 是 ω-连续的(参见上节中的定义)。

演员模型为得出 Dana Scott 的函数的指称语义(在前面章节关于 factorial 的例子所展示的)提供了基础,Carl Hewitt 和 Henry Baker 首次给出了定理证明:

如果一个演员 f 表现得如同数学函数,则 progressionf 是 Scott 连续函数,其最小不动点是

这里的

Hewitt 和 Baker 的论文在定义 immediate-descendantsf 时的缺陷由 Will Clinger 修正。

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

相关

  • 群马大学群马大学群马大学(ぐんまだいがく、Gunma University)1949年设立的群马县的国立大学法人。校区分为:前桥市荒牧地区(教育学部和社会信息学部所在地)、前桥市昭和地区(医学部所在地
  • 第一哲学沉思集《第一哲学沉思集》(副标题为其中论证上帝的存在和灵魂的不灭)是法国哲学家勒内·笛卡儿所著的一本哲学论文选集,以拉丁语首次出版于1641年。由吕纳公爵(Duc de Luynes)翻译的法
  • 李书章李书章(1954年-),河北阜城人。1971年入伍,第三军医大学硕士研究生学历,主任医师。中国人民解放军中将,现任中央军事委员会后勤保障部副部长。曾任第三军医大学副教务长,1999年,任第三
  • 卫滨区卫滨区(原新华区)是中华人民共和国河南省新乡市的一个市辖区。全区管辖1个镇,7个街道办事处,面积52平方公里,2016年人口23万。邮政编码453000,电话区号0373,行政代码为410703,区政府
  • 磁动势磁动势的标准定义是电流流过导体所产生磁通量的势力(),是用来度量磁场或电磁场的一种量,类似于电场中的电动势或电压。它被描述为线圈所能产生磁通量的势力,这样科学家就能够用它
  • 清软颚擦音清软颚擦音是辅音的一种,用于一些语言当中,它的国际音标符号是⟨x⟩,X-SAMPA符号是⟨x⟩,西班牙语的j、汉语拼音中的h及注音符号的ㄏ,实表此音。古英语本有此发音,但在现代英语中,
  • 蛋椅蛋椅是阿纳·雅各布森在1958年为哥本哈根雷迪森SAS皇家酒店设计的一种椅子,由丹麦家具设计公司弗里茨·汉森生产。 据说这个设计的灵感来源于埃罗·沙里宁的“子宫椅”(Womb c
  • 阿纳托利·伊万诺维奇·鲁萨诺夫阿纳托利·伊万诺维奇·鲁萨诺夫(俄语:Анатолий Иванович Русанов,1932年4月20日-),苏联及俄罗斯化学家。俄罗斯科学院院士。圣彼得堡国立大学教授。俄罗
  • 伊万·霍夫汉内斯·巴格拉米扬伊万·赫里斯托福罗维奇·巴格拉米扬(I)(或称霍夫汉内斯·哈恰图罗维奇·巴格拉米扬,亚美尼亚语:Հովհաննես Խաչատուրի(或者称Քրիստափորի,拉丁化:Chri
  • 武者小路公秀武者小路公秀(1929年-),联合国大学副校长。武者小路公秀于1929年10月21日出生。东京都人。1953年学习院大学政经学部毕业后,曾留学于美国和法国。1962年任学习院大学法学部副教授