# On Algebras with Effectful Iteration

Stefan Milius, Jiří Adámek, Henning Urbat

► To cite this version:

Stefan Milius, Jiří Adámek, Henning Urbat. On Algebras with Effectful Iteration. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.144-166, 10.1007/978-3-030-00389-0_9. hal-02044647

HAL Id: hal-02044647

https://inria.hal.science/hal-02044647

Submitted on 21 Feb 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On Algebras with Effectful Iteration

Stefan Milius²,*, Jiří Adámek¹, and Henning Urbat²

¹ Czech Technical University in Prague

² Friedrich-Alexander-Universität Erlangen-Nürnberg

**Abstract** For every finitary monad $T$ on sets and every endofunctor $F$ on the category of $T$-algebras we introduce the concept of an ffg-Elgot algebra for $F$, that is, an algebra admitting coherent solutions for finite systems of recursive equations with effects represented by the monad $T$. The goal of this paper is to study the existence and construction of free ffg-Elgot algebras. To this end, we investigate the locally ffg fixed point $\varphi F$, the colimit of all $F$-coalgebras with free finitely generated carrier, which is shown to be the initial ffg-Elgot algebra. This is the technical foundation for our main result: the category of ffg-Elgot algebras is monadic over the category of $T$-algebras.

## 1 Introduction

Terminal coalgebras yield a fully abstract domain of behavior for a given type of state-based systems whose transition type is described by an endofunctor $F$. Often one is mainly interested in the study of the semantics of *finite coalgebras*; for instance, regular languages are the behaviors of finite deterministic automata, while the terminal coalgebra of the corresponding functor is formed by *all* formal languages. For endofunctors on sets, the *rational fixed point* introduced by Adámek, Milius and Velebil [2] yields a fully abstract domain of behavior for finite coalgebras. However, in recent years there has been a lot of interest in studying coalgebras over more general categories than sets. In particular, categories of algebras for a (finitary) monad $T$ on sets are a paradigmatic setting; they are used, for instance, in the generalized determinization framework of Silva et al. [29] and yield *coalgebraic language equivalence* [9] as a semantic equivalence of systems with a side effect provided by the monad $T$. In the category $\mathcal{C}$ of $T$-algebras, several notions of 'finite' object are natural to consider, and each of those yields an ensuing notion of 'finite' coalgebra: free objects on finitely many generators (*ffg* objects) yield precisely the coalgebras that are the target of generalized determinization; finitely presentable (*fp*) objects are the ones that can be presented by finitely many generators and relations and yield the rational fixed point; and finitely generated (*fg*) objects, i.e. those presented by finitely many generators (but possibly infinitely many relations). Taking the colimits of all coalgebras with ffg, fp, and fg carriers, respectively, yields three coalgebras $\varphi F$, $\varrho F$ and $\vartheta F$ which, under suitable assumptions on $F$, are all fixed

<footnote>* Supported by Deutsche Forschungsgemeinschaft (DFG) under project MI 717/5-1</footnote>
points of $F$ [2, 23, 33]. Our present paper is devoted to studying the fixed point $\varphi F$, which we call the locally ffg fixed point of $F$. For a finitary endofunctor $F$ preserving surjective and non-empty injective morphisms in $\mathcal{C}$, the three fixed points are related (to the terminal coalgebra $\nu F$) as shown in the picture below:

$$ \varphi F \to \varrho F \to \vartheta F \to \nu F, \qquad (1.1) $$

where $\to$ denotes a quotient coalgebra and $\mapsto$ a subcoalgebra. The three right-hand fixed points are characterized by a universal property both as a coalgebra and (inverting their coalgebra structure) as an algebra [2, 18, 23]; see [33] for one uniform proof. We recall this in more detail in Section 2.4.

The main contribution of this paper is a new characterization of the locally ffg fixed point $\varphi F$ by a universal property as an algebra. As already observed by Urbat [33], as a coalgebra, $\varphi F$ does not satisfy the expected finality property. A simple initiality property of $\varphi F$ as an algebra was recently established by Milius [20]. Here we go a step further and introduce the notion of an ffg-Elgot algebra (Section 4), which is an algebra for $F$ equipped with an operation that allows to take solutions of effectful iterative equations (see Remark 4.5) subject to two natural axioms. These axioms are inspired by and closely related to the axioms of (ordinary) Elgot algebras [1], which we recall in Section 3. We then prove that $\varphi F$ is the initial ffg-Elgot algebra (Theorem 4.11).

In addition, we study the construction of free ffg-Elgot algebras. In the case of ordinary Elgot algebras, it was shown in [1] that the parametrized rational fixed point $\varrho(F(-) + Y)$ is a free Elgot algebra on $Y$. In addition, the category of Elgot algebras is the Eilenberg-Moore category for the corresponding monad on $\mathcal{C}$. In the present paper, we first prove that free ffg-Elgot algebras exist on every object $Y$ of $\mathcal{C}$. But is it true that the free ffg-Elgot algebra on $Y$ is $\varphi(F(-) + Y)$? We do not know the answer for arbitrary objects $Y$, but if $Y$ is a free $T$-algebra (on a possibly infinite set of generators), the answer is affirmative (Theorem 4.15).

Finally, we prove that the category of ffg-Elgot algebras is monadic over $\mathcal{C}$, i.e. ffg-Elgot algebras are precisely the Eilenberg-Moore algebras for the monad that assigns to a given object $Y$ of $\mathcal{C}$ its free ffg-Elgot algebra (Theorem 4.16).

# 2 Preliminaries

## 2.1 Varieties and 'Finite' Algebras

Throughout the paper we will work with a (finitary, many-sorted) variety $\mathcal{C}$ of algebras. Equivalently, $\mathcal{C}$ is the category of Eilenberg-Moore algebras for a finitary monad $T$ on the category $\mathbf{Set}^S$ of $S$-sorted sets [6]. We will speak about objects of $\mathcal{C}$ (rather than algebras for $T$) and reserve the word 'algebra' for algebras for an endofunctor on $\mathcal{C}$. All the usual categories of algebraic structures and their homomorphisms are varieties: monoids, (semi-)groups, rings, vector spaces over a fixed field, modules for a (semi-)ring, positive convex algebras, join-semilattices, Boolean algebras, distributive lattices, and many others. In each case, the corresponding monad $T$ assigns to a set the free object on it, e.g. $TX = X^*$
for monoids, the finite power-set monad $T = \mathcal{P}_f$ for join-semilattices, and the subdistribution monad $\mathcal{D}$ for positive convex algebras, etc.

As mentioned in the introduction, every variety $\mathcal{C}$ of algebras comes with three natural notions of 'finite' objects, each of which admits a neat category-theoretic characterization (see [6]):

**Finitely presentable objects** (fp objects, for short) can be presented by finitely many generators and relations. An object $X$ is fp iff the covariant hom-functor $\mathcal{C}(X, -): \mathcal{C} \to \mathbf{Set}$ is finitary, i.e. it preserves filtered colimits.<fnref n="3" /> We denote by $\mathcal{C}_{fp}$ the full subcategory of $\mathcal{C}$ given by all fp objects. In our proofs we will use the well-known fact that every object $X$ is the filtered colimit of the canonical diagram $\mathcal{C}_{fp}/X \to \mathcal{C}$, i.e. objects in the diagram scheme are morphisms $P \to X$ in $\mathcal{C}$ with P fp.

**Finitely generated objects** (fg objects, for short) are presented by finitely many generators but, possibly, infinitely many relations. An object $X$ is fg iff $\mathcal{C}(X, -)$ preserves filtered colimits with monic connecting morphisms. Hence, every fp object is fg but not conversely. In fact, the fg objects are precisely the (regular) quotients of the fp objects [6, Proposition 5.22].

**Free finitely generated objects** (ffg objects, for short) are the objects $(TX_0, \mu_{X_0})$ where $X_0$ is a finite $S$-sorted set (i.e. the coproduct of all components $X_s$, $s \in S$ is finite). An object $X$ is a split quotient of an ffg object iff $\mathcal{C}(X, -)$ preserves sifted colimits [6, Corollary 5.14]. Recall from [6] that sifted colimits are more general than filtered colimits: a sifted colimit is a colimit of a diagram $D: \mathcal{D} \to \mathcal{C}$ whose diagram scheme $\mathcal{D}$ is a sifted category, which means that finite products commute with colimits over $\mathcal{D}$ in $\mathbf{Set}$. For instance, every filtered category and every category with finite coproducts is sifted, see [6, Example 2.16].

