A Structural Approach to Reversible Computation

TL;DR

This paper introduces a structural method to convert high-level functional programs into reversible automata, bridging computation and physics, and providing insights into the logical distinctions between reversible and irreversible computation.

Contribution

It presents a compositional, syntax-directed approach to map functional programs into reversible automata, connecting high-level computation with foundational logical and physical principles.

Findings

Automata size is linear in the functional program size

Provides a concrete model of functional computation

Reveals logical distinctions between reversible and irreversible computation

Abstract

Reversibility is a key issue in the interface between computation and physics, and of growing importance as miniaturization progresses towards its physical limits. Most foundational work on reversible computing to date has focussed on simulations of low-level machine models. By contrast, we develop a more structural approach. We show how high-level functional programs can be mapped compositionally (i.e. in a syntax-directed fashion) into a simple kind of automata which are immediately seen to be reversible. The size of the automaton is linear in the size of the functional term. In mathematical terms, we are building a concrete model of functional computation. This construction stems directly from ideas arising in Geometry of Interaction and Linear Logic---but can be understood without any knowledge of these topics. In fact, it serves as an excellent introduction to them. At the same time, an interesting logical delineation between reversible and irreversible forms of computation emerges from our analysis.