Join Inverse Categories as Models of Reversible Recursion

Abstract

Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modelling reversible functional programming, notably morphism schemes for reversible recursion, a $\dagger$-trace, and algebraic $\omega$-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Reversible computing, that is, the study of computations that exhibit both forward and backward determinism, originally grew out of the thermodynamics of computation. Landauer’s principle states that computations performed by some physical system (thermodynamically) dissipate heat when information is erased, but that no dissipation is entailed by information-preserving computations [28]. This has motivated a long study of diverse reversible computation models, such as logic circuits [15], Turing machines [4, 6], and many forms of restricted automata models [27, 31]. Reversibility concepts are important in quantum computing, but are increasingly seen to be of interest in other areas as well, including high-performance computing [33], process calculi [13], and even robotics [34, 35].

In this paper we concern ourselves with the categorical underpinnings of functional reversible programming languages. At the programming language level, reversible languages exhibit interesting program properties, such as easy program inversion [40]. Now, most reversible languages are stateful, giving them a fairly straightforward semantics interpretation. While functional programs are usually easier to reason about at the meta-level, they do not have the concept of state that imperative languages do, making their semantics interesting objects of study.

Further, many reversible functional programming languages (such as Theseus [25] and the $\varPi$-family of combinator calculi [7]) come equipped with a tacit assumption of totality, a property that is neither required [4] nor necessarily desirable as far as guaranteeing reversibility is concerned. Shedding ourselves of the “tyranny of totality,” however, requires us to handle partiality explicitly as additional categorical structure.

One approach which does precisely that is inverse categories, as studied by Cockett & Lack [9] as a specialization of restriction categories, which have recently been suggested and developed by Giles [16] as models of reversible (functional) programming. In this paper, we will argue that assuming ever slightly more structure on these inverse categories, namely the presence of countable joins of parallel morphisms [17], gives rise to a number of additional properties useful for modelling reversible functional programming, notably two different notions of reversible recursion, and an account of recursive data types (via algebraic $\omega$-compactness with respect to structure-preserving functors), which are not present in the general case. This is done by adopting two different, but complementary, views on inverse categories with countable joins as enriched categories – as $\mathbf {CPO}$-categories, and as (specifically $\varSigma \mathbf {Mon}$-enriched) strong unique decomposition categories [18, 23].

Overview. The necessary background on restriction and inverse categories is presented in Sect. 2. In Sect. 3 we show that inverse categories with countable joins are $\mathbf {CPO}$-enriched, which allows us to demonstrate the existence of (reversible!) fixed points of both morphism schemes and structure-preserving functors. In Sect. 4 we show that inverse categories with countable joins and a join-preserving disjointness tensor are unique decomposition categories equipped with a uniform $\dagger$-trace. Sect. 5 gives conclusions and directions for future work.

2 Background

This section gives an introduction to restriction and inverse categories (with joins), dagger categories, and categories of partial maps as they will be used in the remainder of this text. Unless otherwise stated, the material described in this section can be found in standard texts on restriction and inverse category theory (e.g., Cockett & Lack [9–11], Giles [16], Guo [17]).

We begin by recalling the definition of restriction structures and restriction categories.

Definition 1

(Cockett & Lack, 2002). A restriction structure on a category consists of an operator $\overline{(\cdot )}$ on morphisms mapping each morphism $f : A \rightarrow B$ to a morphism $\overline{f} : A \rightarrow A$ (the restriction idempotent of f) such that

• (i) $f \circ \overline{f} = f$ for all morphisms $f : A \rightarrow B$,

• (ii) $\overline{f} \circ \overline{g} = \overline{g} \circ \overline{f}$ whenever $\text {dom}(f) = \text {dom}(g)$,

• (iii) $\overline{f \circ \overline{g}} = \overline{f} \circ \overline{g}$ whenever $\text {dom}(f) = \text {dom}(g)$, and

• (iv) $\overline{h} \circ f = \overline{h \circ f} \circ f$ whenever $\text {cod}(f) = \text {dom}(h)$.

A category with a restriction structure is called a restriction category.

As a trivial example, any category can be equipped with a restriction structure given by setting $\overline{f} = 1_A$ for every morphism $f : A \rightarrow B$. However, there are also many useful and nontrivial examples of restriction categories (see, e.g., Cockett & Lack [9, Sect. 2.1.3]), the canonical one being the category $\mathbf {Pfn}$ of sets and partial functions. In this category, the restriction idempotent $\overline{f} : A \rightarrow A$ for a partial function $f : A \rightarrow B$ is given by the partial identity function

