Join Inverse Rig Categories for Reversible Functional Programming, and Beyond
arXiv:2105.09929 · doi:10.4204/EPTCS.351.10
Abstract
Reversible computing is a computational paradigm in which computations are deterministic in both the forward and backward direction, so that programs have well-defined forward and backward semantics. We investigate the formal semantics of the reversible functional programming language Rfun. For this purpose, we introduce join inverse rig categories, the natural marriage of join inverse categories and rig categories, which we show can be used to model the language Rfun, under reasonable assumptions. These categories turn out to be a particularly natural fit for reversible computing as a whole, as they encompass models for other reversible programming languages, notably Theseus and reversible flowcharts. This suggests that join inverse rig categories really are the categorical models of reversible computing.
arXiv commentIn Proceedings MFPS 2021, arXiv:2112.13746
References in corpus (7)
- Restriction categories III: colimits, partial limits, and extensivity
- Complementarity relation for irreversible process derived from stochastic energetics
- A functional quantum programming language
- A categorical foundation for structured reversible flowchart languages: Soundness and adequacy
- Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
- Infinite-Dimensionality in Quantum Foundations: W*-algebras as Presheaves over Matrix Algebras
- DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics