2025/01/09 by Palazzo, Matteo, Roversi, Luca
#Computational Complexity (cs.CC) #D.3.1 #F.3.2 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.2501.05259
This work focuses on making certain computational models reversible. We start with the idea that "reversibilizing" should mean a process that gives a computational model an operational semantics capable of interpreting each term as a bijection. The most commonly used method of reversibilization creates operational semantics that halt computation when it is not possible to uniquely determine the starting state from a produced computational state; thus, terms are interpreted as partial bijective functions. We introduce \textsfS-CORE, a language of terms that allows manipulation of variables and stacks. For \textsfS-CORE, we define the operational semantics \textsfR-semantics. With the help of a proof assistant, we certify that \textsfR-semantics makes \textsfS-CORE a reversible imperative computational model where all terms are interpreted as total bijections on an appropriate state space.