$$\begin{aligned} \overline{f}(x) = \left\{ \begin{array}{l l} x &{} \text {if}~f~\text {is defined at}~x\text {,} \\ \text {undefined} &{} \text {otherwise.} \end{array}\right. \end{aligned}$$

Since we take restrictions as additional structure, we naturally want a notion of functors that preserve this structure.

Definition 2

A functor $F : \mathscr {C} \rightarrow \mathscr {D}$ between restriction categories $\mathscr {C}$ and $\mathscr {D}$ is a restriction functor if $\overline{F(f)} = F(\overline{f})$ for all morphisms f of $\mathscr {C}$.

A morphism $f : A \rightarrow B$ of a restriction category is said to be total if $\overline{f} = 1_A$. Given a restriction category $\mathscr {C}$, we can form the category $\mathrm {Total}(\mathscr {C})$, consisting of all objects and only the total morphisms of $\mathscr {C}$, which embeds in $\mathscr {C}$ via a faithful restriction functor. Further, a restriction category in which every restriction idempotent splits is called a split restriction category, and, by way of the Karoubi envelope, every restriction category $\mathscr {C}$ can be embedded in a split restriction category $\mathrm {Split}(\mathscr {C})$ via a fully faithful restriction functor. Restriction categories with restriction functors form a category, $\mathbf {rCat}$.

A useful feature of restriction categories, and one we will exploit throughout this article, is that hom-sets can be equipped with a partial order (often called the natural partial order), defined as follows:

Proposition 1

In a restriction category $\mathscr {C}$, every hom-set ${\mathrm{Hom}_\mathscr {C}}(A,B)$ can be equipped with the structure of a partial order where we let $f \le g$ iff $g \circ \overline{f} = f$. Further, every restriction functor F is locally monotone on this order, in the sense that $f \le g$ implies $F(f) \le F(g)$.

In $\mathbf {Pfn}$, this corresponds to the usual partial order on partial functions: For $f,g : A \rightarrow B$, $f \le g$ if, for all $x \in A$, f is defined at x implies that g is defined at x and $f(x) = g(x)$.

A natural question to ask is when this partial order has a least element: A sufficient condition for this is when the restriction category has a restriction zero.

Definition 3

A restriction category $\mathscr {C}$ has a restriction zero object 0 iff for all objects A and B, there exists a unique morphism $0_{A,B} : A \rightarrow B$ that factors through 0 and satisfies $\overline{0_{A,A}} = 0_{A,A}$.

If such a restriction zero object exists, it is unique up to (total) isomorphism. When a given restriction category has such a restriction zero, the zero map $0_{A,B} : A \rightarrow B$ is precisely the least element of $\mathrm{{Hom}_\mathscr {C}}(A,B)$.

Moving on to inverse categories, in order to define these we first need the notion of a partial isomorphism:

Definition 4

In a restriction category $\mathscr {C}$, we say that a morphism $f : A \rightarrow B$ is a partial isomorphism if there exists a unique morphism $f^\circ : B \rightarrow A$ of $\mathscr {C}$ (the partial inverse of f) such that $f^\circ \circ f = \overline{f}$ and $f \circ f^\circ = \overline{f^\circ }$.

Definition 5

A restriction category $\mathscr {C}$ is said to be an inverse category if all morphisms of $\mathscr {C}$ are partial isomorphisms.

In this manner, if we accept an intuition of restriction categories as “categories with partiality,” inverse categories are “groupoids with partiality” – and, indeed, the category $\mathbf {PInj}$ of sets and partial injective functions is the canonical example of an inverse category. In fact, the Wagner-Preston representation theorem (see, e.g., Lawson [29]) for inverse monoids can be extended to show that every locally small inverse category can be faithfully embedded in $\mathbf {PInj}$ (see Heunen [21] for the general case, or Cockett & Lack [9] for the special case of small categories).

The analogy with groupoids goes even further; similar to how we can construct a groupoid $\text {Core}(\mathscr {C})$ by taking only the isomorphisms of $\mathscr {C}$, every restriction category $\mathscr {C}$ has a subcategory $\text {Inv}(\mathscr {C})$ that is an inverse category, and has as morphisms only the partial isomorphisms of $\mathscr {C}$. Inverse categories with restriction functors form a category, $\mathbf {invCat}$.

More generally, inverse categories are dagger categories (sometimes also called categories with involution):

Definition 6

A category $\mathscr {C}$ is said to be a dagger category if it is equipped with a contravariant endofunctor $(-)^{\dagger } : \mathscr {C} \rightarrow \mathscr {C}^\mathrm{{op}}$ such that $1_A^\dagger = 1_A$ for all objects A, and $f^{\dagger \dagger } = f$ for all morphisms f.

Proposition 2

Every inverse category $\mathscr {C}$ is a dagger category with the dagger functor given by $A^\dagger = A$ on objects, and $f^\dagger = f^\circ$ on morphisms.

As is conventional, we will call $f^\dagger$ the adjoint of f, and say that f is self-adjoint if $f = f^\dagger$, and unitary if $f^\dagger = f^{-1}$. In inverse categories, unitary morphisms thus correspond precisely to (total) isomorphisms. For the remainder of this text, we will use this induced dagger-structure when refering to the partial inverse of a morphism (and write, e.g., $f^\dagger$ rather than $f^\circ$).

A useful feature of this definition of inverse categories is that we do not need an additional notion of an “inverse functor” as a functor that preserves partial inverses; restriction functors suffice.

Definition 7

A functor $F : \mathscr {C} \rightarrow \mathscr {D}$ between dagger categories is a dagger preserving if $F(f)^\dagger = F(f^\dagger )$ for all morphisms f of $\mathscr {C}$.

Proposition 3

Every restriction functor $F : \mathscr {C} \rightarrow \mathscr {D}$ between inverse categories $\mathscr {C}$ and $\mathscr {D}$ is dagger preserving.

That this holds can be seen from the fact that the property of being a partial isomorphism is defined purely in terms of composition and restriction idempotents, both of which are preserved by restriction functors.

2.1 Joins and Compatibility

Given that hom-sets of restriction (and, by extension, inverse) categories are partially ordered, one may wonder when this partial order has joins. It turns out, however, that it does not in the general case, and that only very simple restriction categories have joins for arbitrary parallel morphisms. However, we can define a meaningful notion of joins for parallel morphisms if this operation is not required to be total, but only be defined for compatible morphisms. For restriction categories, this compatibility relation is defined as follows:

Definition 8

Parallel morphisms $f, g : A \rightarrow B$ of a restriction category $\mathscr {C}$ are said to be restriction compatible if $g \circ \overline{f} = f \circ \overline{g}$; if this is the case, we write $f \smile g$. By extension, a set $S \subseteq {\mathrm{Hom}_\mathscr {C}}(A,B)$ is restriction compatible if all morphisms of S are pairwise restriction compatible.

This compatibility relation can be extended to apply to inverse categories by requiring that morphisms be compatible in both directions:

Definition 9

Parallel morphisms $f, g : A \rightarrow B$ of an inverse category $\mathscr {C}$ are said to be inverse compatible if $f \smile g$ and $f^\dagger \smile g^\dagger$; if this is the case, we write $f \asymp g$ . A set $S \subseteq \mathrm{{Hom}_\mathscr {C}}(A,B)$ is inverse compatible if all morphisms of S are pairwise inverse compatible.

The familiar reader will notice that this definition differs in its statement from Guo’s [17, p. 98], who defined $f \asymp g$ in an inverse category $\mathscr {C}$ if $f \smile g$ holds in both $\mathscr {C}$ and $\mathscr {C}^\mathrm{{op}}$ (relying on the observation that inverse categories are simultaneously restriction categories and corestriction categories). To avoid working explicitly with corestriction categories, however, we will use this equivalent definition instead.

We define restriction categories with (countable) joins as follows:

Definition 10

(Guo, 2012). A restriction category $\mathscr {C}$ is a (countable) join restriction category if it has a restriction zero object, and satisfies that for all (countable) restriction compatible subsets S of all hom sets $\mathrm{{Hom}_\mathscr {C}}(A,B)$, there exists a morphism $\bigvee _{s \in S} s$ such that

• (i) $s \le \bigvee _{s \in S} s$ for all $s \in S$, and $s \le t$ for all $s \in S$ implies $\bigvee _{s \in S} s \le t$;

• (ii) $\overline{\bigvee _{s \in S} s} = \bigvee _{s \in S} \overline{s}$;

• (iii) $f \circ \left( \bigvee _{s \in S} s \right) = \bigvee _{s \in S}(f \circ s)$ for all $f : B \rightarrow X$; and

• (iv) $\left( \bigvee _{s \in S} s \right) \circ g = \bigvee _{s \in S}(s \circ g)$ for all $g : Y \rightarrow A$.

In addition, we say that a restriction functor that preserves all thus constructed joins is a join restriction functor.

As a concrete example, $\mathbf {Pfn}$ has joins of all restriction compatible sets; here, $f \smile g$ iff whenever f and g are both defined at some point x, $f(x) = g(x)$, and the join of a set of restriction compatible partial functions F is given by

$$\begin{aligned} \left( \bigvee _{f \in F} f\right) (x) = \left\{ \begin{array}{l l} f'(x) &{} \!\!\!\! \text {if there exists an}~f' \in F~\text {such that}~f'~\text {is defined at}~x, \\ \text {undefined} &{} \text {otherwise.} \end{array}\right. \end{aligned}$$

Notice that the compatibility relation ensures precisely that the result is a partial function.

This, finally, allows us to define join inverse categories by narrowing the definition above to only require the existence of joins of inverse compatible (sets of) morphisms:

Definition 11

An inverse category $\mathscr {C}$ is a (countable) join inverse category if it has a restriction zero object, and Definition 10 is satisfied for all (countable) inverse compatible subsets S of all $\mathrm{{Hom}_\mathscr {C}}(A,B)$.

Analogously to $\mathbf {Pfn}$, the category $\mathbf {PInj}$ is a join inverse category with joins given precisely as in $\mathbf {Pfn}$, since the additional requirement that $f^\dagger \smile g^\dagger$ ensures that the resulting partial function is injective.

2.2 Categories of Partial Maps

Categories of partial maps provide a synthetic approach to partiality in a categorical setting, and was first introduced by Robinson and Rosolini [32] in 1988. To form a category of partial maps, we consider a stable system of monics: In a category $\mathscr {C}$, a collection $\mathcal {M}$ of monics of $\mathscr {C}$ is said to be a stable system of monics if it contains all isomorphisms of $\mathscr {C}$ and is closed under composition and pullbacks (in the sense that the pullback $m'$ of an $m : X \rightarrow B$ in $\mathcal {M}$ along any $f : A \rightarrow B$ exists and $m' \in \mathcal {M}$). Given such a stable system of monics $\mathcal {M}$ in a category $\mathscr {C}$, we can form the category of partial maps as follows:

Proposition 4

Given a category $\mathscr {C}$ and a stable system of monics $\mathcal {M}$ of $\mathscr {C}$, we form the category of partial maps $\mathrm {Par}(\mathscr {C},\mathcal {M})$ by choosing the objects to be the objects of $\mathscr {C}$, and placing a morphism $(m,f) : A \rightarrow B$ for every pair (m, f) where $m : A' \rightarrow A \in \mathcal {M}$ and $f : A' \rightarrow B$ is a morphism of $\mathscr {C}$, as in

factored out by the equivalence relation $\cdot \sim \cdot$ in which $(m,f) \sim (m',f')$ if there exists an isomorphism $\alpha : A' \rightarrow A''$ such that $m' \circ \alpha = m$ and $f' \circ \alpha = f$. Composition of morphisms $(m,f) : A \rightarrow B$ and $(m',g) : B \rightarrow C$ is given by $(m \circ m'', g \circ f') : A \rightarrow C$ where $m''$ and $f'$ arise from the pullback

where $m'' \circ m \in \mathcal {M}$ precisely by $\mathcal {M}$ closed under composition and pullbacks.

Categories of partial maps are prime examples of restriction categories; in fact, of split restriction categories. Further, it can be shown that every restriction category $\mathscr {C}$ embeds fully and faithfully and in a restriction preserving manner into a category of partial maps [9].

3 As CPO-categories

In the present section, we will show that inverse categories with countable joins are intrinsically $\mathbf {CPO}$-enriched. This observation leads to two properties that are highly useful for modelling reversible functional programming, namely the existence of fixed points for both morphism schemes for recursion (that is, continuous endomorphisms on hom-objects) and for locally continuous functors. The former can be applied to model reversible recursive functions, and the latter to model recursive data types [3]. Further, we will show that the partial inverse of the fixed point of a morphism scheme for recursion can be computed as the fixed point of an adjoint morphism scheme, giving a style of recursion similar to the reversible functional programming language rfun [39].

Recall that a category $\mathscr {C}$ is $\mathbf {CPO}$-enriched (or simply a $\mathbf {CPO}$-category) if all $\mathrm{{Hom}_\mathscr {C}}(A,B)$ are pointed $\omega$-complete partial orders (i.e., they have a least element and satisfy that each $\omega$-chain has a supremum), and composition is monotone, continuous and strict. To begin, we will need the lemma below.

Lemma 1

Let $\mathscr {C}$ be an inverse category and $f,g : A \rightarrow B$ be parallel morphisms of $\mathscr {C}$. If $f \le g$ then $f \asymp g$.

This lemma allows us to show $\mathbf {CPO}$-enrichment of join inverse categories:

Theorem 1

Every inverse category $\mathscr {C}$ with countable joins is $\mathbf {CPO}$-enriched.

Proof

Let A, B be objects of $\mathscr {C}$, and let $\{f_i\}_{i \in \omega }$ be an $\omega$-chain in $\mathrm{{Hom}_\mathscr {C}}(A,B)$ with respect to the canonical partial ordering. By Lemma 1, all $f_i$ and $f_j$ for $i,j \in \omega$ of this chain are inverse compatible, so the set $F = \{f_i \mid i \in \omega \}$ is an inverse compatible subset of $\mathrm{{Hom}_\mathscr {C}}(A,B)$. But then we can form the supremum of $\{f_i\}_{i \in \omega }$ by

$$\begin{aligned} \sup \{f_i\}_{i \in \omega } = \bigvee _{f \in F} f \end{aligned}$$

which is the supremum of this chain directly by definition of the join.

Let $f,g : A \rightarrow B$ and $F = \{f_i \mid i \in \omega \}$. Monotony of compositions holds in all restriction categories, not just inverse categories with countable joins: Supposing $f \le g$ then $g \circ \overline{f} = f$, and for $h : B \rightarrow X$,

$$\begin{aligned} h \circ g \circ \overline{h \circ f} = h \circ g \circ \overline{h \circ g \circ \overline{f}} = h \circ g \circ \overline{h \circ g} \circ \overline{f} = h \circ g \circ \overline{f} = h \circ f \end{aligned}$$

so $h \circ f \le h \circ g$ in $\mathrm {Hom}_\mathscr {C}(A,X)$; the argument is analogous for postcomposition. That composition is continuous follows directly by definition of joins, as we have

$$\begin{aligned} h \circ \sup \{f_i\}_{i \in \omega } = h \circ \bigvee _{f \in F} f = \bigvee _{f \in F} (h \circ f) = \sup \{h \circ f_i\}_{i \in \omega } \end{aligned}$$

for all $h : B \rightarrow X$, and analogously for postcomposition. That composition is strict follows by the fact that the zero map $0_{A,B} : A \rightarrow B$ is least in $\mathrm{{Hom}_\mathscr {C}}(A,B)$, and that $g \circ 0_{A,B} = 0_{A,X}$ for all $g : B \rightarrow X$ by the universal mapping property of the zero object, and likewise for postcomposition.    $\square$

Recall that a functor $F : \mathscr {C} \rightarrow \mathscr {D}$ between $\mathbf {CPO}$-categories is locally continuous iff each $F_{A,B} : \mathrm{{Hom}_\mathscr {C}}(A,B) \rightarrow \mathrm {Hom}_\mathscr {D}(FA,FB)$ is monotone and continuous. Note that since all restriction functors preserve the partial order on hom-sets, and since suprema are defined in terms of joins, join restriction functors are in particular locally continuous.

3.1 Reversible Fixed Points of Morphism Schemes

In the following, let $\mathscr {C}$ be an inverse category with countable joins. We will use the term morphism scheme to refer to a monotone and continuous function $f : \mathrm{{Hom}_\mathscr {C}}(A,B) \rightarrow \mathrm {Hom}_\mathscr {C}(X,Y)$ – note that such schemes are morphisms of $\mathbf {CPO}$ and not of the inverse category $\mathscr {C}$, so they are specifically not required to have inverses. Enrichment in $\mathbf {CPO}$ then has the following immediate corollary by Kleene’s fixed point theorem:

Corollary 1

Every morphism scheme of the form $\mathrm{{Hom}_\mathscr {C}}(A,B) \xrightarrow {f} \mathrm{{Hom}_\mathscr {C}}(A,B)$ has a least fixed point $\text {fix}~f : A \rightarrow B$ in $\mathscr {C}$.

Proof

Define $\text {fix}~f = \sup \{f^n(0_{A,B})\}$; that this is the least fixed point follows by Kleene’s fixed point theorem, as $0_{A,B}$ is least in $\mathrm{{Hom}_\mathscr {C}}(A,B)$.    $\square$

Morphism schemes on their own are useful for modelling parametrized reversible functions, i.e., functions that take other functions given at compile-time as parameters to produce new, first-order reversible functions. Since higher-order reversible functional programming is yet to be well-understood, parametrized functions (as implemented in, e.g., Theseus [25]) allow for a higher degree of abstraction and code reuse, as we know it from higher-order functional irreversible programming. With this in mind, recursive reversible functions can be seen as least fixed points of self-parametrized functions.

Given that we can thus model reversible recursive functions via least fixed points of morphism schemes, a prudent question to ask is if the inverse of a least fixed point can be computed as the least fixed point of another morphism scheme. We will answer this in the affirmative, but to do this, we need to show that the induced dagger functor is locally continuous.

Lemma 2

The canonical dagger functor $\dagger : \mathscr {C}^\mathrm{{op}} \rightarrow \mathscr {C}$ is locally continuous.

Proof

Let $f,g : A \rightarrow B$. For monotony, suppose $f \le g$, i.e., $g \circ \overline{f} = f$. Then

$$\begin{aligned} g^\dagger \circ \overline{f^\dagger }&= g^\dagger \circ f \circ f^\dagger = g^\dagger \circ g \circ \overline{f} \circ f^\dagger = \overline{g} \circ \overline{f} \circ f^\dagger = \overline{g \circ \overline{f}} \circ f^\dagger \\&= \overline{f} \circ f^\dagger = f^\dagger \circ f \circ f^\dagger = f^\dagger \circ \overline{f^\dagger } = f^\dagger \end{aligned}$$

so $f^\dagger \le g^\dagger$ as well, as desired. For continuity, let $\{f_i\}_{i \in \omega }$ be an $\omega$-chain in $\mathrm{{Hom}_\mathscr {C}}(A,B)$, and let $F = \{f_i \mid i \in \omega \}$ be the corresponding set for this chain. Since $f \le \bigvee _{f \in F} f$ for each $f \in F$ by Definition 11, we have $f^\dagger \le \left( \bigvee _{f \in F} f\right) ^\dagger$ for all $f \in F$ by monotony of $\dagger$, and so

$$\begin{aligned} \sup \{f_i^\dagger \}_{i \in \omega } = \bigvee _{f \in F} f^\dagger \quad \le \quad \left( \bigvee _{f \in F} f\right) ^\dagger = \sup \{f_i\}^\dagger _{i \in \omega } \end{aligned}$$

by Definition 11. In the other direction, we have $f^\dagger \le \bigvee _{f \in F} f^\dagger$ for all $f \in F$ by Definition 11, so by monotony of $\dagger$, $f = f^{\dagger \dagger } \le \left( \bigvee _{f \in F} f^\dagger \right) ^\dagger$ for all $f \in F$. But then $\bigvee _{f \in F} f \le \left( \bigvee _{f \in F} f^\dagger \right) ^\dagger$ by Definition 11, and so by monotony of $\dagger$, we finally get

$$\begin{aligned} \sup \{f_i\}^\dagger _{i \in \omega } = \left( \bigvee _{f \in F} f\right) ^\dagger \quad \le \quad \left( \bigvee _{f \in F} f^\dagger \right) ^{\dagger \dagger } = \bigvee _{f \in F} f^\dagger = \sup \{f_i^\dagger \}_{i \in \omega } \end{aligned}$$

as desired.    $\square$

With this lemma, we are able to show that the inverse of a least fixed point of a morphism scheme can be computed as the least fixed point of an adjoint morphism scheme:

Theorem 2

Every morphism scheme of the form $\mathrm{{Hom}_\mathscr {C}}(A,B) \xrightarrow {f} \mathrm{{Hom}_\mathscr {C}}(A,B)$ has an adjoint morphism scheme $\mathrm {Hom}_\mathscr {C}(B,A) \xrightarrow {f_\ddagger } \mathrm {Hom}_\mathscr {C}(B,A)$ such that $(\text {fix}~f)^\dagger = \text {fix}~f_\ddagger$.

Proof

Let $\iota _{A,B} : \mathrm{{Hom}_\mathscr {C}}(A,B) \rightarrow \mathrm {Hom}_\mathscr {C}(B,A)$ denote the family of functions defined by $\iota _{A,B}(f) = f^\dagger$; each of these are monotone and continuous by Lemma 2, and an isomorphism (with inverse $\iota _{B,A}$) by $f^{\dagger \dagger } = f$. Given a morphism scheme $f : \mathrm{{Hom}_\mathscr {C}}(A,B) \rightarrow \mathrm{{Hom}_\mathscr {C}}(A,B)$, we define $f_\ddagger = \iota _{A,B} \circ f \circ \iota _{B,A}$ – this is monotone and continuous since it is a (monotone and continuous) composition of monotone and continuous functions. But since

$$\begin{aligned} f_\ddagger ^n = (\iota _{A,B} \circ f \circ \iota _{B,A})^n = \iota _{A,B} \circ f^n \circ \iota _{B,A} \end{aligned}$$

by $\iota _{B,A}$ an isomorphism with inverse $\iota _{A,B}$, and since $0_{A,B}^\dagger = 0_{B,A}$ by the universal mapping property of the zero object, we get

$$\begin{aligned} \text {fix}~f_\ddagger&= \sup \{f_\ddagger ^n(0_{B,A})\} = \sup \{(\iota _{A,B} \circ f^n \circ \iota _{B,A})(0_{B,A})\} = \sup \{f^n(0_{B,A}^\dagger )^\dagger \} \\&= \sup \{f^n(0_{A,B})^\dagger \} = \sup \{f^n(0_{A,B})\}^\dagger = (\text {fix}~f)^\dagger \end{aligned}$$

as desired.   $\square$

In modelling recursion in reversible functional programming, this theorem states precisely that the partial inverse of a recursive reversible functions is, itself, a recursive reversible function, and that it can be obtained by inverting the function body and replacing recursive calls with recursive calls to the thus constructed inverse: Coincidentally, this is precisely the inverse semantics of recursive reversible functions in rfun [39].

3.2 Algebraic $\omega$-compactness for Free!

A pleasant property of $\mathbf {CPO}$-categories is that algebraic $\omega$-compactness – the property that every locally continuous functor has a canonical fixed point – is relatively easy to check for, thanks to the fixed point theorem due to Adámek [3] and Barr [5]:

Theorem 3

(Adámek & Barr). Let $\mathscr {C}$ be a $\mathbf {CPO}$-category with an initial object. If $\mathscr {C}$ has colimits of $\omega$-sequences of embeddings, then $\mathscr {C}$ is algebraically $\omega$-compact over $\mathbf {CPO}$.

Canonical fixed points of functors are of particular interest in modelling functional programming, since they can be used to provide interpretations for recursive data types. In the following, we will couple this theorem with a join-completion theorem for restriction categories to show that every inverse category can be faithfully embedded in an algebraically $\omega$-compact inverse category with joins. That this succeeds rests on the following lemmas:

Lemma 3

If an inverse category $\mathscr {C}$ embeds faithfully in a restriction category $\mathscr {D}$, it also embeds faithfully in Inv $(\mathscr {D})$.

Proof

We notice that $\text{ Inv }: \mathbf {rCat} \rightarrow \mathbf {invCat}$ is right adjoint to the forgetful functor $U : {\mathbf {invCat} \rightarrow \mathbf {rCat}}$, with each component of the counit $\epsilon : U \circ \text{ Inv }\rightarrow 1_\mathbf {rCat}$ given by the faithful inclusion functor $\epsilon _\mathscr {C} : U(\text {Inv}(\mathscr {C})) \rightarrow \mathscr {C}$ (that this is an adjunction follows by an argument entirely analogous to $\text {Core}: \mathbf {Cat} \rightarrow \mathbf {Grpd}$ being right adjoint to $U : \mathbf {Grpd} \rightarrow \mathbf {Cat}$). That faithful restriction functors are preserved follows readily since restriction functors preserve partial isomorphisms, and every restriction functor out of an inverse category factors through Inv-inclusion by this adjunction.    $\square$

Lemma 4

The functor Inv $: \mathbf {rCat} \rightarrow \mathbf {invCat}$ takes join restriction categories to join inverse categories (and preserves join restriction functors).

The latter of these lemmas was shown by Guo [17, Lemma 3.1.27]. To ease presentation of the completion theorem for join restriction categories due to Cockett and Guo [8, 17], we make the following notational shorthand:

Convention 12

For a restriction category $\mathscr {C}$, let $\overline{\mathscr {C}}$ denote the category of pre-sheaves $\mathbf {Set}^\mathrm{{Total}(\mathrm {Split}(\mathscr {C}))^\mathrm{{op}}}$.

Note in particular that $\overline{\mathscr {C}}$ is cocomplete and all colimits are stable under pullback (since colimits in $\overline{\mathscr {C}}$ are constructed object-wise in $\mathbf {Set}$).

Theorem 4

(Cockett & Guo). Every restriction category $\mathscr {C}$ can be faithfully embedded in a join restriction category of the form $\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}})$.

