Janus is a paradigmatic example of reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its 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 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程序既可正向执行，也可反向执行。然而，其小步语义（例如用于调试或作为并发原语扩展的基础）并非可逆，因为在正向计算过程中会丢失信息。例如，它不满足"循环引理"——该引理声明任何规约都存在逆规约，这是进程演算中可逆性的核心性质，而小步语义在进程演算中被广泛使用。本文提出了一种真正可逆的新型小步语义，同时保持与原有语义的等价性。这涉及为高级编程语言定义基于"程序计数器"的语义这一非平凡挑战。