The category $\mathcal{C}$ is cocomplete and the forgetful functor $\mathcal{C} \to \mathbf{Set}^S$ preserves and reflects sifted colimits, that is, sifted colimits in $\mathcal{C}$ are formed on the level of underlying sets [6, Proposition 2.5].

A finitely cocomplete category has sifted colimits if and only if it has filtered colimits and reflexive coequalizers, and, moreover a functor preserves sifted colimits if and only if it preserves filtered colimits and reflexive coequalizers [5].

We denote by $\mathcal{C}_{fg}$ the full subcategory of ffg objects of $\mathcal{C}$. Analogously to the corresponding result for fp objects, every object $X$ is a sifted colimit of the canonical diagram $\mathcal{C}_{fg}/X \to \mathcal{C}$; this follows from [6, Proposition 5.17].

## 2.2 Relation between the object classes.

We already mentioned that every fp object is fg (but not conversely, in general). Clearly, every ffg object is fg, but not conversely in general. So, in general, we have full embeddings

$$ \mathcal{C}_{fg} \stackrel{\neq}{\hookrightarrow} \mathcal{C}_{fp} \stackrel{\neq}{\hookrightarrow} \mathcal{C}_{fg}. $$

<footnote n="3">³ These are colimits of diagrams $D: \mathcal{D} \to \mathcal{C}$ where $\mathcal{D}$ is filtered, i.e. every finite subdiagram has a cocone in $\mathcal{D}$.</footnote>
In rare cases, all three object classes coincide; e.g. in **Set** (considered as a variety) and the category of vector spaces over a field.

In addition to those examples, the equation $\mathcal{C}_{fg} = \mathcal{C}_{fp}$ holds true, for example, for all locally finite varieties (i.e. where ffg objects are carried by finite sets), for positive convex algebras [30], commutative monoids [14, 28], abelian groups, and more generally, in any category of (semi-)modules for a semiring $\mathbb{S}$ that is *Noetherian* in the sense of Ésik and Maletti [12], i.e. every subsemimodule of an fg semimodule is fg itself. For example, the following semirings are Noetherian: every finite semiring, every field, every principal ideal domain such as the ring of integers and therefore every finitely generated commutative ring by Hilbert's Basis Theorem. The tropical semiring $(\mathbb{N} \cup \{\infty\}, \min, +, \infty, 0)$ is not Noetherian [11]. The usual semiring of natural numbers is also not Noetherian, but for the category of $\mathbb{N}$-semimodules (= commutative monoids), $\mathcal{C}_{fp} = \mathcal{C}_{fg}$ still holds.

## 2.3 Functors and Liftings

We will consider coalgebras for functors $F$ on the variety $\mathcal{C}$. In many cases $F$ is a *lifting* of a set functor, i.e. we have functor $F_0: \text{Set}^S \to \text{Set}^S$ such that $F_0 \cdot U = U \cdot F$, where $U: \mathcal{C} \to \text{Set}^S$ is the forgetful functor. It is well-known [7,15] that liftings of a given functor $F_0$ on $\text{Set}^S$ to $\mathcal{C}$, the variety given by the monad $T$, are in bijective correspondence with distributive laws of the monad $T$ over the functor $F_0$. It was observed by Turi and Plotkin [27] that a final coalgebra for $F_0$ lifts to a final coalgebra for the lifting $F$, and this is then the final *bialgebra* for the corresponding distributive law.

Coalgebras for lifted functors are significant for us because the targets of *finite* coalgebras $X$ under *generalized determinization* [29] are precisely those coalgebras for the lifting $F$ carried by ffg objects $TX$. In more detail, generalized determinization is the process of turning a given coalgebra $c: X \to F_0TX$ in $\text{Set}^S$ into a coalgebra for the lifting $F$: one uses the freeness of $TX$ and the fact that $FTX$ is a $T$-algebra to extend $c$ to a $T$-algebra homomorphism $c^*: TX \to FTX$. The *coalgebraic language semantics* [9] of $(X, c)$ is then the final semantics of $c^*$ in $\mathcal{C}$. The classical instance of this is the language semantics of non-deterministic automata considered as coalgebras $X \to \{0,1\} \times (\mathcal{P}_f X)^\Sigma$; here the generalized determinization with $T = \mathcal{P}_f$ and $F = \{0,1\} \times X^\Sigma$ on $\text{Set}$ is the well-known subset construction from automata theory.

## 2.4 Four Fixed Points

Let us now consider a finitary endofunctor $F: \mathcal{C} \to \mathcal{C}$ on our variety. Then we know that $F$ has a terminal coalgebra [4], which we denote by $\nu F$. Its coalgebra structure $\nu F \to F(\nu F)$ is an isomorphism by Lambek's lemma [17], and so $\nu F$ is a fixed point of $F$.

There are three more fixed points of $F$ obtained from 'finite' coalgebras, where 'finite' can mean each of the three notions discussed in the previous subsection. More precisely, we consider the full subcategories of the category
in $\mathbf{Coalg}_{fg} F$; and (b) as an algebra, $\vartheta F$ is the initial fg-iterative algebra for $F$, where fg-iterative is simply the variation of iterative where the domain object of $e: X \to FX + A$ is required to be fg in lieu of fp. Moreover, $\vartheta F$ always is a subcoalgebra of $\nu F$ [23, Theorem 3.10] and thus fully abstract w.r.t. behavioral equivalence.

*The locally ffg fixed point* is the coalgebra $\varphi F$. Recently, Urbat [33] has proved that $\varphi F$ is indeed a fixed point of $F$, provided that $F$ preserves sifted colimits. Actually, he defined $\varphi F$ as the colimit of all $F$-coalgebras whose carrier is a split quotient of an ffg object. However, this is the same colimit as the one we use above. Moreover, loc. cit. provides a general framework that allows to prove that all four coalgebras $\varrho F$, $\vartheta F$, $\vartheta F$ and $\nu F$ are fixed points by one uniform proof. Also, a uniform proof of the universal properties of $\varrho F$, $\vartheta F$ and $\nu F$ is given.

Somewhat surprisingly, the coalgebra $\varphi F$ fails to have the finality property w.r.t. to coalgebras in $\mathbf{Coalg}_{ffg} F$: Urbat [33, Example 4.12] gives an example of a coalgebra for the identity functor on the category $\mathcal{C}$ of algebras with one unary operation (and no equations) that admits two coalgebra homomorphisms into $\varphi F$; see Example 2.2 below. This also shows that $\varphi F$ cannot have a universal property as some kind of iterative algebra (i.e. where solutions are unique).

*Relations between the Fixed Points.* Recall that a *quotient* of a coalgebra is represented by a coalgebra homomorphism carried by a regular epimorphism (= surjective algebra morphism) in $\mathcal{C}$. Suppose we have a finitary functor $F$ on $\mathcal{C}$ preserving surjective and non-empty injective morphisms.<fnref n="4" /> Then the subcoalgebra $\vartheta F$ of $\nu F$ is a quotient of $\varrho F$, which in turn is a quotient of $\varphi F$ [21, 22]; see (1.1). Whenever, $\mathcal{C}_{fp} = \mathcal{C}_{fg}$, we clearly have $\mathbf{Coalg}_{fp} F = \mathbf{Coalg}_{fg} F$ and hence $\varrho F \cong \vartheta F$ (i.e. $\varrho F$ is fully abstract w.r.t. behavioral equivalence), and if $\mathcal{C}_{fp} = \mathcal{C}_{fg} = \mathcal{C}_{ffg}$ then those two coincide with $\varphi F$ as well. Moreover, Milius [21] introduced the notion of a *proper functor* (generalizing the notion of a proper semiring of Ésik and Maletti [11]) and proved that a functor $F$ is proper if and only if the three fixed points coincide, i.e. the picture (1.1) collapses to $\varphi F \cong \varrho F \cong \vartheta F \hookrightarrow \nu F$. Loc. cit. also shows that on a variety $\mathcal{C}$ where fg objects are closed under taking kernel pairs, every endofunctor mapping kernel pairs to weak pullbacks in $\mathbf{Set}$ is proper [21, Proposition 3.18].<fnref n="5" />

