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.

翻译：Janus是可逆编程语言的典型范例。事实上，Janus程序既可以正向执行也可以反向执行。然而，其现有的小步语义（例如可用于调试或作为并发原语扩展的基础）并非可逆，因为在正向计算过程中会丢失信息。例如，它不满足循环引理——该引理声明任何归约操作都存在逆操作，这是进程演算中可逆性的核心性质，而小步语义在此领域被广泛使用。本文提出了一种新颖的小步语义，该语义在保持与原有语义等价的同时实现了真正的可逆性。这涉及一个非平凡的挑战：为高级编程语言定义基于“程序计数器”的语义。