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.