Categorical Semantics of Reversible Pattern-Matching
This work addresses a foundational issue in reversible computation for theoretical computer science, but it is incremental as it builds on existing categorical frameworks.
The paper tackled the problem of modeling reversible pattern-matching in categorical semantics by identifying that join inverse rig categories are insufficient and deriving a new categorical structure to adequately capture it, based on the Theseus language.
This paper is concerned with categorical structures for reversible computation. In particular, we focus on a typed, functional reversible language based on Theseus. We discuss how join inverse rig categories do not in general capture pattern-matching, the core construct Theseus uses to enforce reversibility. We then derive a categorical structure to add to join inverse rig categories in order to capture pattern-matching. We show how such a structure makes an adequate model for reversible pattern-matching.