The stable system of monics $\widehat{\mathcal {M}_{\text {gap}}}$ relates to the join-completion for restriction categories via $\mathcal {M}$-gaps (see Cockett [8] or Guo [17, Sect. 3.2.2] for details). We can now show the algebraic $\omega$-compactness theorem for restriction categories:

Theorem 5

If $\mathscr {C}$ is a restriction category then $\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}})$ is algebraically $\omega$-compact for $\mathbf {CPO}$; so for join restriction functors.

Proof

Let $\mathscr {C}$ be a restriction category. By Theorem 4, $\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}})$ is join restriction category. By Adámek & Barr’s fixed point theorem and the fact that join restriction categories are $\mathbf {CPO}$-enriched (by Theorem 1) and have a restriction zero object (which is specifically initial) by definition, it suffices to show that $\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}})$ has colimits of $\omega$-diagrams of embeddings. Let $D : \omega \rightarrow \mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}})$ be such a diagram of embeddings. This corresponds to the diagram

in $\overline{\mathscr {C}}$. Since $\overline{\mathscr {C}}$ is cocomplete, this diagram has a colimiting cocone $\alpha : D \Rightarrow \text {colim}~D$ such that

commutes. Further, since colimits in $\overline{\mathscr {C}}$ are constructed object-wise in $\mathbf {Set}$, this colimit is stable under pullbacks, so composition in $\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}})$, corresponding to pullbacks in $\overline{\mathscr {C}}$, commutes with this colimit. Thus, the family of morphisms $\{(m_i, \alpha _{D(i+1)} \circ f_i)\}_{i \in \omega }$ is a colimiting cocone for D in $\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}})$.    $\square$

