演员模型理论

从角色的定义便可看出，发生的事件很多，如：本地决策、创建角色、发送消息、接收消息以及对下条信息如何回应发出指令。

然而，本文只关注那些已发送给角色并收到的信息。

这篇文章的研究结果发表在休伊特（Hewitt ）[2006]上。

可数定律，事件是可以被计数的。

1.1 激活排序

激活顺序(-≈→)是对激活其他事件的事件进行排序的建模。(从一个事件传递到它激活的事件，这一信息传递中必须要有能量流)。

• 由于能量的传递，激活排序是相对不变的；也即，对于所有事件 e1.e2，如果 e1 -≈→ e2，那么在所有观察者的相对论参照系中，e1 早于 e2 。
• 激活排序的严格因果定律：在任何情况下e -≈→ e。
• 激活排序中的有限预分解定律： 对于所有事件 e1 ，集合 {e|e -≈→ e1} 是有限的。

1.2 到达排序

角色x（ -x→ )模型的到达排序模拟了消息到达x的事件(总)顺序。到达排序由处理消息的仲裁决定(通常使用称为仲裁器的数字电路)。角色的到达排序就在它的世界线上。到达排序意味着角色模型本身具有不确定性。

• 因为角色x到达排序的所有事件都发生于世界线x，所以角色的到达排序相对不变。即，对于所有参与者x和事件 e1.e2，如果e1 -x→ e2，那么在所有观察者的相对论参照系中，e1早于e2。
• 到达的有限预分配定律：对于所有事件e1和参与者x，集合 {e|e -x→ e1} 是有限的。

1.3 组合排序

组合排序(用 →表示)是所有角色激活排序和到达排序的传递闭包。

• 组合排序相对不变，这是由于它的传递闭包相对不变。即，对于所有事件 e1.e2，如果 e1→e2，那么在所有观察者的相对论参照系中，e1早于e2。
• 组合排序的严格因果定律：因为没有事件e→e。

根据定义，组合排序显然是可传递的。

据推测，上述定律可能包含以下内容：

组合排序中事件之间的有限链定律：组合排序→中两个事件之间没有无限链(即线性有序集)事件。

1.4 组合排序中事件间有限链定律的独立性

然而，出乎意料的是[克林格(Clinger 1981)]证明了组合排序中事件之间的有限链定律独立于以前的定律，即：

定理：组合排序中事件之间的有限链定律并不遵循前面所述的定律。

证据：这足以表明存在一个满足前述定律但违反组合排序中事件间有限链定律的角色计算。

考虑这样一种计算，当一个角色 Initial 被发送一个" Start"消息，导致它采取以下操作时，

1. 计算开始创建一个新的角色Greeter₁，该Greeter₁将被发送一条消息 "SayHelloTo"，地址是 "Greeter₁”；
2. 用Greeter₁的地址发送Initial 消息“Again”；

此后，当收到地址为“ Greeter₁”的“ Again”消息时， Initial 的行为如下(我们将称之为事件 Again_i):

1. 创建一个新的角色Greeter₁，它会被发送一条消息SayHelloTo ，地址是Greeter_i；
2. 用Greeter_i+1的地址发送Initial消息"Again"；

显然， Initial发送" Again"消息的计算永远不会终止。

每个角色 Greeter_i 的行为如下:

• 当它收到一条地址为“Greeter_i-1”的“SayHelloTo ”信息(我们称之为“SayHelloTo_i”事件)，它会向“Greeter_i-1”发送一条“Hello”信息；
• 当它收到“Hello”消息(我们称之为“Hello_i”事件)时，它什么也不做；

现在有可能是 Hello_i - Greeter_i→ SayHelloTo_i，因此 Hello_i→ SayHelloTo_i。

同时 Again_i -≈→ Again_i+1，因此 Again_i → Again_i+1。

此外，在联合排序的严格因果关系法之前陈述的所有法律都得到满足。

但是， Again₁和 SayHelloTo₁之间的组合排序中可能有无限多的事件，如下所示:

Again1→...→Againi→......→Helloi→SayHelloToi→...→Hello1→SayHelloTo1

然而，我们从物理学中得知，无限的能量不能沿着有限的轨道消耗。因此，由于角色模型是以物理为基础的，联合排序中事件之间的有限链法则被认为是角色模型的公理。

1.5 离散定律

组合排序中事件之间的有限链定律与以下定律密切相关:

离散定律: 对于所有事件 e1和 e2，集合 {e|e1→e→e2} 是有限的。

事实上，前两个定律已经被证明是等价的:

定理[克莱格（Clinger）1981]。离散定律等同于组合排序中事件之间的有限链定律(不使用选择公理)。

离散性定律排除了芝诺（Zeon）机器，并与Petri网的结果相关。[贝斯特（Best）等人，1984，1987]。

离散定律意味着无界非确定性的性质。组合排序被克莱格(Clinger 1981)用于构建角色指称模型。

克莱格 Clinger [1981]使用上述角色事件模型构建了使用权力领域的角色构建指称模型。随后休伊特[Hewitt 2006]用到达时间扩充了图表，以构建一个在技术上更简单、更容易理解的指称模型。