Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compositional Reversible Computation

Jacques Carette, Chris Heunen, Robin Kaarsgaard, Amr Sabry

TL;DR

The paper addresses the challenge of making computation reversible in a way that composes modularly rather than only globally or via ad hoc history-tracking. It develops a principled, algebraic framework based on dagger and rig categories, culminating in the canonical term model $\Pi$ and the LR-construction to show how irreversible computation can be recovered from reversible foundations, including both classical and quantum settings. It shows how monads and arrows extend reversibility to effects, with a dagger Frobenius condition ensuring compatibility of reversal with effects, and demonstrates a three-stage LR factorization that echoes the fundamental theorem of reversible computation. In the quantum domain, the Hilbert-space model and Stinespring-style information hiding extend the classical results to open systems and measurement, providing a unified semantic toolkit for reversible and irreversible programming and quantum programming alike.

Abstract

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.

Compositional Reversible Computation

TL;DR

The paper addresses the challenge of making computation reversible in a way that composes modularly rather than only globally or via ad hoc history-tracking. It develops a principled, algebraic framework based on dagger and rig categories, culminating in the canonical term model and the LR-construction to show how irreversible computation can be recovered from reversible foundations, including both classical and quantum settings. It shows how monads and arrows extend reversibility to effects, with a dagger Frobenius condition ensuring compatibility of reversal with effects, and demonstrates a three-stage LR factorization that echoes the fundamental theorem of reversible computation. In the quantum domain, the Hilbert-space model and Stinespring-style information hiding extend the classical results to open systems and measurement, providing a unified semantic toolkit for reversible and irreversible programming and quantum programming alike.

Abstract

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.
Paper Structure (21 sections, 1 theorem, 15 equations, 4 figures)

This paper contains 21 sections, 1 theorem, 15 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Reversibility from Global Histories
  3. Reversibility from Local Histories
  4. Bennett's Trick
  5. Reversibility as a Local Phenomenon
  6. Rig Groupoids
  7. Dagger Categories and Groupoids
  8. Monoidal Categories and Rig Categories
  9. The Canonical Term Model $\Pi$
  10. Finite Sets and Permutations
  11. Curry-Howard
  12. Reversible and Irreversible Effects
  13. Frobenius Monads and Reversible Arrows
  14. The Fundamental Theorem of Reversible Computation
  15. Quantum Effects
  16. ...and 6 more sections

Key Result

theorem thmcountertheorem

The set consisting of just the Toffoli and Hadamard gates is computationally universal for quantum computing. By computationally universal, we mean that the set can simulate, to within $\epsilon$-error, an arbitrary quantum circuit of $n$ qubits and $t$ gates with only poly-logarithmic overhead in $

Figures (4)

  • Figure 1: Bennett's construction of a standard reversible 3-tape Turing machine, starting from an arbitrary Turing machine instrumented to record its history on a dedicated tape.
  • Figure 2: An overly simple 2-tape Turing machine that "looks" like it operationally does the same as Bennett's construction.
  • Figure 3: $\Pi$ syntax
  • Figure 4: Types for $\Pi$ combinators

Theorems & Definitions (1)

  • theorem thmcountertheorem