Finally, using this machinery, we can show how this theorem extends to inverse categories.

Corollary 2

Every inverse category can be faithfully embedded in a join inverse category that is algebraically $\omega$-compact for join restriction functors.

Proof

Let $\mathscr {C}$ be an inverse category. Since $U(\mathscr {C})$ is the exact same category viewed as a restriction category, $U(\mathscr {C})$ embeds faithfully in $\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}})$, which is a join restriction category by Theorem 4, and algebraically $\omega$-compact by Theorem 5. But then it follows by Lemma 3 that $\mathscr {C}$ embeds faithfully in $\text {Inv}(\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}}))$, which is a join inverse category by Lemma 4, and is algebraically $\omega$-compact for join restriction functors (which are specifically locally monotone and continuous) since fixed points of functors are (total) isomorphisms, so preserved in $\text {Inv}(\mathrm {Par}(\overline{\mathscr {C}}, \widehat{\mathcal {M}_{\text {gap}}}))$.    $\square$

4 As Unique Decomposition Categories

A complementary view on inverse categories with countable joins is as unique decomposition categories, a kind of category introduced by Haghverdi [18] equipped with a partial sum operation on Hom-sets via enrichment in the category of $\varSigma$-monoids (shown to be symmetric monoidal by Hoshino [23]). Unique decomposition categories (including Hoshino’s strong unique decomposition categories [23] which we will employ here) are specifically traced monoidal categories [26] if they satisfy certain conditions. This is desirable when modelling functional programming, as traces can be used to model notions of feedback [1] and recursion [19, 20, 24].

