Unifying Guarded and Unguarded Iteration

Abstract

Models of iterated computation, such as (completely) iterative monads, often depend on a notion of guardedness, which guarantees unique solvability of recursive equations and requires roughly that recursive calls happen only under certain guarding operations. On the other hand, many models of iteration do admit unguarded iteration. Solutions are then no longer unique, and in general not even determined as least or greatest fixpoints, being instead governed by quasi-equational axioms. Monads that support unguarded iteration in this sense are called (complete) Elgot monads. Here, we propose to equip monads with an abstract notion of guardedness and then require solvability of abstractly guarded recursive equations; examples of such abstractly guarded pre-iterative monads include both iterative monads and Elgot monads, the latter by deeming any recursive definition to be abstractly guarded. Our main result is then that Elgot monads are precisely the iteration-congruent retracts of abstractly guarded iterative monads, the latter being defined as admitting unique solutions of abstractly guarded recursive equations; in other words, models of unguarded iteration come about by quotienting models of guarded iteration.

1 Introduction

In recursion theory, notions of guardedness traditionally play a central role. Guardedness typically means that recursive calls must be in the scope of certain guarding operations, a condition aimed, among other things, at ensuring progress. The paradigmatic case are recursive definitions in process algebra, which are usually called guarded if recursive calls occur only under action prefixing [6]. A more abstract example are completely iterative theories [11] and monads [19], where, in the latter setting, a recursive definition is guarded if it factors through a given ideal of the monad. Guarded recursive definitions typically have unique solutions; e.g. the unique solution of the guarded recursive definition

$$\begin{aligned} X =a.\,X \end{aligned}$$

is the process that keeps performing the action a.

For unguarded recursive definitions, the picture is, of course, different. E.g. to obtain the denotational semantics of an unproductive while loop characterized by circular operational behavior

one will select one of many solutions of this trivial equation, e.g. the least solution in a domain-theoretic semantics.

Sometimes, however, one has a selection among non-unique solutions of unguarded recursive equations that is not determined order-theoretically, i.e. by picking least or greatest fixpoints. One example arises from coinductive resumptions [16, 25, 26]. In the paradigm of monad-based encapsulation of side-effects [21], coinductive resumptions over a base effect encapsulated by a monad T form a coinductive resumption transform monad $T^\nu$ given by

$$\begin{aligned} T^\nu X= \nu \gamma .\,T(X+\gamma ) \end{aligned}$$

(1)

– that is, a computation over X performs a step with effects from T, and then returns either a value from X or a resumption that, when resumed, proceeds similarly, possibly ad infinitum. We generally restrict to monads T for which (1) exists for all X (although many of our results do not depend on this assumption). Functors (or monads) T for which this holds are called iteratable [1]. Most computationally relevant monads are iteratable (notable exceptions in the category of sets are the powerset monad and the continuation monad). Notice that one has a natural delay map $T^\nu X\rightarrow T^\nu X$ that converts a computation into a resumption, i.e. prefixes it with a delay step. In fact, for $T=\mathsf {id}$, $T^\nu$ is precisely Capretta’s partiality monad [8], also called the delay monad. It is not in general possible to equip $T^\nu X$ with a domain structure that would allow for selecting least or greatest solutions of unguarded recursive definitions over $T^\nu$. However, one can select solutions in a coherent way, that is, such that a range of natural quasi-equational axioms is satisfied, making $T^\nu$ into a (complete) Elgot monad [2, 15].

In the current work we aim to unify theories of guarded and unguarded iteration. To this end, we introduce a notion of abstractly guarded monads, that is, monads T equipped with a distinguished class of abstractly guarded equation morphisms satisfying some natural closure properties (Sect. 3). The notion of abstract guardedness can be instantiated in various ways, e.g. with the class of immediately terminating ‘recursive’ definitions, with the class of guarded morphisms in a completely iterative monad, or with the class of all equation morphisms. We call an abstractly guarded monad pre-iterative if all abstractly guarded equation morphisms have a solution, and iterative if these solutions are unique. Then completely iterative monads are iterative abstractly guarded monads in this sense, and (complete) Elgot monads are pre-iterative, where we deem every equation morphism to be abstractly guarded in the latter case.

The quasi-equational axioms of Elgot monads are easily seen to be satisfied when fixpoints are unique, i.e. in iterative abstractly guarded monads, and moreover stable under iteration-congruent retractions in a fairly obvious sense. Our first main result (Sect. 5, Theorem 22) states that the converse holds as well, i.e. a monad T is a complete Elgot monad iff T is an iteration-congruent retract of an iterative abstractly guarded monad – specifically of $T^\nu$ as in (1). As a slogan,

monad-based models of unguarded recursion arise by quotienting models of guarded recursion.

Our second main result (Theorem 26) is an algebraic characterization of complete Elgot monads: We show that the construction $(-)^\nu$ mapping a monad T to $T^\nu$ as in (1) is a monad on the category of monads (modulo existence of $T^\nu$), and complete Elgot monads are precisely those $(-)^\nu$ -algebras T that cancel the delay map on $T^\nu$, i.e. interpret the delay operation as identity.

As an illustration of these results, we show (Sect. 6) that sandwiching a complete Elgot monad between adjoint functors again yields a complete Elgot monad, in analogy to a corresponding result for completely iterative monads [26]. Specifically, we prove a sandwich theorem for iterative abstractly guarded monads and transfer it to complete Elgot monads using our first main result. For illustration, we then relate iteration in ultrametric spaces using Escardó’s metric lifting monad [12] to iteration in pointed cpo’s, by noting that the corresponding monads on sets obtained using our sandwich theorems are related by an iteration-congruent retraction in the sense of our first main result.

