Categorical Semantics of Reversible Pattern-Matching
arXiv:2109.05837 · doi:10.4204/EPTCS.351.2
Abstract
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.
arXiv commentIn Proceedings MFPS 2021, arXiv:2112.13746
References in corpus (7)
- Synthesis and Optimization of Reversible Circuits - A Survey
- Restriction categories III: colimits, partial limits, and extensivity
- Reversible effects as inverse arrows
- Reversible monadic computing
- Condition/Decision Duality and the Internal Logic of Extensive Restriction Categories
- Inversion, Iteration, and the Art of Dual Wielding
- Join Inverse Rig Categories for Reversible Functional Programming, and Beyond