Erlang的可逆性理论
A Theory of Reversibility for Erlang
摘要：
在可逆语言中，任何向前计算都可以通过有限的向后步骤序列来撤销。可逆计算已经在不同的程序设计语言和形式主义的背景下进行了研究，其中它已被用于测试和验证等。在本文中，我们考虑了Erlang的一个子集，Erlang是一种基于角色模型的函数式并发程序设计语言。我们提出了一个形式化的语义可逆计算在这种语言中，并证明其主要性质，包括其因果一致性。我们还在它的基础上构建了一个回滚操作符，可以用来撤消进程到给定检查点的操作。
英文摘要：
In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for testing and verification, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We present a formal semantics for reversible computation in this language and prove its main properties, including its causal consistency. We also build on top of it a rollback operator that can be used to undo the actions of a process up to a given checkpoint.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