2 Preliminaries

We work in a category $\mathbf {C}$ with finite coproducts. We fix the notation ${\mathsf {in}}_i:X_i\rightarrow X_1+\ldots +X_n$ for the i-th injection. A morphism $\sigma :Y\rightarrow X$ is a summand of X, which we denote , if there is $\sigma ':X'\rightarrow X$ such that X is a coproduct of Y and $X'$ with $\sigma$ and $\sigma '$ being coproduct injections. The morphism $\sigma '$ is called a (coproduct) complement of $\sigma$ and by definition is also a summand. We are not assuming that $\mathbf {C}$ is extensive, and coproduct complements are not in general uniquely determined.

A monad $\mathbb {T}$ over $\mathbf {C}$ can be given in a form of a Kleisli triple where T is an endomap over the objects $|\mathbf {C}|$ of $\mathbf {C}$, the unit $\eta$ is a family of morphisms $(\eta _X:X\rightarrow TX)_{X\in |\mathbf {C}|}$, Kleisli lifting is a family of maps $:\mathsf {Hom}(X,TY)\rightarrow \mathsf {Hom}(TX,TY)$, and the monad laws are satisfied:

$$\begin{aligned} \eta ^{\star }=\mathsf {id}, \qquad \qquad f^{\star }\eta =f, \qquad \qquad (f^{\star } g)^{\star }=f^{\star } g^{\star }. \end{aligned}$$

The standard (equivalent) categorical definition [18] of $\mathbb {T}$ as an endofunctor with natural transformation unit $\eta :{\text {Id}}\rightarrow T$ and multiplication $\mu :TT\rightarrow T$ can be recovered by taking $Tf = (\eta \,f)^\star$, $\mu =\mathsf {id}^\star$. (We adopt the convention that monads and their functor parts are denoted by the same letter, with the former in blackboard bold.) We call morphisms $X\rightarrow TY$ Kleisli morphisms and view them as a high level abstraction of sequential programs with $\mathbb {T}$ encapsulating the underlying computational effect as proposed by Moggi [22], with X representing the input type and Y the output type. A more traditional use of monads in semantics is due to Lawvere [17], who identified finitary monads on $\mathbf {Set}$ with algebraic theories, hence objects TX can be viewed as sets of terms of the theory over free variables from X, the unit as the operation of casting a variable to a term, and Kleisli composition as substitution. We informally refer to this use of monads as algebraic monads.

A(n F -)coalgebra is a pair $(X,f:X\rightarrow FX)$ where $X\in |\mathbf {C}|$ and $F:\mathbf {C}\rightarrow \mathbf {C}$ is an endofunctor. Coalgebras form a category, with morphisms $(X,f)\rightarrow (Y,g)$ being $\mathbf {C}$-morphisms $h:X\rightarrow Y$ such that $(Fh)\, f = g h$. A final object of this category is called a final coalgebra, and we denote it by $(\nu F,{\mathsf {out}}:\nu F\rightarrow F\nu F)$ if it exists. For brevity, we will be cavalier about existence of final coalgebras and silently assume they exist when we need them; that is, we hide sanity conditions on the involved functors, such as accessibility. By definition, $\nu F$ comes with coiteration as a definition principle (dual to the iteration principle for algebras): given a coalgebra $(X,f:X\rightarrow FX)$ there is a unique morphism $({\mathsf {coit}}\,\,f):X\rightarrow \nu F$ such that

$$\begin{aligned} {\mathsf {out}}\,({\mathsf {coit}}\,\,f) = F({\mathsf {coit}}\,\,f)\,\, f. \end{aligned}$$

This implies that ${\mathsf {out}}$ is an isomorphism (Lambek’s lemma) and that ${\mathsf {coit}}\,\,{\mathsf {out}}=\mathsf {id}$ (see [29] for more details about coalgebras for coiteration).

We generally drop sub- and superscripts, e.g. on natural transformations, whenever this improves readability.

3 Guarded Monads

The notion of guardedness is paramount in process algebra: typically one considers systems of mutually recursive process definitions of the form $x_i = t_i$, and a variable $x_i$ is said to be guarded in $t_j$ if it occurs in $t_j$ only in subterms of the form a.s where is action prefixing. A standard categorical approach is to replace the set of terms over variables X by an object TX where $\mathbb {T}$ is a monad. We then can model separate variables by partitioning X into a sum $X_1 +\ldots + X_n$ and thus talk about guardedness of a morphism $f:X\rightarrow T(X_1 + \ldots + X_n)$ in any $X_i$, meaning that every variable from $X_i$ is guarded in f. Since Kleisli morphisms can be thought of as abstract programs we can therefore speak about guardedness of a program in a certain portion of the output type, e.g. . One way to capture guardedness categorically is to identify the operations of $\mathbb {T}$ that serve as guards by distinguishing a suitable subobject of $\mathbb {T}$; e.g. the definition of completely iterative monad [19] follows this approach. For our purposes, we require a yet more general notion where we just distinguish some Kleisli morphisms as being guarded in certain output variables. This is formalized as follows.

Definition 1

((Abstractly) guarded monad). We call a monad $\mathbb {T}$ (abstractly) guarded if it is equipped with a notion of (abstract) guardedness, i.e. with a relation between morphisms $f:X\rightarrow TY$ and summands of Y (by putting the word ‘abstract’ in brackets we mean that we will often omit it later). We call $f:X\rightarrow TY$ (abstractly) $\sigma$ -guarded if f and are in this relation, and then write $f:X\rightarrow _\sigma TY$. Abstract guardedness is required to be closed under the rules in Fig. 1. In rule (wkn), $\sigma$ and $\theta$ are composable summands.

Given guarded monads $\mathbb {T}$, $\mathbb {S}$, a monad morphism $\alpha :T\rightarrow S$ is (abstractly) guarded if whenever $f:X\rightarrow _\sigma TY$ then $\alpha f:X\rightarrow _\sigma SY$.

Fig. 1.

Axioms of guardedness.

Intuitively, (trv) says that if a program does not output anything via a summand of the output type then it is guarded in that summand. Rule (wkn) is a weakening principle: if a program is guarded in some summand then it is guarded in any subsummand of that summand. Rule (cmp) asserts that guardedness is preserved by composition: if the unguarded part of the output of a program is postcomposed with a $\sigma$-guarded program then the result is $\sigma$-guarded, no matter how the guarded part is transformed. Finally, rule (sum) says that putting two guarded equation systems side by side again produces a guarded system. The rules are designed so as to enable a reformulation of the classical laws of iteration w.r.t. abstract guardedness, as we shall see in Sect. 5.

We write $f:X\rightarrow _{i_1,\ldots ,i_k} T(X_1+\ldots +X_n)$ as a shorthand for $f:X\rightarrow _\sigma T(X_1+\ldots +X_n)$ with . More generally, we sometimes need to refer to components of some $X_{i_j}$. This amounts to replacing the corresponding $i_j$ with a sequence of pairs $i_j n_{j,m}$, and $\,\mathsf {in}_{i_j}$ with $\,\mathsf {in}_{i_j}[\,\mathsf {in}_{n_{j,1}},\ldots ,\,\mathsf {in}_{n_{j,k_j}}]$, so, e.g. we write $f:X\rightarrow _{12,2} T((Y+Z)+Z)$ to mean that f is $[\,\mathsf {in}_1\,\mathsf {in}_2,\,\mathsf {in}_2]$-guarded. Where coproducts $Y+Z$ etc. appear in the rules, we mean any coproduct, not just some selected coproduct. We defined the notion of guardedness as a certain relation over Kleisli morphisms and summands. Clearly, the largest such relation is the one declaring all Kleisli morphisms to be $\sigma$-guarded for all $\sigma$. We call monads equipped with this notion of guardedness totally guarded. It turns out that for every monad we also have a least guardedness relation.

Definition 2

Let $\mathbb {T}$ be a monad. A morphism $f:X\rightarrow TY$ is trivially $\sigma$ -guarded for if f factors through $T\sigma '$ for a coproduct complement $\sigma '$ of $\sigma$.

Proposition 3

Let $\mathbb {T}$ be a monad. Then taking the abstractly guarded morphisms to be the trivially guarded morphisms is the least guardedness relation making $\mathbb {T}$ into a guarded monad.

We call a guarded monad trivially guarded if all its abstractly guarded morphisms are trivially guarded. As we see, the notion of abstract guardedness can vary on a large spectrum from trivial guardedness to total guardedness, thus somewhat detaching abstract guardedness from the original intuition. It is for this reason that we introduced the qualifier abstract into the terminology; for brevity, we will omit this qualifier in the sequel in contexts where no confusion is likely, speaking only of guarded monads, guarded morphisms etc.

Remark 4

Although by (wkn), $f:X\rightarrow _{1,2} T(Y+Z)$ implies both $f:X\rightarrow _{1} T(Y+Z)$ and $f:X\rightarrow _{2} T(Y+Z)$, the converse is not required to be true, and in fact can fail even for trivial guardedness. This is witnessed by the following simple counterexample. Let $\mathbb {T}$ be the algebraic monad given by taking TX to be the free commutative semigroup over X satisfying the additional law $x + y = x$. Now the term $x+y\in T(X+Y)$ (seen as a morphism $1\rightarrow T(X+Y)$) with $x\in X$ and $y\in Y$ is both $\,\mathsf {in}_1$-guarded and $\,\mathsf {in}_2$-guarded, being equivalent both to y and to x. But it is not $\mathsf {id}$-guarded, because it does not factor through .

As usual, guardedness serves to identify systems of equations that admit solutions according to some global principle:

Definition 5

(Guarded (pre-)iterative monad). Given $f:X\rightarrow _2 T(Y+X)$, we say that $f^\dagger :X\rightarrow TY$ is a solution of f if $f^\dagger$ satisfies the fixpoint identity $f^\dagger = [\eta ,f^\dagger ]^\star f$. A guarded monad $\mathbb {T}$ is guarded pre-iterative if it is equipped with an iteration operator that assigns to every $\,\mathsf {in}_2$-guarded morphism $f:X\rightarrow _2 T(Y+X)$ a solution $f^\dagger$ of f. If every such f has a unique solution, we call $\mathbb {T}$ guarded iterative.

We can readily check that the iteration operator preserves guardedness.

Proposition 6

Let $\mathbb {T}$ be a guarded pre-iterative monad, let , and let $f:X\rightarrow _{\sigma +\mathsf {id}} T(Y+X)$. Then $f^{\dagger }:X\rightarrow _\sigma TY$.

In trivially guarded monads, there is effectively nothing to iterate, so we have

Proposition 7

Every trivially guarded monad is guarded iterative.

Guardedness in Completely Iterative Monads. One instance of our notion of abstract guardedness is found in completely iterative monads [19], which are based on idealised monads. To make this precise, we need to recall some definitions. First, a module over a monad $\mathbb {T}$ on $\mathbf {C}$ is a pair , where $M$ is an endomap over the objects of $\mathbf {C}$, while the lifting  is a map $\mathsf {Hom}(X,TY)\rightarrow \mathsf {Hom}(M X,M Y)$ such that the following laws are satisfied:

$$\begin{aligned} \eta ^{\circ }= \mathsf {id},&\qquad \qquad g^{\circ }f^{\circ }= (g^\star f)^{\circ }. \end{aligned}$$

Note that $M$ extends to an endofunctor by taking $M f = (\eta f)^{\circ }$. Next, a module-to-monad morphism is a natural transformation $\xi : M \rightarrow T$ that satisfies $\xi f^{\circ }= f^\star \xi$. We call the triple an idealised monad; when no confusion is likely, we refer to these data just as $\mathbb {T}$. Following [19], we can then define guardedness as follows:

Definition 8

Given an idealised monad $\mathbb {T}$ as above, a morphism $f : X \rightarrow T(Y + X)$ is guarded if it factors via $[\eta \,\mathsf {in}_1, \xi ] : Y + M (Y+X) \rightarrow T(Y+X)$. Then, $\mathbb {T}$ is a completely iterative monad if every such guarded f has a unique solution.

It turns out that this notion of guardedness is not an instance of our notion of abstract guardedness. Fortunately, we can fix this by noticing that completely iterative monads actually support iteration for a wider class of morphisms:

Definition 9

Let be an idealised monad. Given , we say that a morphism $f : X \rightarrow T Y$ is weakly $\sigma$ -guarded if it factors through $[\eta \sigma ', \xi ]^\star : T(Y' + MY) \rightarrow TY$ for a complement of $\sigma$.

Since a morphism that factors as $[\eta \,\mathsf {in}_1, \xi ] f$ can be rewritten as $[\eta \,\mathsf {in}_1, \xi ]^\star \eta f$, every guarded morphism in an idealised monad is also weakly guarded.

Theorem 10

Let be an idealised monad. Then the following hold.

• 1. $\mathbb {T}$ becomes abstractly guarded when equipped with weak guardedness as the notion of abstract guardedness.

• 2. If $\mathbb {T}$ is completely iterative, then every weakly $\,\mathsf {in}_2$-guarded morphism $f:X\rightarrow T(Y+X)$ has a unique solution.

That is, completely iterative monads are abstractly guarded iterative monads w.r.t. weak guardedness.

4 Parametrizing Guardedness

Uustalu [28] defines a parametrized monad to be a functor from a category $\mathbf {C}$ to the category of monads over $\mathbf {C}$. We need a minor adaptation of this notion where we allow parameters from a different category than $\mathbf {C}$, and simultaneously introduce a guarded version of parametrized monads:

Definition 11

(Parametrized guarded monad). A parametrized (guarded) monad is a functor from a category $\mathbf {D}$ to the category of (guarded) monads and (guarded) monad morphisms over $\mathbf {C}$. Alternatively (by uncurrying), it is a bifunctor such that for any $X\in |\mathbf {D}|$, is a (guarded) monad, and for every $f:X\rightarrow Y$, is the Z-component of a (guarded) monad morphism .

A parametrized (guarded) monad morphism between guarded monads qua functors into the category of monads over $\mathbf {C}$ is a natural transformation that is componentwise a monad morphism. In uncurried notation, given parametrized monads a natural transformation is a parametrized (guarded) monad morphism if for each $X\in |\mathbf {D}|$, is a (guarded) monad morphism.

Guardedness of the monad morphisms means explicitly that implies .

Example 12

For the purposes of the present work, the most important example (taken from [28]) is where $\mathbb {T}$ is a (non-parametrized) monad on $\mathbf {C}$ and $\varSigma$ is an endofunctor on $\mathbf {C}$. Informally, $\mathbb {T}$ captures a computational effect, e.g. nondeterminism for T being powerset, and $\varSigma$ captures a signature of actions, e.g. $\varSigma X=A\times X$, as in process algebra. Specifically, taking $A=1$ we obtain ; in this case, we have only one guard, which can be interpreted as a delay. The second argument of can thus be thought of as designated for guarded recursion.

Incidentally, our modification of parametrized monads also covers Atkey’s parametrized monads [5], which are certain functors $\mathbf {S}\times \mathbf {S}^{op}\times \mathbf {C}\rightarrow \mathbf {C}$ forming a monad in the third argument. The first and the second arguments serve, e.g., to parametrize the computational effect of interest with initial and final states of different types.

Theorem 13

Let be a parametrized monad, with unit $\eta$ and Kleisli lifting $(-)^\star$. Then

defines a parametrized monad whose unit and Kleisli lifting we denote $\eta ^\nu$ and , respectively. Moreover,

• 1. If is guarded then so is with guardedness defined as follows: given , is $\sigma$-guarded if is $\sigma$-guarded.

• 2. If is pre-iterative under an iteration operator then so is with the iteration operator defined as follows:

  

• 3. If is iterative then so is under the definition from the previous clause.

Example 14

We spell out one instance of Theorem 13 in case $\mathbf {D}=1$ and where is a monad. Then is isomorphically a monad $\mathbb {T}^\nu$ on $\mathbf {C}$ with $T^\nu X=\nu \gamma .\,T(X+\gamma )$, unit $\eta ^\nu = \eta \,\mathsf {in}_1$ and Kleisli star being uniquely determined by the equation

