使用Redex建模Actor：第三部分
内容提要
本文介绍使用PLT Redex建模Actor系统时，通过减少不可观察的非确定性来提高效率。作者将内部计算与通信效果分离，合并发送和投递规则，并采用贪婪归约，使示例程序的评估时间从1015毫秒降至2毫秒，状态数从74减至13。最终模型更简洁，能更真实地反映Actor的观察能力，但要求Actor不发散。
延伸解读
性能提升的关键：减少不可观察的非确定性
本文通过将内部计算与通信效果分离、合并发送和投递规则，以及采用贪婪归约，大幅减少了模型中的不可观察非确定性。这使得示例程序的评估时间从1015毫秒降至2毫秒，状态数从74减至13。这种优化不仅提升了效率，还使生成的轨迹更简洁、更易读，更贴近Actor系统的实际观察能力。
模型适用性的重要前提：非发散Actor
作者强调，这种优化方法要求所有Actor都是非发散的，即每个Actor在有限步内要么产生最终值，要么执行效果（如send、receive等）。如果存在发散Actor，Redex会因无限归约而卡住。对于需要处理发散Actor的场景，作者建议采用限制步数等临时方案，但会引入虚假的交错。因此，该方法适用于大多数实际建模需求，但需注意这一前提。
从细粒度到粗粒度：权衡与选择
文章展示了从细粒度模型（74个状态）到粗粒度模型（13个状态）的逐步优化过程。每一步都通过减少不可观察的交错来简化模型，但同时也牺牲了对某些细节的建模能力。作者指出，这种权衡是合理的，因为Actor系统本身只能观察到部分事件顺序。最终模型保留了相关的非确定性，同时大幅提升了效率，为处理更大规模示例提供了可能。
Q&A
在Redex建模Actor时，如何减少不可观察的非确定性以提高效率？
通过将内部计算与通信效果分离，合并发送和投递规则，并采用贪婪归约，可以减少不可观察的非确定性。具体包括：将配置队列改为单位置缓冲区，将ISWIM内部归约嵌入到外部通信规则中，以及将发送和投递合并为一步。
为什么在Actor模型中，某些交错是无法被观察的？
因为Actor只能观察到消息到达的顺序，而无法区分消息在网络上传输的中间步骤。例如，两个消息同时发送时，接收者只能看到先到后到的顺序，而无法知道发送和投递的具体交错方式。
在Redex中，如何将内部归约嵌入到外部通信规则中？
通过定义一个内部归约关系（ISWIM+Actors-inner-red），并使用apply-reduction-relation*函数在外部规则中贪婪地应用内部归约，直到无法继续归约为止。这样，外部规则一步就可以完成所有内部计算。
为什么这种方法只适用于非发散的程序？
因为如果Actor发散（即内部归约无限进行），apply-reduction-relation*会无限循环，导致Redex无法终止。因此，需要保证每个Actor最终都会进行效果操作或终止，才能使用这种贪婪归约。
在最终模型中，发送和投递是如何合并的？
发送规则直接将消息广播到所有Actor的邮箱中，通过deliver元函数将消息放入匹配的Actor邮箱，从而消除了单独的投递步骤和配置中的消息队列。
通过优化，示例程序的评估时间从多少降低到多少？
从1015毫秒降低到2毫秒，速度提升约500倍。
最终模型相比初始模型，状态数和路径长度有何变化？
状态数从74个减少到13个，路径长度从15步减少到6步。
