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

TL;DR

This paper develops a reversible programming language with inductive types, demonstrating its expressivity by encoding Turing machines and establishing a categorical semantics ensuring full completeness.

Contribution

It introduces a Turing-complete reversible language with inductive types and provides a categorical semantics that guarantees expressivity and correctness.

Findings

Encoding of Reversible Turing Machines in the language

Sound and adequate categorical semantics based on join inverse categories

Full completeness result for computable, partial injective functions

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.