If $\mathbb {T}$ is pre-iterative then so is $\mathbb {T}^\nu$ with iteration

$$\begin{aligned} (f:X\rightarrow T^\nu (Y+X))^\ddagger ={\mathsf {coit}}\,\,\bigl ([\eta \,\mathsf {in}_2,(T[\,\mathsf {in}_1+\mathsf {id},\,\mathsf {in}_1\,\mathsf {in}_2]{\mathsf {out}}\, f)^\dagger ]^\star {\mathsf {out}}\bigr )\,\eta ^\nu \,\mathsf {in}_2. \end{aligned}$$

Example 15

Theorem 13 shows that our notion of guardedness extends along the applications of the final coalgebra transformer on parametrized monads. This can be used to capture existing notions of guardedness as follows. Consider where $\mathbb {T}$ is some monad. In $\mathbf {Set}$, $1+A$ can be thought of as consisting of a set A of visible actions and a silent action $\tau$. In process algebra we standardly consider a process definition to be guarded if every recursive call is preceded by a visible action from A. In our framework this can be reconstructed as follows. The obvious isomorphism

$$\begin{aligned} \nu \gamma .\,T(X+(1+A)\times \gamma )\cong \nu \gamma '.\,\nu \gamma .\,T(X+\gamma + A\times \gamma ') \end{aligned}$$

involves two more parametrized monads: and . By taking the latter to be trivially guarded and then defining guardedness for $\nu \gamma '.\,\nu \gamma .\,T(X+\gamma + A\times \gamma ')$ using Theorem 13, we arrive precisely at the notion we expected for the isomorphic monad .

5 Complete Elgot Monads and Iteration Congruences

Besides the fixpoint identity we are interested in the following classical properties of the iteration operator, which we refer to as the iteration laws [7, 10, 27]:

• naturality: $g^{\star } f^{\dagger } = ([(T\,\mathsf {in}_1) \,g, \eta \,\mathsf {in}_2]^{\star } \,f)^{\dagger }$ for $f:X\rightarrow _2 T(Y+X)$, $g : Y \rightarrow TZ$;

• dinaturality: $([\eta \,\mathsf {in}_1, h]^{\star } \,g)^{\dagger } = [\eta , ([\eta \,\mathsf {in}_1, g]^{\star } \,h)^{\dagger }]^{\star } \,g$ for $g : X \rightarrow _2 T(Y + Z)$ and $h:Z\rightarrow T(Y+X)$ or $g : X \rightarrow T(Y + Z)$ and $h:Z\rightarrow _2 T(Y+X)$;

• codiagonal: $(T[\mathsf {id},\,\mathsf {in}_2] \,f)^{\dagger } = f^{\dagger \dagger }$ for $f : X \rightarrow _{12,2} T((Y + X) + X)$;

• uniformity: $f \,h = T(\mathsf {id}+ h) \,g$ implies $f^{\dagger } \,h = g^{\dagger }$ for $f: X \rightarrow _2 T(Y + X)$, $g: Z \rightarrow _2 T(Y + Z)$ and $h: Z \rightarrow X$.

The axioms are summarized in graphical form in Fig. 2, and then become quite intuitive. The two versions of the dinaturality axiom correspond to the alternative sets of guardedness assumptions mentioned above. We indicate the scope of the iteration operator by a shaded box and guardedness by bullets at the outputs of a morphism.

Fig. 2.

Axioms of guarded iteration.

A guarded pre-iterative monad is called a complete Elgot monad if it is totally guarded and satisfies all iteration laws. In the sequel we shorten ‘complete Elgot monads’ to ‘Elgot monads’ (to be distinguished from Elgot monads in the sense of [2], which have solutions only for morphisms with finitely presentable domain).

In general, the fact that the iteration laws are correctly formulated relies on the axioms for guardedness. E.g., in the dinaturality axiom it suffices to assume that $g : X \rightarrow T(Y + Z)$ is $\,\mathsf {in}_2$-guarded and this implies that both $[\eta \,\mathsf {in}_1, h]^{\star } \,g$ and $[\eta \,\mathsf {in}_1, g]^{\star } \,h$ are $\,\mathsf {in}_2$-guarded by (cmp) and (trv), and additionally (sum) in the latter case. Symmetrically, it suffices to make the analogous assumption about h. In the codiagonal axiom, it follows from the assumption $f : X \rightarrow _{12,2} T((Y + X) + X)$ by (cmp) that $T[\mathsf {id},\,\mathsf {in}_2] \,f$ is $\,\mathsf {in}_2$-guarded and by Proposition 6 that $f^\dagger$ is $\,\mathsf {in}_2$-guarded. Indeed, the axioms for guarded monads are designed precisely to enable the formulation of the iteration laws.

We show that for guarded iterative monads all iteration laws are automatic. Prior to that, we show that dinaturality follows from the others (thus generalizing the corresponding observation made recently [13, 15]).

Proposition 16

Any guarded pre-iterative monad satisfying naturality, codiagonal and uniformity also satisfies dinaturality, as well as the Bekić identity

$$\begin{aligned} \bigl [T[\mathsf {id}+\,\mathsf {in}_1,\,\mathsf {in}_2]^\star \,f, T[\mathsf {id}+\,\mathsf {in}_1,\,\mathsf {in}_2]^\star \,g\bigr ]^\dagger = [h^\dagger , [\eta ,h^\dagger ]^\star g^\dagger ] \end{aligned}$$

where $f:X\rightarrow _{12,2} T((Y+X)+Z)$, $g:Z\rightarrow _{12,2} T((Y+X)+Z)$, and $h= [\eta ,g^\dagger ]^\star f:X\rightarrow _2 T(Y+X)$.