Here, we will show that inverse categories with countable joins and a join-preserving disjointness tensor (due to Giles [16]) are strong unique decomposition categories, and satisfy the conditions required to be equipped with a trace. We extend this result further to show that the trace is a $\dagger$-trace [37], and thus has pleasant inversion properties (the trace in $\mathbf {PInj}$ is well studied, cf. [2, 18, 22]). This is particularly interesting given that the reversible programming language Theseus [25] and the combinator calculus $\varPi ^0$ [7] both rely on a $\dagger$-trace for reversible recursion.

We begin with the definition of a $\varSigma$-monoid [18] (see also Manes & Benson [30] where these are described as positive partial monoids):

Definition 13

A $\varSigma$ -monoid $(M, \varSigma )$ consists of a nonempty set M and a partial operator $\varSigma$ defined on countable families in M (say that a family $\{x_i\}_{i \in I}$ is summable if $\sum _{i \in I} x_i$ is defined) such that

• (i) if $\{x_i\}_{i \in I}$ is a countable family in M and $\{I_j\}_{j \in J}$ is a countable partitioning of I, then $\{x_i\}_{i \in I}$ is summable iff all $\{x_i\}_{i \in I_j}$ and $\sum _{i \in I_j} x_i$ are summable for all $j \in J$, and in this case

  $$\begin{aligned} \sum _{j \in J} \sum _{i \in I_j} x_i = \sum _{i \in I} x_i \,, \end{aligned}$$

