Non-Cartesian Guarded Recursion with Daggers
Louis Lemonnier
TL;DR
This work extends guarded recursion beyond cartesian settings by constructing a guarded model from any category with a terminal object and enriching it over the topos of trees ${\mathbf S}$. It then integrates this guarded construction with dagger rig categories to model higher-order reversible programming with symmetric pattern-matching, showing that a substantial subcategory preserves the dagger and rig structures necessary for reversibility. The framework provides guarded fixed points and inductive type interpretation in a non-cartesian context, with concrete semantics for ground, first-order, and higher-order terms, including quantum-control scenarios. While streams pose a challenge in dagger settings, the authors outline how guarded recursion can nonetheless support reversible computation and expressiveness for higher-order reversible languages, and they identify promising directions for further work on internal logics and quantum-effects integration.
Abstract
Guarded recursion is a framework allowing for a formalisation of streams in classical programming languages. The latter take their semantics in cartesian closed categories. However, some programming paradigms do not take their semantics in a cartesian setting; this is the case for concurrency, reversible and quantum programming for example. In this paper, we focus on reversible programming through its categorical model in dagger categories, which are categories that contain an involutive operator on morphisms. After presenting classical guarded recursion, we show how to introduce this framework into dagger categories with sufficient structure for data types, also called dagger rig categories. First, given an arbitrary category, we build another category shown to be suitable for guarded recursion in multiple ways, via enrichment and fixed point theorems. We then study the interaction between this construction and the structure of dagger rig categories, aiming for reversible programming. Finally, we show that our construction is suitable as a model of higher-order reversible programming languages, such as symmetric pattern-matching.