The proof of the following result runs in accordance with the original ideas of Elgot [10] for iterative theories, except that, by Proposition 16, dinaturality is now replaced by uniformity.

Theorem 17

Every guarded iterative monad validates naturality, dinaturality, codiagonal and uniformity.

We now proceed to introduce key properties of morphisms of guarded monads that allow for transferring pre-iterativity and the iteration laws, respectively.

Definition 18

(Guarded retraction). Let $\mathbb {T}$ and $\mathbb {S}$ be guarded monads. We call a monad morphism $\rho :\mathbb {T}\rightarrow \mathbb {S}$ a guarded retraction if there is a family of morphisms $(\upsilon _X:SX\rightarrow TX)_{X\in |\mathbf {C}|}$ (not necessarily natural in X!) such that

• 1. for every $f:X\rightarrow _{\sigma } SY$, we have $\upsilon _Y f:X\rightarrow _{\sigma } TY$,

• 2. $\rho _X\upsilon _X=\mathsf {id}$ for all $X\in |\mathbf {C}|$.

Theorem 19

Let $\rho :\mathbb {T}\rightarrow \mathbb {S}$ be a guarded retraction, witnessed by $\upsilon :\mathbb {S}\rightarrow \mathbb {T}$, and suppose that is guarded pre-iterative. Then $\mathbb {S}$ is guarded pre-iterative with the iteration operator given by $f^\ddagger = \rho \,(\upsilon f)^\dagger$.

Definition 20

(Iteration congruence). Let $\mathbb {T}$ be a guarded pre-iterative monad and let $\mathbb {S}$ be a monad. We call a monad morphism $\rho :\mathbb {T}\rightarrow \mathbb {S}$ an iteration congruence if for every pair of morphisms $f,g:X\rightarrow _2 T(Y+X)$,

$$\begin{aligned} \rho f = \rho g\implies \rho f^\dagger = \rho g^\dagger . \end{aligned}$$

(2)

If $\rho$ is moreover a guarded retraction, we call $\rho$ an iteration-congruent retraction.

Theorem 21

Under the premises of Theorem 19, assume moreover that $\rho$ is an iteration-congruent retraction. Then any property out of naturality, dinaturality, codiagonal, and uniformity that is satisfied by $\mathbb {T}$ is also satisfied by $\mathbb {S}$.

Proof

(Sketch). The crucial observation is that under our assumptions, (2) is equivalent to the condition that for all $f:X\rightarrow _2 T(Y+X)$,

$$\begin{aligned} \rho \,(\upsilon \rho \,f)^\dagger = \rho f^\dagger . \end{aligned}$$

(3)

Indeed, (2) $\implies$ (3), for $\rho \upsilon \rho \,f=\rho \,f$ and therefore $\rho (\upsilon \rho \,f)^\dagger = \rho \,f^\dagger$ and conversely, assuming (3) both for f and for g, and $\rho f = \rho g$, we obtain that $\rho f^\dagger = \rho (\upsilon \rho \,f)^\dagger = \rho (\upsilon \rho \,g)^\dagger =\rho g^\dagger$. Using (3), the claim is established routinely.    $\square$

Recall from the introduction that a monad $\mathbb {S}$ is iteratable if its coinductive resumption transform  $\mathbb {S}^\nu$ exists. We make $\mathbb {S}^\nu$ into a guarded monad by applying Theorem 13 to $\mathbb {S}$ as a trivially guarded monad; explicitly: $f:X\rightarrow S^\nu (Y+X)$ is guarded iff ${\mathsf {out}}\, f = S(\,\mathsf {in}_1+\mathsf {id})\,g$ for some $g:X\rightarrow S(Y+S^\nu (Y+X))$. We are now set to prove our first main result, which states that every iteratable Elgot monad can be obtained by quotienting a guarded iterative monad; that is, every choice of solutions that obeys the iteration laws arises by quotienting a more fine-grained model in which solutions are uniquely determined:

Theorem 22

A totally guarded iteratable monad $\mathbb {S}$ is an Elgot monad iff there is a guarded iterative monad $\mathbb {T}$ and an iteration-congruent retraction $\rho :\mathbb {T}\rightarrow \mathbb {S}$. Specifically, every iteratable Elgot monad $\mathbb {S}$ is an iteration-congruent retract of its coinductive resumption transform  $\mathbb {S}^\nu$.

Proof

(Sketch). Direction ($\Leftarrow$) immediately follows from Theorems 17 and 21.

In order to prove ($\Rightarrow$), we show that is an iteration-congruent retract of . Let and

$$\begin{aligned} \rho _X = \bigl (S^\nu X\xrightarrow {~{\mathsf {out}}~} S(X+TX)\bigr )^\dagger . \end{aligned}$$

Clearly, $\upsilon f$ is $\sigma$-guarded for every $f:X\rightarrow SY$ and it is easy to verify that $\upsilon$ is left inverse to $\rho$ by using the fixpoint identity for twice.

Naturality of $\rho$ is proved straightforwardly from naturality of . The remaining calculations showing that $\rho$ is a monad morphism and moreover an iteration congruence make heavy use of the Elgot monad laws.    $\square$

The notions of guarded retraction and iteration congruence straightforwardly extend to parametrized monads. We then can take the claims of Theorem 13 further.

Theorem 23

Let be guarded parametrized monads and let be an iteration-congruent retraction. By Theorem 13, and are also parametrized guarded monads. Then , with components

