Semantics for a Turing-Complete Reversible Programming Language with Inductive Types

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 and to interpret inductive types and recursion. We then derive a notion of completeness in the sense that any computable, partial, first-order injective function is the image of a term in the language.

Authors

• Kostia Chardonnet
• Louis Lemonnier
• Benoît Valiron

Keywords

• Reversible programming
• functional programming
• Computability
• Denotational Semantics