*Instances of the three fixed points* have mostly been considered for proper functors (where the three are the same, e.g. for functors on $\mathbf{Set}$), or else on algebraic categories where $\mathcal{C}_{fp} = \mathcal{C}_{fg}$ (where the rational and locally finite fixed points coincide). For example, regular languages for the automaton functor $2 \times (-)^\Sigma$ on $\mathbf{Set}$; rational formal power series for the functor $\mathbb{S} \times (-)^\Sigma$ on $\mathbb{S}$-semimodules (whenever

<footnote n="4">⁴ These are mild assumptions; e.g. if $\mathcal{C}$ is single-sorted and $F$ a lifting of a set functor, then the conditions are fulfilled.</footnote>

<footnote n="5">⁵ Note that these conditions are fulfilled in particular by every locally finite variety and every category of semirings for a Noetherian semiring and any lifted endofunctor whose underlying $\mathbf{Set}$ functor preserves weak pullbacks.</footnote>
$\mathbb{S}$ is a proper semiring the three fixed points coincide); rational (a.k.a. regular) $\Sigma$-trees for the polynomial functor on Set associated to the signature $\Sigma$; eventually periodic and rational streams for the functor $k \times (-)$ on Set and vector spaces over the field $k$, respectively; the behaviors of probabilistic automata modelled as coalgebras for $[0, 1] \times (-)^\Sigma$ on the category of positive convex algebras (that this functor is proper was recently proved by Sokolova and Woracek [31]); finally, (deterministic) context-free languages and constructively $\mathbb{S}$-algebraic formal power-series (the weighted counterpart of context-free languages) [23]. Note that the last two examples are instances of the locally finite fixed point $\vartheta F$, but a description of $\varphi F$ and $\varrho F$ is unknown.

**Remark 2.1.** The rational and locally finite fixed points are defined and studied more generally than in the present setting, namely for finitary functors $F$ on a locally finitely presentable category $\mathcal{C}$ (see Adámek and Rosický [4] for an introduction to locally presentable categories). The following are instances of $\varrho F$ and $\vartheta F$ for $F$ on a locally finitely presentable category $\mathcal{C}$: (a) Courcelle’s algebraic trees [10] as proved in [23]; (b) rational $\lambda$-trees (modulo $\alpha$-equivalence) for a functor on the category of presheaves over finite sets [3] or for a related functor on the category of nominal sets [25]; more generally, (c) rational trees over an arbitrary binding signature (see Fiore et al. [13]) as proved in [24]. Again, (a) is an instance of the locally finite fixed point $\vartheta F$ but a description of the rational fixed point is unknown. In the setting of general locally finitely presentable categories, there is no analogy to $\varphi F$, of course.

We now present a new example where only $\varphi F$ is interesting but the other three fixed points are trivial.

**Example 2.2.** We consider the monad $T$ on Set whose algebras are the algebras with one unary operation $u$ (with no equation):

$$TX = \mathbb{N} \times X \quad \text{with} \quad u(n, x) = (n + 1, x).$$

The functor $F$ is the identity functor $\mathbb{1d}$ on the category $\mathcal{C} = \mathbf{Set}^T$. The final coalgebra for $\mathbb{1d}$ is (lifted from Set and therefore is) the trivial algebra on 1 with $\mathbb{1d}_1$ as coalgebra structure. Since 1 is clearly finitely presented by one generator $x$ and the relation $u(x) = x$, both of the diagrams $\mathbf{Coalg}_{\mathbb{fp}} \mathbb{1d}$ and $\mathbf{Coalg}_{\mathbb{fg}} \mathbb{1d}$ have a terminal object which is then their colimit, whence $\varrho \mathbb{1d} \cong \vartheta \mathbb{1d} \cong 1$.

However, $\varphi \mathbb{1d}$ is non-trivial and interesting: an ffg-coalgebra $TX \xrightarrow{\gamma} TX$ may be viewed (by restricting it to its generators in $X$) as obtained by generalized determinization of an $FT$-coalgebra with $F = \mathbb{1d}$ on Set, i.e. a map $X \xrightarrow{\langle o, \delta \rangle} \mathbb{N} \times X$ that we call *stream coalgebra*. Given a state $x \in X$, we call the sequence of natural numbers

$$(o(x), o(\delta(x)), o(\delta^2(x)), \dots)$$

the *stream generated by* $x$. Since $X$ is finite, this stream is eventually periodic, i.e. of the form $s = s_0 s_1^\omega$ for finite lists $s_0$ and $s_1$ of natural numbers. (Here $(-)^\omega$ means infinite iteration.) Two eventually periodic streams $s = s_0 s_1^\omega$ and $t = t_0 t_1^\omega$
with $s_1 = (s_{1,0}, \dots, s_{1,p-1})$ and $t_1 = (t_{1,0}, \dots, t_{1,q-1})$ are called equivalent if one has

$$q \cdot \sum_{i<p} s_{1,i} = p \cdot \sum_{j<q} t_{1,j} \qquad (2.2)$$

i.e. the entries of the two lists $s_1^q$ and $t_1^p$ of length $p \cdot q$ have the same sum. For instance, the streams

$$s = (1, 2, 7, 4)(1, 3, 2)^\omega = (1, 2, 7, 4, 1, 3, 2, 1, 3, 2, 1, 3, 2, \dots)$$

and

$$t = (5, 6)(0, 4)^\omega = (5, 6, 0, 4, 0, 4, 0, 4, 0, 4, \dots)$$

are equivalent. Note that the above notion of equivalence is well-defined, i.e. not depending on the choice of the finite lists $s_0, s_1$ and $t_0, t_1$ in the representation of $s$ and $t$. In fact, given alternative representations $s = \overline{s_0s_1^q}$ and $t = \overline{t_0t_1^\omega}$ with $\overline{s_1} = (\overline{s_{1,0}}, \dots, \overline{s_{1,p-1}})$ and $\overline{t_1} = (\overline{t_{1,0}}, \dots, \overline{t_{1,q-1}})$, the lists $s_1^p$ and $\overline{s_1^q}$ are equal up to cyclic shift, as are the lists $t_1^q$ and $\overline{t_1^q}$. Therefore from (2.2) it follows that

$$\overline{q} \cdot q \cdot p \cdot \sum_{i<\overline{p}} \overline{s}_{1,i} = \overline{q} \cdot q \cdot \overline{p} \cdot \sum_{i<p} s_{1,i} = \overline{q} \cdot \overline{p} \cdot p \cdot \sum_{j<q} t_{1,j} = \overline{p} \cdot p \cdot q \cdot \sum_{j<\overline{q}} \overline{t}_{1,j}.$$

Dividing by $p \cdot q$ yields

$$\overline{q} \cdot \sum_{i<\overline{p}} \overline{s}_{1,i} = \overline{p} \cdot \sum_{j<\overline{q}} \overline{t}_{1,j},$$

as required.

**Lemma 2.3.** (a) The coalgebra $\phi_{\mathrm{ld}}$ is carried by the set of equivalence classes of eventually periodic streams. The unary operation and the coalgebra structure are both given by $\mathrm{id}: \phi_{\mathrm{ld}} \to \phi_{\mathrm{ld}}$. (b) For any $\mathrm{id}$-coalgebra $(TX, \gamma_X)$ with $X$ finite, the colimit injection $\gamma_X^\# : TX \to \phi_{\mathrm{ld}}$ maps $(m, x) \in TX$ to the equivalence class of the stream generated by $x$.

*Proof.* (1) We first show that the morphisms $(-)^\#$ form a cocone. Given an ffg-coalgebra $(TX, \gamma_X)$ and elements $(m, x), (n, y) \in TX$ with $\gamma_X(m, x) = (n, y)$, the stream generated by $y$ is the tail of the stream generated by $x$, and thus the two streams are equivalent. This shows that $\gamma_X^\#$ is a coalgebra homomorphism.

To show that the morphisms $(-)^\#$ form a compatible family, suppose that $h: (TX, \gamma_X) \to (TY, \gamma_Y)$ is a homomorphism of ffg-coalgebras, and let $(m, x) \in TX$ and $(n, y) \in TY$ with $h(m, x) = (n, y)$ be given. We need to show that the streams generated by $x$ and $y$ are equivalent. Denote by

$$(m_j, x_j) := \gamma_X^j(m, x) \quad \text{and} \quad (n_j, y_j) := \gamma_Y^j(n, y) \quad (j = 0, 1, 2, \dots) \qquad (2.3)$$

the states reached from $(m, x)$ and $(n, y)$ after $j$ steps. Since $h$ is a coalgebra homomorphism, one has $h(m_j, x_j) = (n_j, y_j)$ for all $j$. Since $X$ is finite, there
exist natural numbers $k \ge 0$ and $p > 0$ with $x_k = x_{k+p}$. Then the eventually periodic stream generated by $x$ is given by

