Reversible Computation with Stacks and "Reversible Management of Failures"

TL;DR

This paper introduces SCORE, a language for reversible computation with stacks, and demonstrates how to interpret its operations as total bijections, enabling reversible models suitable for complexity analysis.

Contribution

The paper presents a novel reversible programming language, SCORE, with a method to interpret stack operations as total bijections, advancing reversible computation research.

Findings

SCORE allows reversible manipulation of variables and stacks.

Stack operations in SCORE can be certified as total bijections.

Reversible models in SCORE facilitate complexity analysis.

Abstract

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.