• (ii) any family $\{x_i\}_{i \in I}$ in M where I is singleton is summable with $\sum _{i \in I} x_i = x_j$ if $I = \{j\}$.

The class of $\varSigma$-monoids with homomorphisms preserving partial sums forms a category, $\varSigma \mathbf {Mon}$. As such, a category $\mathscr {C}$ is enriched in $\varSigma \mathbf {Mon}$ if all hom-sets of $\mathscr {C}$ are $\varSigma$-monoids, and composition distributes over partial addition.

Lemma 5

Every inverse category with countable joins is $\varSigma \mathbf {Mon}$-enriched.

Proof

(Sketch). In an inverse category $\mathscr {C}$, defining

$$\begin{aligned} \sum _{i \in I} s_i = \bigvee _{s \in \{s_i \mid i \in I\}} s \end{aligned}$$

for a countable family $\{s_i\}_{i \in I}$ of some hom-set $\mathrm{{Hom}_\mathscr {C}}(A,B)$, summability coincides with inverse compatibility. That the axioms of $\varSigma$-monoids are satisfied follows straightforwardly by Definition 11.    $\square$

Haghverdi defines unique decomposition categories in the following way:

Definition 14

(Haghverdi). A unique decomposition category $\mathscr {C}$ is a symmetric monoidal category enriched in $\varSigma \mathbf {Mon}$ such that for all finite index sets I and all $j \in I$, there are quasi-injections $\iota _j : X_j \rightarrow {\oplus }_{i \in I} X_i$ and quasi-projections $\rho _j : {\oplus }_{i \in I} X_i \rightarrow X_j$ satisfying