$$ (m_1 - m_0, m_2 - m_1, \dots, m_k - m_{k-1}) (m_{k+1} - m_k, \dots, m_{k+p} - m_{k+p-1})^{\omega} $$

Since $h(m_k, x_k) = (n_k, y_k)$ and $h(m_{k+p}, x_{k+p}) = (n_{k+p}, y_{k+p})$, one has $y_k = y_{k+p}$, which implies that $y$ generates the stream

$$ (n_1 - n_0, n_2 - n_1, \dots, n_k - n_{k-1}) (n_{k+1} - n_k, \dots, n_{k+p} - n_{k+p-1})^{\omega} $$

To show that the streams generated by $x$ and $y$ are equivalent, it suffices to verify that $m_{k+p} - m_k = n_{k+p} - n_k$, as this entails that

$$ p \cdot \sum_{i<p} m_{k+i+1} - m_{k+i} = p \cdot (m_{k+p} - m_k) = p \cdot (n_{k+p} - n_k) = p \cdot \sum_{i<p} n_{k+i+1} - n_{k+i}. $$

To prove the desired equation, we compute

$$ \begin{aligned} (n_{k+p}, y_{k+p}) &= h(m_{k+p}, x_{k+p}) \\ &= h(m_{k+p}, x_k) \\ &= h(m_{k+p} - m_k + m_k, x_k) \\ &= (m_{k+p} - m_k + n_k, y_k) \end{aligned} $$

where the last equality uses that $h(m_k, x_k) = (n_k, y_k)$ and that $h$ is a morphism in $\mathcal{C}$. This implies $n_{k+p} = m_{k+p} - m_k + n_k$.

