带栈的可逆计算与“故障的可逆管理”

本文研究了使计算模型可逆的方法。广义上讲，将计算模型转换为可逆模型，即对其进行可逆化，意味着以保守的方式扩展其操作语义，使得模型中的每个项都可解释为一个双射。我们回顾了最常见的可逆化计算模型的策略，该策略产生的操作语义会在计算状态无法从其后续状态唯一确定时停止计算，从而允许项被解释为部分双射函数。我们感兴趣的是其项可被解释为全双射函数的可逆计算模型。这对于研究与可逆计算模型相关的计算复杂性方面至关重要。我们引入了SCORE，一种用于操作变量和栈的语言。值得注意的是，常见的可逆化策略自然会导致将栈操作函数解释为部分双射。根据我们的兴趣，我们展示了如何在状态空间中解释SCORE，在该状态空间中，使用证明助手，我们验证了栈操作是全双射。由此可知，所有SCORE项都可以解释为全双射。