• (i) $\rho _k \circ \iota _j = 1_{X_k}$ if $j=k$, and $0_{X_j, X_k}$ otherwise, and

• (ii) $\varSigma _{i \in I} \iota _i \circ \rho _i = 1_{{\oplus }_{i \in I} x X_i}$.

This definition is strengthened by Hoshino:

Definition 15

(Hoshino). A strong unique decomposition category is a symmetric monoidal category enriched in $\varSigma \mathbf {Mon}$ satisfying that the identity on the monoidal unit I is $0_{I,I}$, and $1_X \oplus 0_{Y,Y} + 0_{X,X} \oplus 1_Y = 1_{X \oplus Y}$ for all X and Y.

An elementary result is that strong unique decomposition categories are unique decomposition categories, with their quasi injections and projections given by $\iota _1 = (1_A \oplus 0_{0,B}) \circ u_r^{-1} : A \rightarrow A \oplus B$ and $\rho _1 = u_r \circ (1_A \oplus 0_{B,0}) : A \oplus B \rightarrow A$, and analogously for $\iota _2$ and $\rho _2$ (thus extending to any finite index set).

As such, (strong) unique decomposition categories rely on a sum-like monoidal tensor – in the context of inverse categories, such a one can be found in Giles’ definition of a disjointness tensor [16, Definition 7.2.1].

Definition 16

(Giles). An inverse category $\mathscr {C}$ with a restriction zero object 0 is said to have a disjointness tensor if it is equipped with a symmetric monoidal restriction functor $- \oplus - : \mathscr {C} \times \mathscr {C} \rightarrow \mathscr {C}$ such that

• (i) the restriction zero 0 is the tensor unit, and

• (ii) the morphisms given by $\amalg _1 = (1_A \oplus 0_{0,B}) \circ u_r^{-1} : A \rightarrow A \oplus B$ and ${\amalg _2 = (0_{0,B} \oplus 1_A) \circ u_l^{-1} : A \rightarrow B \oplus A}$ are jointly epic, and their partial inverses $\amalg _1^\dagger : A \oplus B \rightarrow A$ and $\amalg _2^\dagger : B \oplus A \rightarrow A$ are jointly monic,

where $u_l : 0 \oplus A \rightarrow A$ and $u_r : A \oplus 0 \rightarrow A$ denote the left respectively the right unitor of the symmetric monoidal tensor.

Though not required from this definition, since we are working exclusively with join inverse categories, we make the additional assumption that the disjointness tensor is a join restriction functor. Since Giles’ definition already demands that the zero object be the monoidal unit, and even defines $\amalg _i$ precisely like Hoshino’s definition of $\iota _i$ (one can similarly see that $\amalg _i^\dagger = \rho _i$), we can show the following:

Theorem 6

Every inverse category with countable joins and a join-preserving disjointness tensor is a strong unique decomposition category.

Proof

By Lemma 5, any inverse category with countable joins (and a join-preserving disjointness tensor) is enriched in $\varSigma \mathbf {Mon}$, so it suffices to show that the (specifically symmetric monoidal) disjointness tensor satisfies Definition 15. That $1_{I,I} = 0_{I,I}$ follows by $1_{0,0} = 0_{0,0}$ for the (restriction) zero 0, and $1_X \oplus 0_{Y,Y} + 0_{X,X} \oplus 1_Y = 1_{X \oplus Y}$ by the definition of partial sums as joins and the additional requirement that the disjointness tensor preserves joins.    $\square$

Due to the $\varSigma \mathbf {Mon}$-enrichment on unique decomposition categories, the trace can be constructed as a denumerable sum of morphisms, provided that morphisms of a certain form are always summable, cf. [18, Proposition 4.0.11] and [23, Corollary 5.4]:

Theorem 7

(Haghverdi, Hoshino). Let $\mathscr {C}$ be a (strong) unique decomposition category such that for every X, Y, and U and every $f : X \oplus U \rightarrow Y \oplus U$, the sum $f_{11} + \sum _{n=0}^\infty f_{21} \circ f^n_{22} \circ f_{12}$ exists, where $f_{ij} = \rho _j \circ f \circ \iota _i$. Then $\mathscr {C}$ has a uniform trace given by

$$\begin{aligned} \text {Tr}^U_{X,Y}(f) = f_{11} + \sum _{n=0}^\infty f_{21} \circ f^n_{22} \circ f_{12}\,. \end{aligned}$$

In a join inverse category, we say that parallel morphisms $f, g : A \rightarrow B$ are inverse disjoint if $\overline{f} \circ \overline{g} = 0_{A,A}$ and $\overline{f^\dagger } \circ \overline{g^\dagger } = 0_{B,B}$.

