A Reversible Semantics for Janus

TL;DR

This paper introduces a new small-step semantics for the Janus reversible programming language that is genuinely reversible, addressing the information loss in previous semantics and enabling true backward execution.

Contribution

It presents a novel reversible small-step semantics for Janus, incorporating a program counter to maintain reversibility at a high level.

Findings

The new semantics satisfies the Loop Lemma, ensuring true reversibility.

It remains equivalent to the previous semantics in behavior.

The approach involves a non-trivial design of semantics based on a program counter.

Abstract

Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current small-step semantics (useful, e.g., for debugging or as a basis for extensions with concurrency primitives) is not reversible, since it loses information while computing forwards. E.g., it does not satisfy the Loop Lemma, stating that any reduction has an inverse, a main property of reversibility in process calculi, where a small-step semantics is commonly used. We present here a novel small-step semantics which is actually reversible, while remaining equivalent to the previous one. It involves the non-trivial challenge of defining a semantics based on a "program counter" for a high-level programming language.