为可逆编程语言Janus设计了可逆的细粒度语义，保留正向计算信息。
A Reversible Semantics for Janus
- 基于程序计数器构建可逆小步语义，解决原语义丢失信息问题
- 新语义满足环路引理，实现正向与反向执行的严格对应
- 适用于需要可逆性的调试与并发扩展场景
Janus 是一种典型的可逆编程语言，其程序可正向与反向执行。然而，其现有的小步语义在正向计算过程中会丢失信息，不满足过程演算中可逆性的重要性质——环路引理（Loop Lemma），即任意还原步骤都存在逆步骤。本文提出一种新的小步语义，实现了真正的可逆性，同时保持与原语义等价。该语义通过引入程序计数器机制，为高层编程语言构造可逆细粒度行为，解决了高阶语言中可逆语义设计的关键挑战。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。