is again an iteration-congruent retraction.

Theorems 22 and 23 jointly provide a simple and structured way of showing that Elgotness extends along the parametrized monad transformer : If is Elgot then by Theorem 22 there is an iteration-congruent retraction ; by Theorem 23, it gives rise to an iteration-congruent retraction

and by Theorem 22, the right-hand side is again Elgot. We have thus proved.

Corollary 24

Given a parametrized monad and $X\in |\mathbf {C}|$, if is Elgot then so is .

This yields a more general and simpler proof of one of the main results in [15].

Example 25

By instantiating in Corollary 24 with where ${\mathcal P}_{\omega }$ is the countable powerset monad, we obtain $\nu \gamma .\,{\mathcal P}_{\omega }(X+A\times \gamma )$, which can be viewed as a semantic domain for countably branching processes that possibly terminate with results in X and are taken modulo strong bisimilarity. The simple fact that ${\mathcal P}_{\omega }$ is Elgot [15] implies that so is $\nu \gamma .\,{\mathcal P}_{\omega }(X+A\times \gamma )$. This justifies the use of systems of possibly unguarded recursive process algebra equations (as done, e.g., in [6]). It is worth noting that the iteration operator of the transformed monad is neither least nor unique. It arises by introducing an additional delay action that guards all recursive calls and then eliminating these delays from the unique solution of the new recursive definition; the delay elimination is the effect of $\rho ^\nu$ in Theorem 23.

Theorem 22 characterizes iteratable Elgot monads as iteration-congruent retracts of their -transforms. We take this perspective further as follows. Let us call $\mathbb {T}$ strongly iteratable if every $T^{\nu \ldots \nu }$ exists. Consider the functor $\mathbb {T}\mapsto \mathbb {T}^\nu$ on the category of strongly iteratable monads over $\mathbf {C}$. This is itself a monad: the unit $\varvec{\eta }$ is the natural transformation with components and the multiplication $\varvec{\mu }:T^{\nu \nu }\rightarrow T^\nu$ has components

For every T we define the delay transformation . This leads to our second main result:

Theorem 26

The category of strongly iteratable Elgot monads over $\mathbf {C}$ is isomorphic to the full subcategory of the category of -algebras for strongly iteratable $\mathbb {S}$ consisting of the -algebras $(S^\nu ,\rho :S^\nu \rightarrow S)$ satisfying .

Proof

(Sketch). To show that every strongly iteratable Elgot monad is a -algebra, one has to check the equations $\rho \varvec{\eta }=\mathsf {id}$ and $\rho \varvec{\mu }=\rho \rho ^\nu$ where $\rho ^\nu = {\mathsf {coit}}\,\,(\rho \,{\mathsf {out}}):S^{\nu \nu }\rightarrow S^\nu$. The first equation follows relatively easily. The second one is shown along the following lines:

Here, (i) and (iii) only amount to equivalent transformations of $\varvec{\mu }$ and $\rho ^\nu$, respectively, while (ii) makes crucial use of the fact that $\rho$ is an iteration congruence, as implied by Theorem 22.

For the converse implication, we start with a -algebra and verify the Elgot monad laws for the iteration operator $f^\dagger = \rho ({\mathsf {coit}}\,\,f)$.    $\square$

Remark 27

The delay cancellation condition is essential, as can be seen on a simple example. Let $\mathbf {Mon}(\mathbf {C})^\nu$ be the category of -algebras and let be its subcategory figuring in Theorem 26. Since the identity functor is the initial monad, the initial object of $\mathbf {Mon}(\mathbf {C})^\nu$ is Capretta’s delay monad [8] . On the other hand, the initial object of (if it exists) is the initial Elgot monad $\mathbb {L}$, which on $\mathbf {C}=\mathbf {Set}$ is the maybe monad .

If $\mathbf {C}=\mathbf {Set}$, then $DX=(X\times N + 1)$ does turn out to be Elgot [14] (but applying Theorem 26 to D qua Elgot monad yields a different -algebra structure than the initial one), and $\mathbb {L}$ is, in this case, a retract of $\mathbb {D}$ in . The situation is more intricate in categories with a non-classical internal logic, for which $\mathbb {D}$ is mainly intended. We believe that in such a setting, neither is $\mathbb {D}$ Elgot in general, nor is $\mathbb {L}$ the maybe monad. However, there will still be a unique -algebra morphism $\mathbb {D}\rightarrow \mathbb {L}$ in $\mathbf {Mon}(\mathbf {C})^\nu$.

6 A Sandwich Theorem for Elgot Monads

As an application of Theorem 22, we show that sandwiching an Elgot monad between adjoint functors again yields an Elgot monad. A similar result has been shown for completely iterative monads [26]; this result generalizes straightforwardly to guarded iterative monads:

Theorem 28

Let $F : \mathbf {C}\rightarrow \mathbf {D}$ and $U : \mathbf {D}\rightarrow \mathbf {C}$ be a pair of adjoint functors with the associated natural isomorphism $\varPhi : \mathbf {D}(FX,Y) \rightarrow \mathbf {C}(X,UY)$, and let $\mathbb {T}$ be a guarded iterative monad on $\mathbf {D}$. Then the monad induced on the composite functor UTF is guarded iterative, with the guardedness relation defined by taking $f : X \rightarrow _\sigma UTFY$ if and only if $\varPhi ^{-1}f : FX \rightarrow _\sigma TFY$, and the unique solutions given by $f \mapsto \varPhi ((\varPhi ^{-1}f)^\dagger )$.

