This work examines approaches to making computational models reversible. Broadly speaking, transforming a computational model into a reversible one, i.e. reversibilizing it, means extending its operational semantics conservatively in a way that each term of the model is interpretable as a bijection. We recall that the most common strategy to reversibilize a computational model yields operational semantics that halts computations whenever a computational state cannot be uniquely determined from its successor state, thereby allowing terms to be interpreted as partial bijective functions. We are interested in reversible computational models whose terms can be interpreted as total bijective functions. This is essential for studying aspects of computational complexity related to reversible computational models. We introduce SCORE, a language designed for manipulating variables and stacks. Notably, common reversibilization strategies naturally lead to interpreting the functions for stack manipulation as partial bijections. According to our interests, we demonstrate how to interpret SCORE in a state space where, using a proof-assistant, we certify that stack operations are total bijections. It follows that all SCORE terms can be interpreted as total bijections.

翻译：本研究探讨了使计算模型可逆化的方法。广义而言，将计算模型转化为可逆模型（即“可逆化”）意味着以保守方式扩展其操作语义，使得模型的每个项均可解释为双射。我们回顾了可逆化计算模型的最常见策略，该策略产生的操作语义会在计算状态无法从其后续状态唯一确定时终止计算，从而允许将项解释为部分双射函数。我们关注的是其项可解释为完全双射函数的可逆计算模型。这对于研究可逆计算模型相关的计算复杂性方面至关重要。我们提出了SCORE语言，该语言专为操作变量和栈而设计。值得注意的是，常见的可逆化策略自然导致将栈操作函数解释为部分双射。基于我们的研究目标，我们展示了如何在状态空间中解释SCORE，并通过证明辅助工具验证栈操作是完全双射。由此可得，所有SCORE项均可解释为完全双射函数。