Lemma 6

In an inverse category, the following hold:

• (i) All inverse disjoint morphisms are inverse compatible,

• (ii) $g \smile g'$ and $f \smile f'$ implies $g \circ f \smile g' \circ f'$ when $\text {dom}(g) = \text {cod}(f)$, and

• (iii) $\overline{g \circ f} = \overline{g \circ f} \circ \overline{f}$ when $\text {dom}(g) = \text {cod}(f)$.

This lemma allows us to show the existence of all trace sums: The core idea is to use part (ii) of this lemma until we get morphisms that are immediately disjoint by (iii), so inverse compatible by (i).

Lemma 7

In a join inverse category with a disjointness tensor, all morphisms of the forms $f_{11}$ or $f_{21} \circ f^n_{22} \circ f_{12}$ for any $n \in \mathbb {N}$ and some $f : X \oplus U \rightarrow Y \oplus U$ are pairwise inverse compatible.

Recall that a $\dagger$-category with a trace is said to have a $\dagger$ -trace (see, e.g., Selinger [37]) if $\text {Tr}^U_{X,Y}(f)^\dagger = \text {Tr}^U_{Y,X}(f^\dagger )$ for every morphism $f : X \oplus U \rightarrow Y \oplus U$.

Theorem 8

Every inverse category $\mathscr {C}$ with countable joins and a join-preserving disjointness tensor has a uniform $\dagger$-trace.

Proof

By Theorem 6, $\mathscr {C}$ is a (strong) unique decomposition category, and by Lemma 7 it has all trace sums, so it follows that $\mathscr {C}$ has a uniform trace. To see that this is a $\dagger$-trace, let $f : X \oplus U \rightarrow Y \oplus U$ be a morphism of $\mathscr {C}$. We notice that

$$\begin{aligned} (f_{ij})^\dagger = (\rho _j \circ f \circ \iota _i)^\dagger = (\amalg _j^\dagger \circ f \circ \amalg _i)^\dagger = \amalg _i^\dagger \circ f^\dagger \circ \amalg _j^{\dagger \dagger } = \amalg _i^\dagger \circ f^\dagger \circ \amalg _j = (f^\dagger )_{ji} \end{aligned}$$

and so $(f_{11})^\dagger = (f^\dagger )_{11}$ and

$$\begin{aligned} (f_{21} \circ f_{22}^n \circ f_{12})^\dagger = (f_{12})^\dagger \circ (f_{22}^n)^\dagger \circ (f_{21})^\dagger = (f^\dagger )_{21} \circ (f^\dagger _{22})^n \circ (f^\dagger )_{12} \end{aligned}$$

which gives us

$$\begin{aligned} \text {Tr}^U_{X,Y}(f)^\dagger&= \left( f_{11} + \sum _{n \in \omega } f_{21} \circ f_{22}^n \circ f_{12}\right) ^\dagger = \left( f_{11} \vee \bigvee _{n \in \omega } f_{21} \circ f_{22}^n \circ f_{12}\right) ^\dagger \\&=\! (f_{11})^\dagger \vee \left( \bigvee _{n \in \omega } f_{21} \circ f_{22}^n \circ f_{12}\right) ^\dagger =\! (f_{11})^\dagger \vee \bigvee _{n \in \omega } (f_{12})^\dagger \circ (f_{22}^n)^\dagger \circ (f_{21})^\dagger \\&= (f^\dagger )_{11} \vee \bigvee _{n \in \omega } (f^\dagger )_{21} \circ (f^\dagger )_{22}^n \circ (f^\dagger )_{12} = \text {Tr}_{Y,X}^U(f^\dagger ) \end{aligned}$$

by definition of the partial sum as join (Lemma 5), and by $(\bigvee _{f \in F} f)^\dagger = \bigvee _{f \in F} f^\dagger$ by Lemma 2.    $\square$

5 Conclusion

We have shown that inverse categories with countable joins carry with them a few key properties that are highly useful for modelling partial reversible functional programming. Notably, we have shown that any inverse category with countable joins is CPO-enriched – from this view, we gathered that morphism schemes have fixed points, and that the partial inverses of such fixed points can be computed as fixed points of adjoint morphism schemes. This gave us a model of recursion à la rfun.

Further, we were able to show that any inverse category can be embedded in an inverse category with joins, in which all join restriction functors have canonical fixed points. Finally, we showed that the presence of a join-preserving disjointness tensor on an inverse category with countable joins gives us a strong unique decomposition category, and in turn, a uniform $\dagger$-trace: a model of recursion à la Theseus and $\varPi ^0$.

Restriction categories have recently been considered as enriched categories by Cockett & Garner [12], though their approach relied on enrichments based on weak double categories rather than monoidal categories, as it is otherwise usually done (including in this paper). Further, fixed points in categories with a notion of partiality have previously been considered, notably by Fiore [14] who also relied on order-enrichment, though his work was in categories of partial maps directly. Finally, Giles [16] has shown the construction of a trace in inverse categories recently, relying instead on the presence of countable disjoint sums rather than joins (whether or not this approach leads to a $\dagger$-trace is unspecified). It should also be noted that the trace in the canonical inverse category $\mathbf {PInj}$ has seen study independent of unique decomposition and restriction categories, notably by Hines [22] and Abramsky, Haghverdi, and Scott [2].

As regards future work, since an inverse category with countable joins and a disjointness tensor is $\dagger$-traced, it can be embedded in a $\dagger$-compact closed category via the Int-construction [26, 38]. It may be of interest to consider $\dagger$-compact closed categories generated in this manner, as we suspect these will be inverse categories as well (notably, $\text {Int}(\mathbf {PInj})$ is [22]) – and could provide, e.g., an alternative treatment of projectors as restriction idempotents, and isometries as restriction monics (see also Selinger [36]).

Additionally, while our focus in this article has been on inverse categories, we conjecture that many of these results can be generalized to restriction categories.