Join Inverse Rig Categories for Reversible Functional Programming, and Beyond

TL;DR

This paper introduces join inverse rig categories as a new mathematical framework to model reversible functional programming languages like Rfun, capturing the semantics of reversible computation and unifying various reversible programming models.

Contribution

It defines join inverse rig categories and demonstrates their suitability as categorical models for reversible computing languages such as Rfun, Theseus, and reversible flowcharts.

Findings

Join inverse rig categories effectively model Rfun semantics.

They encompass models for Theseus and reversible flowcharts.

The framework suggests a unified categorical foundation for reversible computing.

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.