Embracing the Laws of Physics: Three Reversible Models of Computation
Academic Article

Overview

Research

View All

Overview

abstract

Our main models of computation (the Turing Machine and the RAM) make
fundamental assumptions about which primitive operations are realizable. The
consensus is that these include logical operations like conjunction,
disjunction and negation, as well as reading and writing to memory locations.
This perspective conforms to a macro-level view of physics and indeed these
operations are realizable using macro-level devices involving thousands of
electrons. This point of view is however incompatible with quantum mechanics,
or even elementary thermodynamics, as both imply that information is a
conserved quantity of physical processes, and hence of primitive computational
operations.
Our aim is to re-develop foundational computational models that embraces the
principle of conservation of information. We first define what conservation of
information means in a computational setting. We emphasize that computations
must be reversible transformations on data. One can think of data as modeled
using topological spaces and programs as modeled by reversible deformations. We
illustrate this idea using three notions of data. The first assumes
unstructured finite data, i.e., discrete topological spaces. The corresponding
notion of reversible computation is that of permutations. We then consider a
structured notion of data based on the Curry-Howard correspondence; here
reversible deformations, as a programming language for witnessing type
isomorphisms, comes from proof terms for commutative semirings. We then "move
up a level" to treat programs as data. The corresponding notion of reversible
programs equivalences comes from the "higher dimensional" analog to commutative
semirings: symmetric rig groupoids. The coherence laws for these are exactly
the program equivalences we seek.
We conclude with some generalizations inspired by homotopy type theory and
survey directions for further research.