Now, to obtain a similar result for Elgot monads, we can easily combine Theorems 22 and 28 without having to verify the equational properties by hand.

Theorem 29

With an adjunction as in Theorem 28, let $\mathbb {S}$ be an Elgot monad on $\mathbf {D}$. Then, the monad induced on the composition USF is an Elgot monad.

Proof

(Sketch). By Theorem 22, there exists a guarded iterative monad $\mathbb {T}$ and an iteration-congruent retraction $\rho : \mathbb {T}\rightarrow \mathbb {S}$. By Theorem 28, the monad induced on UTF is guarded iterative. Again by Theorem 22, it suffices to show that $U \rho F : UTF \rightarrow USF$ is an iteration-congruent retraction, which is straightforward.    $\square$

Example 30

(From Metric to CPO-based Iteration). As an example exhibiting sandwiching as well as the setting of Theorem 22, we compare two iteration operators on $\mathbf {Set}$ that arise from different fixed-point theorems: Banach’s, for complete metric spaces, and Kleene’s, for complete partial orders, respectively. We obtain the first operator by sandwiching Escardo’s metric lifting monad $\mathbb {S}$ [12] in the adjunction between sets and bounded complete ultrametric spaces (which forgets the metric in one direction and takes discrete spaces in the other), obtaining a monad on $\mathbf {Set}$. Given a bounded complete metric space (X, d), S(X, d) is a metric on the set $(X\times \mathbb N)\cup \{\bot \}$. As we show in the appendix, $\mathbb {S}$ is guarded iterative if we define $f:(X,d)\rightarrow S(Y,d')$ to be $\sigma$-guarded if $k>0$ whenever $f(x)=(\sigma (y),k)$. By Theorem 28, is also guarded iterative (of course, this can also be shown directly). The second monad arises by sandwiching the identity monad on cpos with bottom in the adjunction between sets and cpos with bottom that forgets the ordering in one direction and adjoins bottom in the other, obtaining an Elgot monad $\mathbb {L}$ on Set according to Theorem 29. The latter is unsurprising, of course, as $\mathbb {L}$ is just the maybe monad $LX=X+1$.

The monad keeps track of the number of steps needed to obtain the final result. We have an evident extensional collapse map , which just forgets the number of steps. One can show that $\rho$ is in fact an iteration-congruent retraction, so we obtain precisely the situation of Theorem 22.

7 Related Work

Alternatively to our guardedness relation on Kleisli morphisms, guardedness can be formalized using type constructors [23] or, categorically, functors, as in guarded fixpoint categories [20]; the latter cover also total guardedness, like we do. Our approach is slightly more fine-grained, and in particular natively supports the two variants of the dinaturality axiom (Fig. 2), which, e.g., in guarded fixpoint categories require additional assumptions [20, Proposition 3.15] akin to the one we discuss in Remark 4.

A result that resembles our Theorem 26, due to Adámek et al. [3], states roughly that if $\mathbf {C}$ is locally finitely presentable and hyperextensive (e.g. $\mathbf {C}=\mathbf {Set}$) then the finitary Elgot monads are the algebras for a monad on the category of endofunctors given by where $\rho$ takes rational fixpoints (i.e. final coalgebras among those where every point generates a finite subcoalgebra). Besides Theorem 26 making fewer assumptions on $\mathbf {C}$, the key difference is that, precisely by dint of this result, $L_H$ is already an Elgot monad; contrastingly, we characterize Elgot monads as quotients of guarded iterative monads, i.e. of monads where guarded recursive definitions have unique fixpoints.

8 Conclusions and Further Work

We have given a unified account of monad-based guarded and unguarded iteration by axiomatizing the notion of guardedness to cover standard definitions of guardedness, and additionally, as a corner case, what we call total guardedness, i.e. the situation when all morphisms are declared to be guarded. We thus obtain a common umbrella for guarded iterative monads, i.e. monads with unique iterates of guarded morphisms, and Elgot monads, i.e. totally guarded monads satisfying Elgot’s classical laws of iteration. We reinforce the view that the latter constitute a canonical model for monad-based unguarded iteration by establishing the following equivalent characterizations: provided requisite final coalgebras exist, a monad $\mathbb {T}$ is Elgot iff

• it satisfies the quasi-equational theory of iteration [2, 15] (definition);

• it is an iteration-congruent retract of a guarded iterative monad (Theorem 22);

• it is an algebra $(\mathbb {T},\rho )$ of the monad $T\mapsto \nu \gamma .\,T(X+\gamma )$ in the category of monads satisfying a natural delay cancellation condition (Theorem 26).

In future work, we aim to investigate further applications of this machinery, in particular to examples which did not fit previous formalizations. One prospective target is suggested by the work of Nakata and Uustalu [24], who give a coinductive big-step trace semantics for a while-language. We conjecture that this work has an implicit guarded iterative monad under the hood, for which guardedness cannot be defined using the standard argument based on a final coalgebra structure of the monad because is not a final coalgebra.

In type theory, there is growing interest in forming an extensional quotient of the delay monad [4, 9]. It is shown in [9] that under certain reasonable conditions, a suitable collapse of the delay monad by removing delays is again a monad; however, the proof is already quite complex, and proving directly that the collapse is in fact an Elgot monad, as one would be inclined to expect, seems daunting. We expect that Theorem 26 may shed light on this issue. A natural question that arises in this regard is whether the subcategory of -algebras figuring in the theorem is reflexive. A positive answer would provide a means of constructing canonical quotients of -algebras (such as the delay monad) with the results automatically being Elgot monads.