Semantics for a Turing-complete Reversible Programming Language with Inductive Types
Kostia Chardonnet, Louis Lemonnier, Benoît Valiron
TL;DR
This work presents a reversible, higher-order language with inductive types, patterned after Theseus, and proves reversible Turing completeness by encoding RTMs as isos. It develops a sound and adequate denotational semantics in a DCPO-enriched join inverse rig category, handling recursion and inductive types via initial algebras. A canonical representation and Bennett-style garbage-removal constructions show that every computable partial injective function is realizable as an iso, establishing a precise correspondence with $\mathbf{PInj}$. The results bridge reversible programming with categorical semantics and demonstrate that reversible languages can capture all computable injective morphisms, with potential implications for energy-efficient and quantum computation models.
Abstract
This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching. We then derive a full completeness result, stating that any computable, partial injective function is the image of a term in the language.