Erlang 语言的可逆性理论

在可逆语言中，任何前向计算都可由有限步后向步骤撤销。可逆计算已在多种编程语言与形式化方法中被研究，并用于测试与验证等。本文中，我们考虑 Erlang（一种基于 actor 模型的函数式并发编程语言）的一个子集。我们给出该语言中可逆计算的的形式语义，并证明其包括因果一致性在内的主要性质。我们还在此基础上构建了一个回滚算子，可用于将某进程的动作撤销至给定检查点。