(2) We prove that the cocone $(-)^{\#}$ is a colimit cocone. Since sifted colimits in Coalgld are formed as in $\mathcal{C}$ and thus as in Set, it suffices to show that (i) the morphisms $\gamma_X^{\#}$ are jointly surjective and (ii) given ffg-coalgebras $(TX, \gamma_X)$ and $(TY, \gamma_Y)$ and two states $(m, x) \in TX$ and $(n, y) \in TY$ merged by $\gamma_X^{\#}$ and $\gamma_Y^{\#}$, there exists a zig-zag in Coalgfgld connecting the two states. Statement (i) is clear because finite stream coalgebras generate precisely the eventually periodic streams. For (ii), we adapt the argument of the first part of our proof and continue to use the notation (2.3). Since $X$ and $Y$ are finite, there exist natural numbers $k \ge 0$ and $p > 0$ with $x_k = x_{k+p}$ and $y_k = y_{k+p}$. As the streams generated by $x$ and $y$ are equivalent, one has $m_{k+p} - m_k = n_{k+p} - n_k$. Consider the ffg-coalgebra $(TZ, \gamma_Z)$ with $Z = \{z_0, z_1, \dots, z_{k+p-1}\}$, and $\gamma_Z$ defined by

$$ \gamma_Z(z_j) = (0, z_{j+1}) \quad (j < k + p - 1) \quad \text{and} \quad \gamma_Z(z_{k+p-1}) = (m_{k+p} - m_k, z_k). $$

Form the morphisms $g: TZ \to TX$ and $h: TZ \to TX$ given by

$$ g(z_j) = (m_j, x_j) \quad \text{and} \quad h(z_j) = (n_j, y_j) \quad (j < k + p). $$

Then $g$ and $h$ are coalgebra homomorphisms. Indeed, for $j < k + p - 1$ we have

$$ \begin{aligned} g(\gamma_Z(z_j)) &= g(0, z_{j+1}) && (\text{def. } \gamma_Z) \\ &= (m_{j+1}, x_{j+1}) && (\text{def. } g) \\ &= \gamma_X(m_j, x_j) && (\text{def. } m_{j+1}, x_{j+1}) \\ &= \gamma_X(g(z_j)) && (\text{def. } g) \end{aligned} $$
and moreover

$$
\begin{align*}
g(\gamma_Z(z_{k+p-1})) &= g(m_{k+p} - m_k, z_k) && (\text{def. } \gamma_Z) \\
&= (m_{k+p} - m_k + m_k, x_k) && (\text{def. } g) \\
&= (m_{k+p}, x_{k+p}) \\
&= \gamma_X(m_{k+p-1}, x_{k+p-1}) && (\text{def. } m_{k+p}, x_{k+1}) \\
&= \gamma_X(g(z_{k+p-1})) && (\text{def. } g)
\end{align*}
$$

and analogously for $h$. Thus we have constructed a zig-zag

$$
(TX, \gamma_X) \xleftarrow{g} (TZ, \gamma_Z) \xrightarrow{h} (TY, \gamma_Y)
$$

in $\mathrm{Coalg}_{\mathrm{fg}}$ld connecting $(m, x)$ and $(n, y)$, as required. $\square$

Observe that every non-empty ffg-coalgebra $(TX, \gamma_X)$ admits infinitely many coalgebra homomorphisms into $\phi_{\mathrm{ld}}$, for instance, any constant map into $\phi_{\mathrm{ld}}$ is one. This shows that, in general, the coalgebra $\phi_F$ is not final w.r.t. the coalgebras in $\mathrm{Coalg}_{\mathrm{fgg}} F$.

3 Recap: Elgot Algebras

In this section we briefly recall the notion of an Elgot algebra [1] and some key
results to contrast this with our subsequent development of ffg-Elgot algebras in
Section 4. Throughout this section we assume the endofunctor $F: \mathcal{C} \to \mathcal{C}$ to be
finitary.

**Definition 3.1.** An fp-equation is a morphism

$$
e: X \to FX + A,
$$

where $X$ is an fp object (of variables) and $A$ an arbitrary object of parameters.
Suppose that $A$ carries the structure of an $F$-algebra $a: FA \to A$. Then a
solution of $e$ in $A$ is a morphism $e^\dagger: X \to A$ such that the square (2.1) commutes.

**Notation 3.2.** We use the following notation for fp-equations:

(1) Given an fp-equation $e: X \to FX + A$ and a morphism $h: A \to B$ we have an fp-equation

$$
h \bullet e = (X \xrightarrow{e} FX + A \xrightarrow{FX+h} FX + B).
$$

(2) Given a pair of fp-equations $e: X \to FX + Y$ and $f: Y \to FY + Z$ we combine them into the following fp-equation

$$
e \bullet f = (X + Y \xrightarrow{[e, \mathrm{inr}]} FX + Y \xrightarrow{FX+f} FX + FY + Z \xrightarrow{\mathrm{can}+Z} F(X+Y) + Z),
$$

where can = [Finl, Finr]: FX + FY → F(X + Y) denotes the canonical
morphism.
**Definition 3.3.** An Elgot algebra is a triple $(A, a, \dagger)$ where $(A, a)$ is an $F$-algebra and $\dagger$ is an operation

$$ \frac{e: X \to FX + A}{e^\dagger: X \to A} $$

assigning to every fp-equation in $A$ a solution subject to the following two conditions:

(1) Weak Factoriality. Given a pair of equations $e: X \to FX + Z$, $f: Y \to FY + Z$, where $Z$ is an fp object, and a coalgebra homomorphism $m: X \to Y$ for $F(-)+Z$, then for every morphism $h: Z \to A$ we have $(h \bullet f)^\dagger \cdot m = (h \bullet e)^\dagger$:

$$ \begin{tikzcd} X \arrow[r, "e"] \arrow[d, "m"] & FX + Z \arrow[d, "Fm+Z"] \\ Y \arrow[r, "f"] & FY + Z \arrow[d, "Fm+Z"] \arrow[dl, "\dagger"'] \arrow[ur, "\dagger"'] \arrow[dl, "m"] \arrow[ur, "\dagger"'] \arrow[r, "A", "(h\bullet e)^\dagger"] \arrow[r, "(h\bullet f)^\dagger", "\dagger"] \arrow[dl, "m"] \arrow[ur, "\dagger"'] \arrow[dl, "(h\bullet f)^\dagger", "\dagger"] \end{tikzcd} \quad \text{for all } h: Z \to A. $$

(2) Compositionality. For every pair of fp-equations $e: X \to FX + Y$ and $f: Y \to FY + A$ we have

$$ (e \blacksquare f)^\dagger \cdot \mathrm{inl} = (f^\dagger \bullet e)^\dagger: X \to A. $$

**Remark 3.4.** Later we will need the following properties of $\bullet$ and $\blacksquare$:

(1) $t \bullet (s \bullet e) = (t \cdot s) \bullet e$ for every $e: X \to FX + A$, $s: A \to B$ and $t: B \to C$;

(2) $s \bullet (e \blacksquare f) = e \blacksquare (s \bullet f)$ for every $e: X \to FX + Y$, $f: Y \to FY + A$ and $s: A \to B$;

(3) $(e \blacksquare f) \blacksquare g = (\mathrm{inl} \bullet e) \blacksquare (f \blacksquare g)$ for every $e: X \to FX + Y$, $f: Y \to FY + Z$ and $g: Z \to FZ + V$.

For the proof of the first two see [1, Remark 4.6]. The remaining one is easy to prove by considering the three coproduct components of $X + Y + Z$ separately, we leave this as an easy exercise for the reader.

Note that, in lieu of weak functoriality, $\dagger$ previously [1] was required to satisfy (full) functoriality, i.e. given fp-equations $e: X \to FX + A$, $f: Y \to FY + A$ and a coalgebra homomorphism $m: (X, e) \to (Y, f)$ we have $f^\dagger \cdot m = e^\dagger: X \to A$. However, this makes no difference:

**Lemma 3.5.** *Functoriality and weak functoriality are equivalent properties of $\dagger$.*

*Proof.* Factoriality clearly implies Weak Factoriality. In order to prove the converse, let $e: X \to FX + A$, $f: Y \to FY + A$ be fp-equations, and let $m: (X, e) \to (Y, f)$ be a coalgebra morphism. Write $A$ is the filtered colimit of its canonical diagram $\mathcal{C}_{fp}/A$ (cf. Section 2.1). The functor $FX + (-)$ preserves filtered colimits, and so $FX + A$ is the filtered colimit of the diagram formed by all morphisms $FX + h: FX + Z \to FX + A$. Since $X$ is fp, the morphism
$e: X \to FX + A$ factors through one of these morphisms, i.e. there exists a morphism $h: Z \to A$ with $Z$ fp and $e': X \to FX + Z$ such that $e = h \bullet e'$:

<figure><img src="image_2.png" /></figure>

Similarly, we have a factorization of $f: Y \to FY + A$, and by filteredness of the diagram $\mathcal{C}_{fp}/A \to \mathcal{C}$ we can assume the same $h: Z \to A$ is used. Thus a morphism $f': Y \to FY + Z$ is given such that $h \bullet f' = (FY + h) \cdot f' = f$. We do not claim that $m$ is a coalgebra homomorphism from $(X, e')$ to $(Y, f')$. However, the corresponding equation holds when postcomposed by the colimit injection $FY + h$:

$$ \begin{align*} (FX + h) \cdot (Fm + Z) \cdot e' &= (Fm + A) \cdot (FX + h) \cdot e' \\ &= (Fm + A) \cdot e \\ &= f \cdot m \\ &= (FY + h) \cdot f' \cdot m. \end{align*} $$

Therefore there exists a morphism $h: Z' \to A$ with $Z'$ fp and a connecting morphism $z: Z \to Z'$ in $\mathcal{C}_{fp}/A$, i.e. $z$ satisfies $h' \cdot z = h$, such that $FY + z$ merges $(Fm + Z) \cdot e'$ and $f' \cdot m$. It follows that $m$ is a coalgebra homomorphism from $z \cdot e'$ to $z \cdot f'$:

<figure><img src="image_3.png" /></figure>

Indeed, the left-hand square commutes when postcomposed with $FY + z$; thus, since the upper and lower parts as well as the right-hand square commute, so does the outside, as desired. By weak functoriality, we thus conclude

$$ \begin{align*} f^{\dagger} \cdot m &= (h \bullet f')^{\dagger} \cdot m = ((h' \cdot z) \bullet f')^{\dagger} \cdot m = (h' \bullet (z \bullet f'))^{\dagger} \cdot m \\ &= (h' \bullet (z \bullet e'))^{\dagger} = ((h' \cdot z) \bullet e')^{\dagger} = (h \bullet e')^{\dagger} = e^{\dagger}. \quad \square \end{align*} $$

**Examples 3.6.** Let us recall a few examples of Elgot algebras [1].

(1) Iterative $F$-algebras (cf. Section 2.4): the operation $\dagger$ assigning to every equation its unique solution satisfies Compositionality and (Weak) Factoriality, see [1, 2.15–1.19]. It follows that $\varrho F$, $\vartheta F$ and $\nu F$ are Elgot algebras.
(2) Cpo enrichable algebras. Recall that a complete partial order (cpo, for short) is a partially ordered set having joins of $\omega$-chains. Cpos form a category CPO together with the continuous functions, i.e. functions preserving joins of $\omega$-chains. Let $F_0$: Set $\rightarrow$ Set be a functor having a locally continuous lifting $F$: CPO $\rightarrow$ CPO, i.e. a lifting such that the hom mappings CPO($X$, $Y$) $\rightarrow$ CPO($FX$, $FY$) are continuous. For example, every polynomial functor $F_\Sigma$ associated to the signature $\Sigma$ has a lifting to CPO.

Suppose further that $a: FA \rightarrow A$ is an algebra where $A$ is a CPO with a least element $\perp$ and $a$ is continuous. Then $A$ is an Elgot algebra w.r.t. the operation $\dagger$ assigning the least solution. More precisely, given an fp-equation $e: X \rightarrow FX + A$ (in Set) consider $X$ as a cpo with discrete order and let $e^\dagger: X \rightarrow A$ be the least fixed point of the continuous function

$$h \mapsto [a, A] \cdot (Fh + A) \cdot e$$

on the cpo of continuous functions from $X$ to $A$. For details see [1, 3.5-3.8].

(3) CMS enrichable algebras. A related example is based on complete metric spaces, i.e. metric spaces in which every Cauchy sequence has a limit. Here one considers the category CMS of complete metric spaces with distances in $[0, 1]$ and non-expanding maps, i.e. maps $f: X \rightarrow Y$ such that for every $x, x' \in X$ one has $d_Y(fx, fx') \le d_X(x, x')$. Let $F_0$: Set $\rightarrow$ Set have a locally contracting lifting to CMS, i.e. a lifting $F: CMS \rightarrow CMS$ such that there exists some $\varepsilon < 1$ such that for all $f, g: X \rightarrow Y$ in CMS one has

$$d_{X,Y}(f,g) \le \varepsilon d_{FX,FY}(Ff, Fg),$$

where $d_{X,Y}$ denotes the sup-metric on CMS($X$, $Y$). Again, polynomial set functors have locally contracting liftings to CMS.

Now suppose that $a: FA \rightarrow A$ is a non-empty algebra such that $A$ carries a complete metric space and $a$ is a non-expanding map. Then $A$ is iterative, whence an Elgot algebra. In fact, for every equation $e: X \rightarrow FX + A$ consider $X$ as a discrete metric space (i.e. all distances are 1) and consider the $\varepsilon$-contracting function

$$h \mapsto [a, A] \cdot (Fh + A) \cdot e$$

on CMS($X$, $A$). Then, by Banach's fixed point theorem, this function has a unique fixed point, viz. a unique solution of $e$. For details see [1, 2.8-2.11].

(4) As a concrete instance of the previous point one can obtain fractals as solutions of equations. For example, let $A$ be the set of closed subsets of the unit interval $[0, 1]$ equipped with the following binary operation:

$$(C, C') \mapsto \frac{1}{3}C \cup \left(\frac{1}{3}C' + \frac{2}{3}\right),$$

where $\frac{1}{3}C = \{\frac{1}{3}c | c \in C\}$ etc. Then $A$ is an algebra for $F_0X = X \times X$ on Set, and this $F_0$ has the locally contracting lifting $F(X, d) = (X \times X, \frac{1}{3}d_{\max})$,
where $d_{\max}$ denotes the usual maximum metric on the cartesian product. One sees that $A$ is an algebra for $F$ when equipped with the so-called Hausdorff metric. Hence, it is an Elgot algebra. For example, let $X = \{x\}$ and let $e: X \to FX + A$ be given by $e(x) = (x, x)$. Then $e^{\dagger}(x)$ is the well-known Cantor set.

The rational fixed point $\varrho F$ is, besides being the initial iterative $F$-algebra, also an initial Elgot algebra. Moreover, for every object $Y$, the rational fixed point $\varrho(F(-) + Y)$ is a free iterative algebra on $Y$. Thus, the object assignment $R: Y \mapsto \varrho(F(-) + Y)$ yields a monad on $\mathcal{C}$, and one obtains the following

**Theorem 3.7 ([1]).** The category of Eilenberg-Moore algebras for $R$ is isomorphic to the category of Elgot algebras for $F$.

Thus, in particular, $\varrho(F(-) + Y)$ is not only a free iterative algebra but also a free Elgot algebra on $Y$.

# 4 FFG-Elgot Algebras

The rest of our paper is devoted to studying the fixed point $\varphi F$, the colimit of all ffg-coalgebras for $F$, in its own right and establish a universal property of it as an algebra.

**Assumption 4.1.** Throughout the rest of the paper we assume that $\mathcal{C}$ is a variety of algebras and that $F: \mathcal{C} \to \mathcal{C}$ is an endofunctor preserving sifted colimits.

**Examples 4.2.** (1) For the monad $T$ representing $\mathcal{C}$, all functors that are liftings of finitary set functor $F_0$ (i.e., with a distributive law of $T$ over $F_0$) preserve sifted colimits. Indeed, finitary set functors $F_0$ preserve all sifted colimits [6, Proposition 6.30]. Since $\mathcal{C}$ is cocomplete and the forgetful functor $U: \mathcal{C} \to \mathbf{Set}$ preserves and reflects sifted colimits, it follows that every lifting of $F_0$ preserves sifted colimits, too. The following examples are not liftings of set functors.

(2) The functor $FX = X + X$, where $+$ denotes the coproduct of $\mathcal{C}$ preserves sifted colimits. More generally, every coproduct of sifted colimit preserving functors preserves them too. Similarly, for finite products of sifted colimit preserving functors. Thus, all polynomial functors on $\mathcal{C}$ preserve sifted colimits.

(3) Let $\mathcal{C}$ is an entropic variety, i.e. such that the usual tensor product makes it symmetric monoidal closed. (Examples include sets, vector spaces, join-semilattices, or abelian groups.) Then the functor $FX = X \otimes X$ preserves sifted colimits. To see this, it suffices to show that (a) $F$ is finitary and (b) it preserves reflexive coequalizers (see [5]). First note that since $\mathcal{C}$ is symmetric monoidal closed, we know that each functor $X \otimes -$ and $- \otimes X$ is a left adjoint and therefore preserves all colimits.

Ad (a). Suppose that $D: \mathcal{D} \to C$ is a filtered diagram with colimit injections $a_d: Dd \to A$ for $d \in \mathcal{D}$. We need to prove that all $a_d \otimes a_d: Dd \otimes Dd \to A \otimes A$
form a colimit cocone. That is, for every morphism $f: X \to A \otimes A$ with $X$ fp, (i) there exists some $d \in \mathcal{D}$ and $g: X \to Dd \otimes Dd$ with $(a_d \otimes a_d) \cdot g = f$ and (ii) given $g, h: X \to Dd \otimes Dd$ that yield $f$ in this way, there exists a morphism $m: d \to d'$ in $\mathcal{D}$ such that $Dm \otimes Dm$ merges $g$ and $h$.

To prove (i), we use that $- \otimes A$ is finitary to obtain some $d \in \mathcal{D}$ and $f': X \to A \otimes Dd$ with $(A \otimes a_d) \cdot f' = f$. Now use that $Dd \otimes -$ is finitary to obtain $d' \in \mathcal{D}$ and $f'': X \to Dd \otimes Dd'$ with $(Dd \otimes a_{d'}) \cdot f'' = f'$. Since $\mathcal{D}$ is filtered, we can choose morphisms $m: d \to \bar{d}$ and $n: d' \to \bar{d}$ in $\mathcal{D}$. Let $g = (Dm \otimes Dn) \cdot f''$. Then we have

$$ (a_{\bar{d}} \otimes a_{\bar{d}}) \cdot g = (a_{\bar{d}} \otimes a_{\bar{d}}) \cdot (Dm \otimes Dn) \cdot f'' = (a_d \otimes a_{d'}) \cdot f'' \\ = (a_d \otimes A) \cdot (Dd \otimes a_{d'}) \cdot f'' = (a_d \otimes A) \cdot f' = f $$

as desired.

For (ii), use first that $- \otimes A$ is finitary and choose some morphism $o: d \to d'$ such that

$$ (Do \otimes A) \cdot ((Dd \otimes a_d) \cdot g) = (Do \otimes A) \cdot ((Dd \otimes a_d) \cdot h). $$

It follows that $(Dd' \otimes a_d)$ merges $(Do \otimes Dd) \cdot g$ and $(Do \otimes Dd) \cdot h$. Now use that $Dd' \otimes -$ is finitary and choose a morphism $p: d \to d''$ in $\mathcal{D}$ such that $(Dd' \otimes Dp)$ also merges those two morphisms. Finally, use that $\mathcal{D}$ is filtered to choose two morphisms $q: d' \to \bar{d}$ and $r: d'' \to \bar{d}$ such that $q \cdot o = r \cdot p$, and let us call this last morphism $m: d \to \bar{d}$. It is then easy to see that $Dm \otimes Dm$ merges $g$ and $h$:

$$ \begin{align*} (Dm \otimes Dm) \cdot g &= (D(q \cdot o) \otimes D(r \cdot p)) \cdot g = (Dq \otimes Dr) \cdot (Do \otimes Dp) \cdot g \\ &= (Dq \otimes Dr) \cdot (Dd' \otimes Dp) \cdot (Do \otimes Dd) \cdot g \\ &= (Dq \otimes Dr) \cdot (Dd' \otimes Dp) \cdot (Do \otimes Dd) \cdot h \\ &= (Dm \otimes Dm) \cdot h. \end{align*} $$

Ad (b). Let $f, g: A \to B$ be, and let $c: B \to C$ be their coequalizer. Use that all functors $- \otimes X$ and $X \otimes -$ preserve coequalizers to see that in the following diagram, whose parts commute in the obvious way, all rows and columns are coequalizers:

<figure><img src="image_4.png" /></figure>
By the ‘3-by-3 lemma’ [16, Lemma 0.17], it follows that the diagonal yields a coequalizer too, i.e., $c \otimes c$ is a coequalizer of the pair $f \otimes f, g \otimes g$ as desired.

(4) Combining the previous argument with induction, we see that sifted colimit preserving functors on an entropic variety $\mathcal{C}$ are stable under finite tensor products. Thus, all tensor-polynomial functors on $\mathcal{C}$ preserve sifted colimits.

Under our assumptions we know that $\varphi F$ is a fixed point of $F$ and we will henceforth denote the inverse of its coalgebra structure by $t: F(\varphi F) \to \varphi F$.

**Definition 4.3.** By an ffg-equation is meant a morphism $e: X \to FX + A$ where $X$ is an ffg object. An ffg-Elgot algebra is a triple $(A, a, \dagger)$ where $(A, a)$ is an $F$-algebra and $\dagger$ is an operation

$$ \frac{e: X \to FX + A}{e^{\dagger}: X \to A} $$

assigning to every ffg-equation in $A$ a solution and satisfying Weak Factoriality 3.3(1) and Compositionality 3.3(2) with $X, Y$ and $Z$ restricted to ffg objects.

**Remark 4.4.** Note that in categories where fp objects are ffg, e.g. in the category of sets or vector spaces, (ordinary) Elgot algebras and ffg-Elgot algebras are the same concept. However, in the present setting this may not be the case. Moreover, we do not know whether, for ffg-Elgot algebras, weak functoriality implies functoriality. Moreover, the proofs of our main results (in particular Proposition 4.8 and Theorem 4.12) do not work when weak functoriality is replaced by functoriality.

**Remark 4.5.** In the case where $F: \mathbf{Set}^T \to \mathbf{Set}^T$ is a lifting of a functor $F_0: \mathbf{Set} \to \mathbf{Set}$ (via a distributive law $\lambda$), then an $F$-algebra is given by a set $A$ equipped with both a $T$-algebra structure $\alpha: TA \to A$ and an $F_0$-algebra structure $a: F_0A \to A$ such that $a$ is a $T$-algebra homomorphism, i.e. one has $\alpha \cdot Ta = a \cdot F\alpha \cdot \lambda_A$. Morphisms of $F$-algebras are those maps that are both $T$-algebra and $F_0$-algebra homomorphisms. Now one may think of ffg-equations and their solutions as modelling *effectful iteration*. Indeed, let $X_0$ be a finite set of variables and consider any map

$$ e_0: X_0 \to T(F_0X_0 + A). $$

Then this may be regarded as a system of recursive equations with variables $X_0$ and parameters in $A$, where for any recursive call a side effect in $T$ might happen. If $(A, \alpha, a)$ is an $F$-algebra, a solution to such a recursive system should assign to each variable in $X_0$ an element of $A$, i.e. we have a map $e_0^\dagger: X_0 \to A$, such that the square below commutes (here we write $+$ for disjoint union and $\oplus$ for the coproduct in $\mathcal{C}$, which may be different):

<figure><img src="image_5.png" /></figure>
**Lemma 4.10.** *Morphisms of ffg-Elgot algebras are F-algebra homomorphisms.*

Note that the converse fails in general. In fact, [1, Example 4.4] exhibits an (fgf-)Elgot algebra for the identity functor on Set and an algebra morphism on it which is not solution-preserving.

**Theorem 4.11.** *The triple $(\varphi F, t, \dagger)$ is the initial ffg-Elgot algebra for F.*

*Proof (Sketch).* Let $(A, a, \ddagger)$ be an ffg-Elgot algebra. We obtain a cocone over the diagram

$$ \mathrm{Coalg}_{\mathrm{fgf}} F \to \mathrm{Coalg} F \xrightarrow{U} \mathscr{C} $$

(where $U$ is the forgetful functor) as follows: to every ffg-coalgebra $c: C \to FC$ assign the solution

$$ (i_A \bullet c)^{\ddagger}: C \to A $$

of $i_A \bullet c: C \to FC + A$, where $i_A: 0 \to A$ is the unique morphism. Thus there exists a unique morphism $h: \varphi F \to A$ in $\mathscr{C}$ such that the triangle below commute for every ffg-coalgebra $c: C \to FC$:

<figure><img src="image_6.png" /></figure>

One then shows that the morphism $h$ is solution-preserving and is the unique such morphism. $\square$

The following result is the key to constructing free ffg-Elgot algebras. In the case where $\mathscr{C}_{\mathrm{fgf}} = \mathscr{C}_{\mathrm{fp}}$, this yields a new result about ordinary Elgot algebras.

**Theorem 4.12.** Let $a: FA \to A$ be an F-algebra and let $Y$ be a free object of $\mathscr{C}$. For any morphism $h: Y \to A$, there is a bijective correspondence between

(i) solution operators $\dagger$ such that $(A, a, \dagger)$ is an ffg-Elgot algebra for F, and

(ii) solution operators $\ddagger$ such that $(A, [a, h], \ddagger)$ is an ffg-Elgot algebra for $F(-) + Y$.

*Proof (Sketch).* (1) Given an ffg-Elgot algebra $(A, a, \dagger)$ for F, we define a solution operator $\ddagger$ w.r.t. $F(-) + Y$ as follows. For any ffg-equation $e: X \to FX + Y + A$, let

$$ e_h \equiv X \xrightarrow{e} FX + Y + A \xrightarrow{FX+[h,A]} FX + A $$

and put

$$ e^{\ddagger} := e_h^{\dagger}. $$

Then one can prove that $(A, [a, h], \ddagger)$ is an ffg-Elgot algebra for $F(-) + Y$. (In order to verify weak functoriality, the assumption that $Y$ is free is critical.)
(2) Conversely, given an ffg-Elgot algebra $(A, [a, h], \ddag)$ for $F(-)+Y$, we define a solution operator $\dagger$ w.r.t. $F$ as follows. For any ffg-equation $e: X \to FX + A$, let

$$ \bar{e} \equiv X \xrightarrow{e} FX + A \xrightarrow{\text{inl}+A} FX + Y + A $$

and put

$$ e^\dagger := \bar{e}^\ddag. $$

Then one can prove that $(A, a, \dagger)$ is an ffg-Elgot algebra.

(3) Finally, one shows that the two passages $\dagger \mapsto \ddag$ and $\ddag \mapsto \dagger$ are mutually inverse. $\square$

For the forgetful functor of ffg-Elgot algebras

$$ U_F: \text{fgg-Elgot} F \to \mathscr{C} $$

recall that the slice category $Y/U_F$ has as objects all morphisms $y: Y \to U_F(A, a, \dagger)$, and morphisms into $y': Y \to U_F(B, b, \ddag)$ are the solution-preserving morphisms $p: (A, a, \dagger) \to (B, b, \ddag)$ with $p \cdot y = p'$. Denote by $\pi: Y/U_F \to \mathscr{C}$ the projection functor.

**Corollary 4.13.** For every free object $Y$ of $\mathscr{C}$, there is an isomorphism $I$ of categories such that

$$ U_{F(-)+Y} = (\text{fgg-Elgot}(F(-) + Y) \xrightarrow{I} Y/U_F \xrightarrow{\pi} \mathscr{C}). $$

It is given by $(A, [a, h], \ddag) \mapsto (h: Y \to U_F(A, a, \dagger))$.

**Construction 4.14.** For any object $Y$ of $\mathscr{C}$ denote by $\Phi Y$ the colimit of all ffg-coalgebras for $F(-)+Y$, that is, $\Phi Y = \varphi(F(-)+Y)$. Its coalgebra structure is invertible, and we denote by $t_Y: F\Phi Y \to \Phi Y$ and $\eta_Y: Y \to \Phi Y$ the components of its inverse.

The $F$-algebra $(\Phi Y, t_Y)$ is endowed with a canonical solution operation $\dagger$: given an ffg-equation $e: X \to FX + \Phi Y$, put $\bar{e} \equiv X \xrightarrow{e} FX + \Phi Y \xrightarrow{FX+\text{inl}} FX + Y + \Phi Y$. This ffg-equation for $F(-)+Y$ has a solution $\bar{e}^\ddag: X \to \Phi Y$ in the ffg-Elgot algebra $\Phi Y = \varphi(F(-)+Y)$, and we put $e^\dagger := \bar{e}^\ddag$.

The next result shows that all ffg-Elgot algebras form an algebraic category over the given variety $\mathscr{C}$.

**Theorem 4.15.** For every free object $Y$ of $\mathscr{C}$, the algebra $(\Phi Y, t_Y)$ with the solution operation $\dagger$ is a free ffg-Elgot algebra for $F$ on $Y$ with $\eta_Y$ as the universal morphism.

*Proof (Sketch).* $\Phi Y$ is an ffg-Elgot algebra since it, together with $\eta_Y$, corresponds to the initial ffg-Elgot algebra $\varphi(F(-)+Y)$ under the isomorphism of Corollary 4.13. To verify its universal property, let $(A, a, \dagger)$ be an ffg-Elgot algebra for $F$ and $h: Y \to A$ a morphism. Corollary 4.13 gives an ffg-Elgot algebra $(A, [a, h], \oplus)$ for $F(-)+Y$ with $e^\dagger = \bar{e}^\oplus$ for all ffg-equations $e: X \to FX + A$. Furthermore,
Corollary 4.13 states that a morphism $p: \Phi Y \to A$ in $\mathcal{C}$ is solution-preserving w.r.t. $F(-) + Y$ if and only if it is solution-preserving w.r.t. $F$ and satisfies $p \cdot \eta_Y = h$. Therefore the universal property of $\Phi Y$ w.r.t. $F$ follows from the initiality of $\Phi Y$ w.r.t. $F(-) + Y$ (see Theorem 4.11). $\square$

**Theorem 4.16.** *The forgetful functor $U_F$: ffg-Elgot $F \to \mathcal{C}$ is monadic.*

*Proof (Sketch).* (1) First, one readily proves that $U_F$ creates sifted colimits. Moreover, $U_F$ has a left adjoint. Indeed, for every ffg object $Y$ there exists a free ffg-Elgot algebra on $Y$ by Theorem 4.15, which defines the corresponding functor $\Phi: \mathcal{C}_{fgg} \to \text{fgg-Elgot } F$. We can extend it to a left adjoint of $U_F$ as follows. Given an object $Y$ of $\mathcal{C}$ expressed as a sifted colimit $y_i: Y_i \to Y$ ($i \in I$) of ffg objects, then the image of that sifted diagram under $\Phi$ has a colimit $\text{colim}_{i \in I} \Phi Y_i$ which, since $U_F$ creates sifted colimits, is an ffg-Elgot algebra. It follows easily that this colimit is a free ffg-Elgot algebra on $Y$.

(2) By Beck's theorem it remains to prove that $U_F$ creates coequalizers of $U_F$-split pairs of morphisms. Thus let $f, g: (A, a, \dagger) \to (B, b, \ddagger)$ be solution-preserving morphisms of ffg-Elgot algebras and suppose that morphisms $c: B \to C$, $s: C \to B$ and $t: B \to A$ in $\mathcal{C}$ are given with $c \cdot f = c \cdot g$, $c \cdot s = \text{id}_C$, $g \cdot t = \text{id}_B$ and $s \cdot c = f \cdot t$.

$$A \underset{g}{\overset{f}{\rightleftarrows}} B \quad \underset{s}{\overset{c}{\rightleftarrows}} C$$

Since the category **Alg** *F* of *F*-algebras and their morphisms is monadic over $\mathcal{C}$ [8] we know that there is a unique *F*-algebra structure $\gamma: FC \to C$ such that *C* is an *F*-algebra homomorphisms from (*B*, *b*) to (*C*, $\gamma$) and *c* is, moreover, a coequalizer of *f* and *g* in **Alg** *F*. Define a solution operator $*$ for (*C*, $\gamma$) as follows. Given an ffg-equation *e*: $X \to FX + C$, put $e^* = c \cdot (s \cdot e)^{\ddagger}$. One then proves that $*$ is the unique solution operator making (*C*, $\gamma$, $*$) an ffg-Elgot algebra and *c* a solution-preserving morphism from (*B*, *b*, $\ddagger$) to (*C*, $\gamma$, $*$). Moreover, *c* is a coequalizer of *f* and *g* in ffg-Elgot *F*. $\square$

# 5 Conclusions and Further Work

For a functor *F* on a variety preserving sifted colimits, the concept of an Elgot algebra [1] has a natural weakening obtained by working with iterative equations having ffg objects of variables. We call such algebras ffg-Elgot algebras. We have proved that the locally ffg fixed point $\varphi_F$ of an endofunctor, constructed by taking the colimit of all *F*-coalgebras with an ffg carrier, is the initial ffg-Elgot algebra for *F*. Furthermore, we have proved that all free ffg-Elgot algebras exist, and we have shown that the colimit of all ffg-carried coalgebras for $F(-) + Y$ yield a free ffg-Elgot algebra on $Y$ whenever $Y$ is a free object of $\mathcal{C}$ on some (possibly infinite) set. Finally, we have proved that the forgetful functor ffg-Elgot *H* $\to \mathcal{C}$ is monadic.

We leave the task of giving a coalgebraic construction of arbitrary free ffg-Elgot algebras for further work. In addition, the study of the properties of the
ensuing free ffg-Elgot algebra monad is also left for the future. The monad of
ordinary free Elgot algebras (cf. Section 3) yields the free Elgot monad on the
given endofunctor $F$; it should be interesting to see whether the above monad of
free ffg-Elgot algebras is characterized by a similar universal property.

Finally, in the current setting we have the following picture of categories and
forgetful functors: **ffg-Elgot F ↪ → Alg F → ℂ → Set**. Each of those functors has
a left-adjoint and is in fact monadic, and we have shown that the composite of
the first two is monadic, too. We leave the question whether the composite of all
three of the functors is monadic for further work.

References

1. Adámek, J., Milius, S., Velebil, J.: Elgot algebras. Log. Methods Comput. Sci. 2(5:4), 31 pp. (2006)

2. Adámek, J., Milius, S., Velebil, J.: Iterative algebras at work. Math. Structures Comput. Sci. 16(6), 1085–1131 (2006)

3. Adámek, J., Milius, S., Velebil, J.: Semantics of higher-order recursion schemes. Log. Methods Comput. Sci. 7(1:15), 43 pp. (2011)

4. Adámek, J., Rosický, J.: Locally presentable and accessible categories. Cambridge University Press (1994)

5. Adámek, J., Rosický, J., Vitale, E.: What are sifted colimits? Theory Appl. Categ. 23, 251–260 (2010)

6. Adámek, J., Rosický, J., Vitale, E.: Algebraic Theories. Cambridge University Press (2011)

7. Applegate, H.: Acyclic models and resolvent functors. Ph.D. thesis, Columbia University (1965)

8. Barr, M.: Coequalizers and free triples. Math. Z. 116, 307–322 (1970)

9. Bonsangue, M.M., Milius, S., Silva, A.: Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log. 14(1:7) (2013)

10. Courcelle, B.: Fundamental properties of infinite trees. Theoret. Comput. Sci. 25, 95–169 (1983)

11. Ésik, Z., Maletti, A.: Simulation vs. equivalence. In: Proc. 6th Int. Conf. Foundations of Computer Science. pp. 119–122. CSREA Press (2010)

12. Ésik, Z., Maletti, A.: Simulations of weighted tree automata. In: Proc. CIAA’11. Lecture Notes Comput. Sci., vol. 6482, pp. 321–330. Springer (2011)

13. Fiore, M., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proc. LICS’99. pp. 193–202. IEEE Press (1999)

14. Freyd, P.: Rédei’s finiteness theorem for commutative semigroups. Proc. Amer. Math. Soc. 19(4) (1968)

15. Johnstone, P.T.: Adjoint lifting theorems for categories of algebras. Bull. London Math. Soc. 7, 294–297 (1975)

16. Johnstone, P.T.: Topos Theory. Academic Press, London (1977)

17. Lambek, J.: A fixpoint theorem for complete categories. Math. Z. 103, 151–161 (1968)

18. Milius, S.: Completely iterative algebras and completely iterative monads. Inform. and Comput. 196, 1–41 (2005)

19. Milius, S.: A sound and complete calculus for finite stream circuits. In: Proc. LICS’10. pp. 449–458. IEEE Computer Society (2010)
20. Milius, S.: Proper functors and fixed points for finite behaviour (2017), submitted; available online at: http://arxiv.org/abs/1705.09198

21. Milius, S.: Proper functors and their rational fixed point. In: Bonchi, F., König, B. (eds.) Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO'17). LIPIcs, vol. 72, pp. 18:1–18:15. Schloss Dagstuhl (2017)

22. Milius, S., Pattinson, D., Wißmann, T.: A new foundation for finitary corecursion and iterative algebras, submitted, available online at: http://arxiv.org/abs/1802.08070

23. Milius, S., Pattinson, D., Wißmann, T.: A new foundation for finitary corecursion: The locally finite fixpoint and its properties. In: Proc. FoSSaCS'16. Lecture Notes Comput. Sci. (ARCoSS), vol. 9634, pp. 107–125. Springer (2016)

24. Milius, S., Schröder, L., Wißmann, T.: Regular behaviours with names: On rational fixpoints of endofunctors on nominal sets. Appl. Categ. Structures 24(5), 663–701 (2016)

25. Milius, S., Wißmann, T.: Finitary corecursion for the infinitary lambda calculus. In: Proc. CALCO'15. LIPIcs, vol. 35, pp. 336–351 (2015)

26. Nelson, E.: Iterative algebras. Theoret. Comput. Sci. 25, 67–94 (1983)

27. Plotkin, G.D., Turi, D.: Towards a mathematical operational semantics. In: Proc. Logic in Computer Science (LICS'97). pp. 280–291 (1997)

28. Rédei, L.: The Theory of Finitely Generated Commutative Semigroups. Pergamon, Oxford-Edinburgh-New York (1965)

29. Silva, A., Bonchi, F., Bonsangue, M.M., Rutten, J.J.M.M.: Generalizing determination from automata to coalgebras. Log. Methods Comput. Sci 9(1:9) (2013)

30. Sokolova, A., Woracek, H.: Congruences of convex algebras. J. Pure Appl. Algebra 219(8), 3110–3148 (2015)

31. Sokolova, A., Woracek, H.: Proper semirings and proper convex functors. Tech. Rep. 22/2017, Institute for Analysis and Scientific Computing – Vienna University of Technology, TU Wien (2017), Available at http://www.asc.tuwien.ac.at/preprint/2017/asc22x2017.pdf

32. Tiuryn, J.: Unique fixed points vs. least fixed points. Theoret. Comput. Sci. 12, 229–254 (1980)

33. Urbat, H.: Finite behaviours and finitary corecursion. In: Proc. CALCO'17. LIPIcs, vol. 72, pp. 24:1–24:15 (2017)