Reversible computing is motivated by both pragmatic and foundational considerations arising from a variety of disciplines. We take a particular path through the development of reversible computation, emphasizing compositional reversible computation. We start from a historical perspective, by reviewing those approaches that developed reversible extensions of lambda-calculi, Turing machines, and communicating process calculi. These approaches share a common challenge: computations made reversible in this way do not naturally compose locally. We then turn our attention to computational models that eschew the detour via existing irreversible models. Building on an original analysis by Landauer, the insights of Bennett, Fredkin, and Toffoli introduced a fresh approach to reversible computing in which reversibility is elevated to the status of the main design principle. These initial models are expressed using low-level bit manipulations, however. Abstracting from the low-level of the Bennett-Fredkin-Toffoli models and pursuing more intrinsic, typed, and algebraic models, naturally leads to rig categories as the canonical model for compositional reversible programming. The categorical model reveals connections to type isomorphisms, symmetries, permutations, groups, and univalent universes. This, in turn, paves the way for extensions to reversible programming based on monads and arrows. These extensions are shown to recover conventional irreversible programming, a variety of reversible computational effects, and more interestingly both pure (measurement-free) and measurement-based quantum programming.

翻译：可逆计算受到来自多个学科的实际应用和理论基础的双重推动。我们沿着一条特定路径探讨可逆计算的发展，重点关注组合式可逆计算。首先从历史视角出发，回顾那些对λ演算、图灵机和通信进程演算进行可逆扩展的研究方法。这些方法面临一个共同挑战：以此方式实现的可逆计算无法自然地实现局部组合。随后我们将注意力转向那些避免通过现有不可逆模型进行迂回建模的计算模型。基于Landauer的原创性分析，Bennett、Fredkin和Toffoli的见解开创了可逆计算的新范式，其中可逆性被提升为核心设计原则。然而这些初始模型采用低层次的比特操作进行表达。通过从Bennett-Fredkin-Toffoli模型的低层次抽象出发，探索更具本质性、类型化和代数化的模型，自然导向以严格范畴作为组合式可逆编程的规范模型。该范畴模型揭示了与类型同构、对称性、置换、群及单值宇宙的深刻联系。这进而为基于单子与箭头的可逆编程扩展铺平道路。研究证明这些扩展能恢复传统不可逆编程，实现多种可逆计算效应，并更有意义地同时涵盖纯（无测量）和基于测量的量子编程范式。