Theory and Applications of Categories, Vol. 14, No. 8, 2005, pp. 157–199.

INTRODUCTION TO COALGEBRA

JIŘÍ ADÁMEK

Abstract. A survey of parts of General Coalgebra is presented with applications to the theory of systems. Stress is laid on terminal coalgebras and coinduction as well as iterative algebras and iterative theories.

1. Preface: Is this Really an Introduction to Coalgebra?

For my series of lectures on coalgebra on the preconference to CTCS 2002 I prepared a short text called “Introduction to Coalgebra” that was intended to cover the material of the series. I was not worried about the the choice of topics: they were given by the intentions of the course. Two years later the Program Chair Rick Blute suggested that I could publish the text in the proceedings—and after I agreed, I found myself in a fix: what topics to choose? If I add to the existing text the minimum of material that would indeed constitute a general introduction to coalgebra, the text would grow immensely. Besides, excellent introductions exist already, see e.g. [R1], [G], [JR]. I decided for a minimalistic approach: in the following sections I try and present an introduction to the parts of coalgebra which are those “dearest to my heart”, and to which I have also contributed. Thus, a substantial part of coalgebra topics is not mentioned at all; I hope the reader will enjoy what I present below, and I ask her or him not to take a missing topic as a message of any kind. Almost all proofs are omitted, with precise references provided, just some simple, instructive proofs are left.

Contents

1 Preface 157 2 Introduction: Systems as Coalgebras 158 3 Categories of Algebras and Coalgebras 161 4 Constructions of Coalgebras 169 5 Bisimulation and Coinduction 174 6 Iterative Algebras 182 7 Iterative Theories 187 8 Complete Iterativity 190 9 Parametrized Iterativity 191 10 Coalgebra in Classes 195

Supported by the Grant Agency of Czech Republic, No. 201/02/0148.

Received by the editors 2004-10-07 and, in revised form, 2005-01-25.

Transmitted by Richard Blute. Published on 2005-05-08.

2000 Mathematics Subject Classification: 08A70, 08C05, 93A30, 18A40, 18C20, 18C35.

\begin{matrix}c \\ ◯ \end{matrix} Jiří Adámek, 2004. Permission to copy for private use granted.

2. Introduction: Systems as Coalgebras

The present section, closely following ideas of J. Rutten [R1], tries and explains the motivation of General Coalgebra which stems from various types of dynamical systems.

2.1 The earliest observation in the literature about application of coalgebras is probably due to M. Arbib and E. G. Manes [AMa] concerning deterministic automata described by a set Q (of states), a next-state function δ: Q × Σ [figure] Q (where Σ is the set of inputs) and a predicate final: Q [figure]bool. Initial states are ignored at the moment, see later. We can use the curried version of the next-state function, say δ̄: Q [figure] Q^{Σ} where δ̄(q) is the function δ(q, −): Σ [figure] Q for every state q ∈ Q. Then δ̄ and final yield together one function from Q to Q^{Σ} × bool. In other words, a deterministic automaton consists of a set Q and a “dynamics”

α: Q [figure] HQ where HQ = Q^{Σ} × bool .

Observe that there is a canonical way of making a functor H: Set [figure]Set out of the above rule HQ = Q^{Σ} × bool for objects Q: given a morphism h: Q_{1} [figure] Q_{2} then Hh: Q_{1}^{Σ}×bool [figure] Q_{2}^{Σ}×bool is the function which to every pair (u, x) with u: Σ [figure] Q_{1} and x ∈ bool assigns the pair (h·u, x).

2.2 Deterministic automata constitute an example of coalgebras specified by an endofunctor H of Set: a coalgebra is a pair (Q, α) consisting of a set Q (of “states”) and a function α: Q [figure] HQ (“dynamics”). Given coalgebras (Q, α) and (Q′, α′), a coalgebra homomorphism is a function f: Q [figure] Q′ such that the square

(1)  [figure: Q′; HQ′; α′; Q; Q′; f; Q; HQ; α; HQ; HQ′; Hf]

commutes. For example in the above case of H = (−)^{Σ} × bool, this is precisely the concept of functional simulation of deterministic automata.

2.3 An important example of coalgebras are labeled transition systems consisting of a state set Q and transitions

q [figure: s] q̄ for q, q̄ ∈ Q and s ∈ Σ

(where Σ is the set of possible actions). More precisely, for every action s a binary relation [figure: s]is given on Q. This can be viewed as a coalgebra for the functor

H = 𝒫(Σ × −)

where 𝒫: Set [figure] Set is the power-set functor. (Recall that for every set Q, the powerset 𝒫Q consists of all subsets of Q, and for every function f: Q_{1} [figure] Q_{2} the function 𝒫f maps M ⊆ Q_{1} to f[M] ⊆ Q_{2}.) In fact, define

α: Q [figure] 𝒫(Σ × Q)

by assigning to every state q the set α(q) of all pairs (s, q̄) ∈ Σ×Q with q [figure: s] q̄. Coalgebra homomorphisms f: (Q, α) [figure] (Q′, α′) are precisely the functions which preserve and reflect transitions. That is

(a) q [figure: s] q̄ in Q implies f(q) [figure: s] f(q̄) in Q′

and

(b) f(q) [figure: s] q̄ in Q′ implies q [figure: s] q̂ in Q for some q̂ ∈ Q with f(q̂) = q̄.

These homomorphisms serve e.g. for a simple formulation of a strong bisimulation, see Section 5.

2.4 Just as in algebraic semantics the initial algebra plays a central role, in coalgebra the terminal coalgebras (i.e., terminal objects of the category of all coalgebras) are of major importance. Recall that a terminal coalgebra is a coalgebra T [figure: τ] HT such that for every coalgebra Q [figure: α] HQ there exists a unique homomorphism ⟦α⟧: Q [figure] T. Usually, T is the set of all “types of behaviors” of states and ⟦α⟧ assigns to q ∈ Q the type of behavior q has.

2.5. Example. H = (−)^{Σ} × bool (deterministic automata). Here T = 𝒫Σ^{∗} is the set of all formal languages, considered as an automaton as follows: for a language L ∈ 𝒫Σ^{∗} and s ∈ Σ put

δ(L, s) = {w ∈ Σ^{∗}; sw ∈ L};

and final(L) = true iff L contains ε.

Given an automaton (Q, α) the unique homomorphism

⟦α⟧: Q [figure] T = exp Σ^{∗}

assigns to every state q the language ⟦α⟧(q) ⊆ Σ^{∗} which the automaton Q accepts in case q is the initial state. Here we see the manner in which the (so far missing) concept of initial state is recaptured.

2.6. Example. HX = X × X + 1. This is an endofunctor whose coalgebras are deterministic systems with a binary input and deadlock states (i.e., states that do not react to input). In fact, each such system is described by the dynamics

α: Q [figure] Q × Q + 1

taking deadlock states to the right-hand summand, and non-deadlock states q to the pair α(q) = (q_{0}, q_{1}) of next states. Homomorphisms are the functional bisimulations, i.e., maps preserving and reflecting input reaction and preserving and reflecting deadlock states.

A terminal coalgebra T consists of all (finite and infinite) binary trees^{1}: the unique deadlock of T the trivial single-node tree, the next states of a nontrivial tree are the two maximal proper subtrees.

Given a system (Q, α) the unique homomorphism

⟦α⟧: Q [figure] T

takes every state q to the tree ⟦α⟧(q) ∈ T obtained by the unfolding of q in the system Q.

2.7. Example. H = 𝒫_{f}, the finite-power-set functor. This functor assigns to every set X the set 𝒫_{f}X of all finite subsets of X, and behaves on morphisms as the power-set functor 𝒫 does.

A coalgebra of 𝒫_{f} can be viewed as a finitely branching nondeterministic system: the dynamics

α: Q [figure] 𝒫_{f}Q

assigns to every state q the collection α(q) of all possible next states. Sometimes one also identifies Q with a finitely branching directed graph: α(q) is the set of all neighbour nodes of q. However, this is often not a reasonable point of view because the coalgebra homomorphisms are much stronger than graph homomorphisms: given two systems (Q, α) and (Q′, α′), a coalgebra homomorphism is a function h: Q [figure] Q′ which preserves and reflects the dynamics. That is, h is a graph homomorphism such that if q̄ is a next state of h(q) in Q′, then there exists a next state q̂ of q in Q with q̄ = h(q̂).

A final coalgebra of 𝒫_{f} can be described as the coalgebra of all strongly extensional, finitely branching trees, see Example 5.10(iv).

2.8. Example. H = 𝒫(Σ × −). As we will see in Section 3, this endofunctor of Set does not have a terminal coalgebra. However, every endofunctor H of Set has a terminal coalgebra in Class, the category of classes, see Section 10. For example, the terminal coalgebra of 𝒫(Σ × −) is the coalgebra T of all nonordered trees with nodes labeled in Σ modulo tree bisimilarity.

Given a labeled transition system (Q, α), the unique homomorphism

⟦α⟧: Q [figure] T

assigns to every state q the bisimilarity class of the unfolding tree of q in Q.

1Trees are understood to be rooted and they are considered up-to isomorphism. Unless explicitly stated we consider ordered trees, i.e., with a linear order on the set of children of every node.

2.9 Terminal coalgebras of “derived” endofunctors are also of some importance: for every set Y a terminal coalgebra, CY, of the endofunctor H(−)×Y is a cofree coalgebra colored in Y, a concept explained in Section 3. A terminal coalgebra, T Y, of the endofunctor H(−)+Y is a free completely iterative algebra on Y —the concept of (completely) iterative algebras and their relationship to coalgebra is explained in Sections 6–9. The last section is devoted to coalgebra in the category of classes: this category has a number of convenient properties, e.g., every endofunctor H has a terminal coalgebra (and, consequently, the above coalgebras CY and T Y always exist).

2.10 Although all important examples of application of coalgebra seem to concern coalgebras in Set, there are good reasons to develop the whole theory in an abstract category, e.g., (1) the dualization, see 3.6, only works in the abstract setting, (2) the techniques used are often clearer in the abstract categorical formulation, and (3) the category of classes may actually be preferable to Set.

3. Categories of Algebras and Coalgebras

3.1. Algebras. Let 𝒜 be a category. For every endofunctor H: 𝒜 [figure] 𝒜 by an H-algebra is meant a pair consisting of an object A ∈ 𝒜 and a morphism α: HA [figure] A.

Given H-algebras HA [figure: α] A and HB [figure: β] B, by a homomorphism is meant a morphism h: A [figure] B of 𝒜 for which the following square

[figure: HB; B; β; HA; HB; Hh; HA; A; α; A; B; h]

commutes.

Example: for the set functor HX = (X × X) + 1 an H-algebra is a set A together with one binary operation, A × A [figure] A, and one constant, 1 [figure] A, represented by the corresponding morphism α: A × A + 1 [figure] A. Homomorphisms are functions preserving the two operations in the usual algebraic sense.

We denote by Alg H the category of all H-algebras and homomorphisms. They were for the first time considered by J. Lambek [L] who proved the following

3.2. Lambek Lemma. (An initial H-algebra is a fixed point of H.) If HI [figure: φ] I is an initial object of Alg H, then φ is an isomorphism.

Proof. For the H-algebra H(HI) [figure: Hφ] HI there exists a unique homomorphism

[figure: H(HI); HI; Hφ; HI; H(HI); Hh; HI; I; φ; I; HI; h; HI; I; φ; H(HI); HI; Hφ; H(HI); HI; HI; I; φ]

Then φh is an endomorphism of algebra I—thus φh = id, since I is initial. The upper square of the above diagram yields hφ = F (φh) = id.

3.3. Examples. (i) The power-set functor 𝒫 does not have an initial algebra: by the Cantor Theorem 𝒫 has no fixed point (since card 𝒫I > card I).

(ii) The functor HX = (X×X)+1 has an initial algebra I consisting of all finite binary trees. The binary operation is that of tree-tupling, and the constant is the single-node tree.

(iii) For the set-functor HX = Σ × X + 1 an H-algebra is a unary algebra with operation symbols from Σ and one constant. An initial algebra is the set Σ^{∗} of all finite words (= sequences) over Σ, with the operations Σ × Σ^{∗} [figure] Σ^{∗} of concatenation, (σ_{1} … σ, σ_{n}) [figure] (σσ_{1} … σ_{n}) and the constant ε.

3.4. Coalgebras. A pair (A, α) consisting of an object A and a morphism α: A [figure] HA is called an H-coalgebra. We call α the dynamics of the coalgebra A. Given H-coalgebras (A, α) and (B, β), by a homomorphism is meant a morphism h: A [figure] B in 𝒜 for which the following square

[figure: B; HB; β; A; B; h; A; HA; α; HA; HB; Hh]

commutes.

3.5. Notation. We denote by Coalg H the category of all coalgebras and homomorphisms.

In case a terminal coalgebra T [figure: τ] HT, i.e., a terminal object of Coalg H, exists, we

denote for every coalgebra α: A  [figure] HA by ⟦α⟧: A  [figure] T the unique homomorphism

[figure: A; HA; α; T; A; ⟦α⟧; T; HT; τ; HT; HA; H⟦α⟧]
3.6. Observation.  If we form the obvious functor H^{op} : 𝒜^{op}  [figure] 𝒜^{op}, then the

categories Alg H^{op} and Coalg H are dual to each other.

3.7. Corollary. Terminal H-coalgebras are fixed points of H.

In fact, this follows from Lambek Lemma by duality.

3.8. Examples. Coalgebras over endofunctors of Set.

(i) For HX = X + 1 a coalgebra A [figure: α] A + 1 is precisely a set A with a partial unary operations. Homomorphisms h: A [figure] B of coalgebras are the “strong” homomorphisms of partial unary algebras, i.e., given a ∈ A then the A-operation is defined in A iff the B-operation is defined in h(a).

A final coalgebra can be described as the coalgebra

\overline{ℕ} = ℕ ∪ \{∞\}

of extended natural numbers whose dynamics is the following predecessor function

pred(0) undefined
pred(n) = n − 1 for 0 < n < ∞

and

pred(∞) = ∞.

Given a coalgebra A, the unique homomorphism ⟦α⟧: A [figure] \overline{ℕ} assigns to every state a the maximum n such that all α^{i}(a) for 1 ≤ i < n are defined.

(ii) For HX = Σ × X a coalgebra A [figure: α] Σ × A consists of two functions A [figure] Σ and A [figure] A. A terminal coalgebra is the set

T = Σ^{ω}

of all infinite sequences in Σ with the dynamics given by the functions “head” and “tail”:

τ: T  [figure] Σ × T,  τ(x_{0}, x_{1}, x_{2}, …) = (x_{0}, (x_{1}, x_{2}, x_{3}, …)).

(iii) For HX = X × X + 1 a coalgebra A [figure: α] A × A + 1 is given by a partial function from A to A × A. A terminal coalgebra has been described the Example 2.6: T consists of all binary trees.

(iv) 𝒫 has no terminal coalgebras.

3.9. Remark. The examples (i)–(iii) in 3.8 are special cases of the following situation: suppose a signature Σ, i.e., a set of operation symbols σ with prescribed arities ar σ ∈ ℕ, is given. We denote by H_{Σ} : Set [figure]Set the following polynomial functor

H_{Σ}X = Σ_{0} + (Σ_{1} × X) + (Σ_{2} × X × X) + ⋯

where Σ_{n} ⊆ Σ is the set of all n-ary symbols. Elements of H_{Σ}X are denoted by σ(x_{1}, …, x_{n}) for σ ∈ Σ_{n}.

H_{Σ}-algebras are the usual Σ-algebras of General Algebra, i.e., sets A equipped with an n-ary operation σ_{A}: A^{n} [figure] A for every σ ∈ Σ_{n} (or, equivalently, with a function from H_{Σ}A to A).

H_{Σ}-coalgebras are deterministic automata with a state set Q, an output set Σ and with n next states for every state with an n-ary output.

An initial algebra, I_{Σ}, can be described as the algebra of all finite Σ-trees, i.e., ordered trees with all nodes labeled in Σ so that a label in Σ_{n} implies that the node has precisely n children. The operation

H_{Σ}(I_{Σ}) [figure] I_{Σ}

is tree-tupling: given σ ∈ Σ_{n} and Σ-labeled trees t_{1}, …, t_{n}, form the Σ-labeled tree

[figure: σ; t_{1}; t_{2}; σ; t_{n}; σ; …]

We now denote by

T_{Σ}

the analogous coalgebra obtained by dropping the finiteness requirement: T_{Σ} has as elements all (finite or infinite) Σ-labeled trees. We again have a structure of an algebra H_{Σ}(T_{Σ}) [figure] T_{Σ} given by tree tupling. This (as in I_{Σ} above) is an isomorphism, so we can invert it:

3.10. Theorem. (See [AP1].) The coalgebra T_{Σ} of all Σ-labeled trees whose dynamics is “parsing”, i.e., the inverse of tree-tupling, is terminal for H_{Σ}.

3.11. Example. The functor HX = X + 1 of 3.7(i) is polynomial with Σ_{0} = {⊥}, Σ_{1} = {σ} and Σ_{n} = ∅ for n > 1. The coalgebra T_{Σ} consists of the following trees

[figure: ⊥; ⊥; σ; σ; σ; ⊥; …]

and the unique infinite tree with all nodes labeled by σ. This is isomorphic to \overline{ℕ} as described in 3.7(i).

3.12. Remark. (a) Recall that the concept of a free algebra on an object X (of generators): it is an algebra

φ_{X}: HX^{#} [figure] X^{#}

together with a universal arrow

η_{X}: X [figure] X^{#}

of the canonical forgetful functor Alg H [figure] 𝒜. This means that for every algebra A and every morphism f: X [figure] A (interpretation of generators) there exists a unique homomorphism

f′: X^{#} [figure] A with f = f′·η_{X}.

(b) H is called a varietor, see [AT1], provided that free algebras exist, i.e., the above forgetful functor of Alg H has a left adjoint X [figure] X^{#}.

For example, a nonconstant functor H: Set [figure] Set is a varietor iff H has arbitrarily large fixed points, see [AT1].

(c) It is easy to verify that the Lambek Lemma implies that X^{#} is a coproduct

X^{#} = HX^{#} + X with injections φ_{X} and η_{X}.

In fact, X^{#} is an initial algebra of the functor H(−)+X (and vice versa: an initial algebra of H(−) + X is a free H-algebra on X).

(d) If H is a varietor, then the monad of free H-algebras was elegantly characterized by M. Barr [B1] as the free monad on H. Also conversely: if an endofunctor of a complete, well-powered category generates a free monad, it must be a varietor. Moreover, Alg H is monadic over 𝒜, being equivalent to the Eilenberg-Moore category of the free-algebra monad.

3.13. Remark. Dually H is a covarietor if cofree coalgebras exist (or, if H generates a cofree comonad).

Explicitly, for every object X (of “colors”) in 𝒜 a cofree coalgebra on colors from X is a coalgebra

ψ_{X}: X_{#} [figure] HX_{#}

together with a universal “coloring” morphism

ε_{X}: X_{#} [figure] X;

for every coalgebra (A, α) and every coloring morphism f: A [figure] X there exists a unique homomorphism

f′: A [figure] X_{#} with f = ε_{X}·f′.

The interpretation is that we can use colors (elements of X) to color the states of systems. We cannot observe individual states, but can observe their colors. Then X_{#} is the set of all types of behaviors of states of systems colored in X.

3.14. Examples. (1) For HX = X ×X +1 a cofree coalgebra X_{#} is the coalgebra of all binary trees with nodes colored in X. Given a system (Q, α) and a coloring f: Q [figure] X, the unique homomorphism f′: Q [figure] X_{#} assigns to every state q the colored tree obtained by unfolding q in the system Q and observing the colors of the future states.

(2) More generally, for every polynomial functor H_{Σ} a cofree coalgebra X_{#} is the coalgebra of all Σ-trees with an additional coloring of the nodes in X. This is, obviously, just the terminal coalgebra of the polynomial functor H_{Σ[X]} where the new signature Σ[X] has operation symbols from Σ × X and the arity of every pair (σ, x) is n for σ ∈ Σ_{n}.

(3) A cofree H-coalgebra on X is precisely a terminal coalgebra of H(−) × X. This statement, dual to 3.11(c), is illustrated by the above example of H_{Σ[X]} = H_{Σ}(−) × Σ.

(4) If 1 is a terminal object of 𝒜 then

1_{#} = T

is a terminal coalgebra.

(5) The power-set functor 𝒫 does not have cofree coalgebras. But it has them in the category of classes, see Section 10.

3.15. Remark. (a) Recall that a functor is called finitary if it preserves filtered colimits, and accessible if it preserves, for some infinite cardinal λ, λ-filtered colimits. In case 𝒜 = Set, accessible endofunctors are precisely the bounded endofunctors of [KM] (as proved in [AP2]). That is, such that for some cardinal λ every coalgebra is a union of subalgebras of cardinalities at most λ.

(b) Every accessible endofunctor of Set is a varietor and a covarietor; however, there are varietors and covarietors which are not accessible, see [AT1].

(c) Recall that an object A of a category 𝒜 is called finitely presentable provided that its hom-functor hom(A, −): 𝒜 [figure]Set is finitary. The category 𝒜 is called locally finitely presentable in the sense of Gabriel and Ulmer [GU], see also [AR], provided that

1. 𝒜 has colimits

and

2. 𝒜 has a small set of finitely presentable objects whose closure under filtered colimits is all of 𝒜.

For example in Set “finitely presentable” means finite, and every set is a directed colimit of finite sets. Thus, Set is locally finitely presentable. In an equationally definable class of algebras “finitely presentable” has the classical meaning (of presentation by finitely many generators and finitely many equations), and each such category is locally finitely presentable. In contrast, the category of domains and continuous functions is not locally finitely presentable: except trivial domains no object is finitely presentable.

(d) Generalizing (b), every accessible endofunctor of a locally finitely presentable category is a varietor and a covarietor, see [B2].

3.16. Example. The polynomial functor H_{Σ} is a (finitary) varietor and a covarietor. A free algebra X^{#} is the algebra of all finite Σ-trees on X (where “on X” means that leaves are labeled by nullary operation symbols or by elements of X). A cofree coalgebra X_{#} is the coalgebra of all finite and infinite Σ-trees with an additional coloring of all nodes in X.

3.17. Theorem. (See [A0].) Let 𝒜 have and H preserve ω-colimits. If 0 is the initial object of 𝒜 and !: 0 [figure] H0 the unique morphism, then an initial algebra I is a colimit of the ω-chain

0 [figure: !] H0 [figure: H!] HH0 [figure: HH!]⋯

3.18. Corollary. If 𝒜 has and H preserves ω^{op}-limits then a terminal coalgebra T is a limit of

1 [figure: !] H1 [figure: H!] HH1 [figure: HH!] ⋯ (1 terminal in 𝒜).

3.19. Theorem. (Initial-Algebra Construction, see [A0].) Let 𝒜 have and H preserve λ-colimits (λ an infinite cardinal). Then an initial algebra is I = colim_{i<λ} W_{i} for the λchain determined (essentially uniquely) as follows:

Initial step: W_{0} = 0, W_{1} = H0 and W_{01} = !: 0 [figure] H0.

Isolated step: W_{i+1} = HW_{i} and W_{i+1,j+1} = HW_{i,j}: HW_{i} [figure] HW_{j}.

Limit step: W_{j} = colim_{i<j} W_{i} for limit ordinals j.

3.20. Corollary. (Terminal-Coalgebra Construction.) If 𝒜 has and H preserves λ^{op}-limits, then a terminal algebra is T = lim_{i<λ} W_{i} for the dual λ^{op}-chain (W_{0} = 1, W_{i+1} = HW_{i} and W_{j} = lim_{i<j} W_{i} for limit ordinals j).

3.21. Theorem. (See [W1].) A finitary functor H: Set [figure] Set requires only ω + ω steps of the terminal-coalgebra construction:

T = lim_{i<ω+ω} W_{i}.

Example. (See [W1].) The terminal coalgebra-construction of 𝒫_{f} yields after ω steps all, not necessarily finitely branching, strongly extensional trees as W_{ω}, compare 5.10(iv). Then W_{ω+1,ω}: 𝒫_{f}W_{ω} [figure] W_{ω} is the subset of all trees finitely branching at level 1, W_{ω+2,ω}: 𝒫_{f}W_{ω+1} [figure] W_{ω} are all trees finitely branching at levels 1 and 2, etc. Thus T = lim_{i<ω+ω} W_{i} is the algebra of all finitely branching strongly extensional trees.

3.22. Remark. (i) Whenever H is an accessible endofunctor, then so is H(−) + Y for every object Y. Consequently, a terminal coalgebra T Y of the latter functor exists.

By Lambek’s Lemma, the dynamics T Y [figure] HT Y + Y is an isomorphism. In other words, T Y is a coproduct of HT Y and Y; we denote by

τ_{Y} : HT Y  [figure] T Y  (T Y is an H-algebra)

and

η_{Y} : Y  [figure] T Y  (T Y contains Y)

the coproduct injections.

In general, we use inr and inl for coproduct injections.

(ii) Recall that if Y^{#} is a free H-algebra on Y, then for every morphism s: X [figure] Y^{#} there exists a unique homomorphism ŝ: X^{#} [figure] Y^{#} extending s. We prove now that T Y has a similar property; we include a full proof because it is simple and instructive. The result also follows from Theorem 8.4 below.

3.23. Substitution Theorem. (See [Mo] or [AAMV].) For every accessible functor H and every morphism s: X [figure] T Y there exists a unique homomorphism ŝ: T X [figure] T Y of H-algebras extending s. (That is, a unique ŝ with s = ŝ·η_{x} and ŝ·τ_{X} = τ_{Y} ·Hŝ.)

Proof. Consider the following dynamics α on T X + T Y for the endofunctor H(−) + Y: α is a composite of

T X + T Y = HT X + X + T Y [figure: id +[s,id]] HT X + T Y = HT X + HT Y + Y

followed by the canonical morphism HT X + HT Y + Y [figure] H(T X + T Y) + Y. The homomorphism ⟦α⟧: T X+T Y [figure] T Y has the right-hand component ⟦α⟧ inr: T Y [figure] T Y of which it is easy to verify that this is an endomorphism of T Y in Coalg(H(−) + Y). Since T Y is terminal, we conclude

⟦α⟧ inr = id .

Thus, ⟦α⟧ is fully determined by

ŝ =^{def} ⟦α⟧ inl: T X [figure] T Y.

Since ⟦α⟧ is a homomorphism, one can readily check

s = ŝ · η_{X} and τ_{Y} ·Hŝ = ŝ · τ_{X}.

3.24. Remark. Recall the concept of a monad in the form of “Kleisli triples”: a monad is an endofunctor T together with a natural transformation η: Id [figure] T and a function assigning to every morphism s: X [figure] T Y a morphism ŝ: T X [figure] T Y such that (i) ŝ·η_{X} = s, (ii) η̂_{X} = id_{T X} and (iii) given t: Y [figure] T Z then t̂·ŝ = ˆ(t̂·s).

It follows immediately from the Substitution Theorem that T is a monad. We will see in Section 7 that T is a free completely iterative monad on H.

Thus, for a polynomial functor H_{Σ} we get the Σ-tree monad as a free completely iterative monad on Σ. This was originally proved in [EBT].

4. Constructions of Coalgebras

4.1. Assumption. Throughout this section H denotes an endofunctor of a category 𝒜. The forgetful functor of Coalg H is denoted by U: Coalg H [figure] 𝒜.

4.2. Colimits of Coalgebras. They are easy to construct (for the same reason for which limits of algebras are). For example, a coproduct of coalgebras A_{t} [figure: α_{t}] HA_{t}, t ∈ T, is a coproduct ∐_{t∈T} A_{t} (with injections in_{t}) in 𝒜 equipped with the unique dynamics turning each in_{t} into a homomorphism, viz

[H in_{t} ·α_{t}]_{t∈T} : ∐_{t∈T} A_{t} [figure] H(∐_{t∈T} A_{t}).

More generally, the following is easy to prove:

4.3. Proposition. The forgetful functor U: Coalg H [figure] 𝒜 creates colimits. That is, a colimit of a diagram D: 𝒟 [figure]Coalg H is obtained from a colimit C = colim U·D in 𝒜 (assuming this exists) by equipping C with the unique dynamics on C turning the colimit cocone into a cocone of homomorphisms.

4.4. Remark. (a) Limits of coalgebras are less obvious. Except those that H preserves: it is easy to see that U creates all such limits. We prove a criterion for completeness of Coalg H below.

(b) For the power-set functor 𝒫 we know that Coalg 𝒫 is not complete because it does not have a terminal object (see 3.8(iv)).

(c) If H is a covarietor, then U is comonadic—this is just the dual of 3.12(d). Consequently, the existence of equalizers in Coalg H implies that Coalg H is complete: see Linton’s proof of the dual statement in [Li]. That proof provides an explicit description of products in Coalg H via equalizers: let (A_{i}, α_{i}) be coalgebras, i ∈ I, and form the unique homomorphisms

ᾱ_{i}: A_{i} [figure] (A_{i})_{#} with ε_{A_{i}} · ᾱ_{i} = id_{A_{i}}.

For the products A = ∏ A_{i} and B = ∏(A_{i})_{#} in 𝒜 we obtain a canonical morphism

k: A_{#}  [figure] B extending to a homomorphism k′: A_{#}  [figure] B_{#}. And the product ᾱ =
∏_{i∈I} ᾱ_{i}: A  [figure] B yields another homomorphism ᾱ_{#} : A_{#}  [figure] B_{#}. The equalizer of this

parallel pair

E [figure: e] A_{#} [figure: k′; ᾱ_{#}] B_{#}

in Coalg H is a product of the given coalgebras (with projections E [figure: e] A_{#} [figure: ε_{A}] A [figure: π_{i}] A_{i}).

4.5. Quotient Coalgebras. Recall that in General Algebra monomorphisms are precisely the homomorphisms that are carried by monomorphisms in the base category. Thus the concept of subalgebra needs no discussion: one works with the usual categorical concept of subobject. Dually, quotient coalgebras are just represented by epimorphisms in Coalg H. This is substantiated by the following 4.6. Lemma. Epimorphisms in Coalg H are precisely the homomorphisms carried by epimorphisms in 𝒜.

Proof. If a homomorphism h: (A, α) [figure] (B, β) is an epimorphism in 𝒜, then it is an epimorphism in Coalg H because the forgetful functor U: Coalg H [figure] 𝒜 is faithful. For the converse, use the fact that U creates colimits: if h is an epimorphism, then a pushout of h and h (in Coalg H, thus, in 𝒜) is formed by id_{B}, id_{B}.

4.7. Remark. If 𝒜 = Set, then every quotient coalgebra of a coalgebra (A, α) can be represented by a congruence, i.e., an equivalence relation ∼ on A such that the canonical morphism c: A [figure] A/∼ is a homomorphism

[figure: A/∼; H(A/∼); α^{∗}; A; A/∼; c; A; HA; α; HA; H(A/∼); Hc]

(for a, necessarily unique, α^{∗}). And conversely, every congruence yields a quotient coalgebra on A/∼.

4.8 Monomorphisms in Coalg H are more difficult (dually to the difficulties with epimorphisms well known from General Algebra). It is clear that every homomorphism carried by a monomorphism in 𝒜 is a monomorphism in Coalg H (since U is faithful), but not conversely. In fact, if 𝒜 = Set, then homomorphisms which are injective maps (i.e., are monomorphisms in 𝒜) are precisely the regular monomorphisms of Coalg H, see Theorem 3.4 in [GS2]; that paper is also the source of the following example inspired by [AM]:

4.9. Example. Denote by

(−)_{2}^{3} : Set [figure]Set

the functor which is the subfunctor of the polynomial functor X [figure] X^{3} on all triples (x_{1}, x_{2}, x_{3}) ∈ X^{3} whose coordinates are not pairwise distinct. Let A be the coalgebra on {a, b} whose structure map α: A [figure] A_{2}^{3} is defined by

α(a) = (a, b, b) and α(b) = (b, b, a).

It is easy to see that the (constant) map from A to the terminal, one-element, coalgebra is a monomorphism.

4.10. Subcoalgebras. Analogously to General Algebra, where the canonical factorization structure for morphisms is (regular epi, mono)—or, equivalently, (strong epi, mono), for coalgebra we propose to use the factorization system (epi, strong mono) because, as we prove below, strong monomorphisms in Coalg H are precisely those carried by strong monomorphisms in 𝒜.

Recall that a monomorphism m is called strong in a category iff for every epimorphism e and every commutative square

[figure: m; e; d]  (diagonal fill-in)

there exists a diagonal d making both triangles commutative. All “everyday” categories have (epi, strong mono)-factorization of morphisms. E.g. every strongly complete category, i.e., a category which has all small limits and all intersections of subobjects (possibly large), has (epi, strong mono) factorizations, see 14.21 and 14.C in [AHS].

By a subcoalgebra of a coalgebra (A, α) we understand a strong subobject in Coalg H, i.e., one represented by a strong monomorphism with codomain (A, α). This is substantiated by the following

4.11. Lemma. If 𝒜 has (epi, strong mono)-factorizations and H preserves strong monomorphisms, then strong monomorphisms in Coalg H are precisely the morphisms carried by strong monomorphisms in 𝒜.

4.12. Corollary. For endofunctors H of Set, strong monomorphisms in Coalg H are precisely the one-to-one homomorphisms.

Proof of 4.11 and 4.12. If a homomorphism h: (A, α) [figure] (B, β) is a strong monomorphism in 𝒜, then it is a strong monomorphism Coalg H due to Lemma 4.6.

Conversely, if h is a strong monomorphism in Coalg H, factorize it in 𝒜 as an epimorphism e: A [figure] C followed by a strong monomorphism i: C [figure] B. Use the diagonal fill-in in 𝒜 to make e and i homomorphisms:

[figure: HA; B; A; HA; α; A; C; e; C; B; i; HC; HB; Hi; HA; HC; He; HA; B; B; HB; β; C; HC; γ]

By using the diagonal fill-in in Coalg H:

[figure: (A, α); (B, β); h; (A, α); (A, α); id; (A, α); (C, γ); e; (C, γ); (B, β); i; (C, γ); (A, α)]

conclude that e is an isomorphism—thus, h is a strong monomorphism in 𝒜.

For 𝒜 = Set define H′ by H′X = HX if X ≠ ∅ and H′∅ = ∅ to obtain a functor H′ preserving (strong) monomorphisms. It is clear that Coalg H′ and Coalg H are isomorphic categories. Apply the above to H′.

4.13. Corollary. Let 𝒜 have (epi, strong mono)-factorizations. If 𝒜 = Set or if H preserves strong monomorphisms, then Coalg H also has (epi, strong mono)- factorizations. They are, in fact, created by the forgetful functor U.

4.14. Limit Theorem. For every covarietor on a strongly complete category preserving strong monomorphisms the category of coalgebras is complete.

Proof. Due to 4.4(c) it is sufficient to prove the existence of equalizers in Coalg H. Given homomorphisms h, k: (A, α) [figure] (B, β) with an equalizer e: E [figure] A in 𝒜, we denote by S the (possibly large) poset of all strong subobjects of A in 𝒜. Since 𝒜 is strongly complete, S is a complete lattice. For every strong subobject m: M [figure] A we have a strong subobject Hm: HM [figure] HA and pulling it back along α yields a strong subobject α^{−1}(Hm) in S. Put

m^{∗} = α^{−1}(Hm) ∩ e

to obtain an endomap (−)^{∗} of S. Since this endomap is order-preserving, it has a largest post-fixed point m_{0} : M_{0} [figure] A (by Knaster-Tarski theorem). Since m_{0} ⊆ α^{−1}(Hm_{0}), there exists a dynamics M_{0} [figure] HM_{0} turning m_{0} into a homomorphism. Since m_{0} ⊆ e, we have hm_{0} = km_{0}. Thus m_{0} is a equalizer of h and k. In fact, due to Corollary 4.12 we only need to show, for every homomorphism m: (M, γ) [figure] (A, α) carried by a strong monomorphism m in 𝒜, that

hm = km implies m ⊆ m_{0}.

Now m ⊆ α^{−1}(Hm), since m is a homomorphism, and m ⊆ e, since hm = km—thus, m is a post-fixed point of (−)^{∗}. Consequently, m ⊆ m_{0}.

4.15. Corollary. For every covarietor in Set the category of coalgebras is complete.

In fact, if H preserves strong monomorphisms, this follows from 4.14. If H does not, use the argument of 4.12 (see the end of proof).

4.16. Remark. (i) The above theorem improves a bit Corollary II.5 of [A1] where instead of strong completeness we assumed completeness and well-poweredness.

(ii) The assumption that H preserve monomorphisms is essential: a noncomplete category Coalg H for a covarietor on a strongly complete category is presented in [A1] (the dual of Example III.2 there).

(iii) The proof of 4.14 constructs a greatest subcoalgebra in the sense of B. Jacobs [J]. Thus, the result can also be deduced from Corollary 4.3 in [J], but the present proof is simpler. Previous results on limits of coalgebras due to J. Worrell [W2] and P. Gumm and T. Schöder [GS1] are special cases of Theorem 4.14.

4.17. Coequations. Recall from [BH] that (systems of) equations in General Algebra can be modelled by forming a strong quotient e: X^{#} [figure] E of (the underlying object of) a free algebra X^{#}. Then an algebra A satisfies e iff every homomorphism f: X^{#} [figure] A factorizes through e.

Dually, J. Rutten [R1] introduced presentations of classes of coalgebras over Set by subobjects of cofree coalgebras, for all accessible endofunctors of Set. There is an immediate generalization:

4.18. Definition. Let H: 𝒜 [figure] 𝒜 be a covarietor. By a coequation we mean a strong subobject (in 𝒜) of a cofree coalgebra:

m: M  [figure] X_{#}  for X ∈ 𝒜.

A coalgebra A is said to satisfy the coequation if every homomorphism h: A [figure] X_{#} factorizes through m in 𝒜

[figure: M; X_{#}; m; A; M; A; X_{#}; h]

4.19. Example. For deterministic systems with binary input and deadlocks, i.e., HX = X × X + 1 in Set (see Example 2.6) recall that the terminal coalgebra 1_{#} is the coalgebra of all binary trees. Let m: M [figure] 1_{#} be the set of all finite trees. Then a coalgebra satisfies m iff every run in the system ends in a deadlock.

For the trivial one-node tree t ∈ 1_{#} the coequation

[figure: 1_{#} − {t}; 1_{#}]

is satisfied by precisely all systems without deadlocks.

4.20. Birkhoff’s Covariety Theorem.  Let H: Set  [figure]Set be a covarietor.

Then a full subcategory of Coalg H is presentable by coequations iff it is closed under coproducts, subalgebras and quotient coalgebras in Coalg H.

This theorem, proved in [AP1], is a slight generalization of Rutten’s original formulation in [R1]. A different approach based on dualizing Lawvere’s algebraic theories, was presented by A. Kurz and J. Rosický [KR]. The relationship between the results of [KR] and [AP1] is made clear in [A2].

Birkhoff’s Covariety Theorem actually holds for all endofunctors of Set, not necessarily varietors, as proved in [A2]—however, a somewhat subtle analysis of the concept of coequation is needed then.

4.21. Remark. Some results useful in coalgebra request that the endofunctor H should weakly preserve pullbacks, i.e., map pullback squares to weak pullback squares (where the latter have the factorization property of pullbacks, except that the uniqueness of factorizations is not required). This assumption is relatively weak, e.g. in 𝒜 = Set the collection of all endofunctors weakly preserving pullback contains

(a) all polynomial endofunctors,

(b) the power-set functor,

and

(c) any product, coproduct, power or composite of functors weakly preserving pullbacks.

Consequently, the functors (−)^{Σ} × bool, used for automata, see 2.1, and 𝒫(Σ × −) , used for labeled transition systems, see 2.3, weakly preserve pullbacks. In contrast, (−)_{2}^{3}, see 4.9, does not weakly preserve pullbacks.

An example of consequences of the above property we recall that if an endofunctor H weakly preserves pullbacks, then every monomorphism in Coalg H is strong, even regular, see [R1].

5. Bisimulation and Coinduction

5.1. Motivating Example. Consider labeled transition systems as coalgebras of 𝒫(Σ × −) , see 2.3. The concept of (strong) bisimulation goes back to R. Milner [M]: it is an equivalence between states “based intuitively on the idea that we wish to distinguish between two states if the distinction can be detected by an external agent interacting with each of them”. Formally, a state a_{1} in a labeled transition system A_{1} is bisimilar to a state a_{2} in A_{2} provided that there exists a relation R between the state sets A_{1} and A_{2} such that

(i) a_{1} is related to a_{2}, i.e., a_{1} R a_{2}

(ii) for every related pair b_{1} R b_{2} and every transition b_{1} [figure: s] b′_{1} in A_{1} there exists a transition b_{2} [figure: s] b′_{2} in A_{2} with b′_{1} R b′_{2}

and (iii) for every related pair b_{1} R b_{2} and every transition b_{2} [figure: s] b′_{2} in A_{2} there exists a

transition b_{1} [figure: s] b′_{1} in A_{1} with b_{1} R b′_{1}.

This is quite natural—and rather clumsy. The conditions (ii) and (iii) can be elegantly summarized by saying that there is a dynamics on the relation R, i.e., a function

R [figure: ϱ] 𝒫(Σ × R)

for which both projections r_{i}: R [figure] A_{i} (i = 1, 2) become coalgebra homomorphism. The equivalence between this and (ii) & (iii) above follows from the description of coalgebra homomorphism in 2.3.

5.2. Remark. (1) In the category of sets the above example led P. Aczel [Ac] to define a bisimulation between two H-coalgebras A_{1} and A_{2} as a relation R ⊆ A_{1} × A_{2} for which there exists a dynamics R [figure] HR turning both projections r_{i}: R [figure] A_{i} (i = 1, 2) into homomorphisms of H-coalgebras.

(2) In a general finitely complete category with (epi, strong mono)-factorizations (see 4.10 for an explanation of this factorization system), a relation between objects A_{1} and A_{2} is a strong subobject of A_{1} × A_{2}. This is represented by a strong monomorphism R [figure] A_{1} × A_{2}, or, equivalently, by a pair of morphisms

[figure: A_{1}; A_{2}; R; A_{1}; r_{1}; R; A_{2}; r_{2}]

with the property that the induced morphism ⟨r_{1}, r_{2}⟩: R [figure] A_{1}×A_{2} is a strong monomorphism.

(3) Recall that relations are ordered (as strong subobjects of A_{1} × A_{2}) and can be composed by applying pullbacks as follows: given a relation S between A_{2} and A_{3} (represented

by s_{1} : S  [figure] A_{2} and s_{2} : S  [figure] A_{3}), form a pullback

[figure: R; S; P; R; t_{1}; P; S; t_{2}; A_{1}; A_{2}; R; A_{1}; r_{1}; R; A_{2}; r_{2}; A_{2}; A_{3}; S; A_{2}; s_{1}; S; A_{3}; s_{2}]

of r_{2} and s_{1}. Factorize ⟨r_{1}t_{1}, s_{2}t_{2}⟩: P [figure] A_{1} ×A_{3} as an epimorphism followed by a strong monomorphism, then the latter represents the composite R ∘ S.

(4) For every relation r_{i}: R_{i} [figure] A_{i}, i = 1, 2, between A_{1} amd A_{2} the opposite relation R^{−1} between A_{2} and A_{1} is represented by r_{2} and r_{1}.

(5) A relation R between A and A is called an equivalence relation if it is reflexive (i.e., it contains the diagonal of A), symmetric (i.e., R = R^{−1}) and transitive (i.e., R = R ∘ R).

5.3. Definition. By a bisimulation between H-coalgebras (A_{1}, α_{1}) and (A_{2}, α_{2}) is meant a relation r_{i}: R [figure] A_{i} (i = 1, 2) such that exists a dynamics on R making both r_{1} and r_{2} homomorphisms of H-coalgebras.

5.4. Examples. (1) The diagonal relation on A_{1}, represented by id, id: A_{1} [figure] A_{1}, is a bisimulation between (A_{1}, α_{1}) and itself.

(2) If R is a bisimulation between A_{1} and A_{2}, then the opposite relation R^{−1} is a bisimulation between A_{2} and A_{1}.

(3) If H weakly preserves pullbacks, then a composite of bisimulations is a bisimulation, see [R1]. In fact, for 𝒜 = Set, nonempty pullbacks are sufficient—and the converse also holds: if for an endofunctor H bisimulations on H-coalgebras are closed under composition, then H weakly preserves nonempty pullbacks, see [GS2].

5.5. Proposition. Let 𝒜 be a well-powered, complete category with coproducts, and let H be an endofunctor preserving strong monomorphisms. Then for every pair of coalgebras there exists a largest bisimulation between them.

Proof. Given algebras (A_{1}, α_{1}) and (A_{2}, α_{2}), since A_{1} ×A_{2} has only a set of subobjects, there exists a set of representatives:

[figure: A_{1}; A_{2}; R^{t}; A_{1}; r_{1}^{t}; R^{t}; A_{2}; r_{2}^{t}] (t ∈ T)

of all bisimulations.

We form a coproduct R = ∐_{t∈T} R_{t} in 𝒜 and obtain morphisms r_{i} = [r_{i}^{t}]_{t∈T}: R [figure] A_{i} for i = 1, 2. There exists a dynamics ϱ: R [figure] HR turning r_{1} and r_{2} into a homomorphisms (in fact, use the dynamics that exist on each R_{t}). Factorize ⟨r_{1}, r_{2}⟩: R [figure] A_{1} × A_{2} into an epimorphism followed by a strong subobject \overline{R} of A_{1} × A_{2}. Then \overline{R} is a bisimulation due to 4.13. Obviously, it contains each R_{t}, i.e., it is the largest bisimulation.

5.6. Corollary. If H moreover preserves weak pullbacks, then on every coalgebra there exists a largest bisimulation which is an equivalence relation.

In fact, reflexivity follows from 5.4(1), symmetry from 5.4(2), and transitivity from 5.4(3).

5.7. Definition. The largest bisimulation on a given coalgebra is called the bisimilarity.

5.8. Remark. (i) Let H weakly preserve pullbacks and have a terminal coalgebra T. For every coalgebra (A, α) we form the kernel equivalence of the unique homomorphism ⟦α⟧: A [figure] T, i.e., the pullback

[figure: A; A; P; A; p_{1}; P; A; p_{2}; A; T; ⟦α⟧; A; A; A; T; ⟦α⟧]

It is easy to see that P is a relation, i.e., ⟨p_{1}, p_{2}⟩ is a strong monomorphism. And since H weakly preserves pullbacks, P is a bisimulation. It follows easily that this is the bisimilarity relation:

bisimilarity = kernel of the unique homomorphism ⟦α⟧.

(ii) The condition of weakly preserving pullbacks is not needed here: it is sufficient to assume that H weakly preserves kernel pairs of nonempty maps. For 𝒜 = Set this last condition is equivalent to stating that every congruence (see 4.7) of every coalgebra is a bisimulation (as proved in [GS2]). This is not the case in general:

5.9. Example. (See [AM].) For the coalgebra A of Example 4.9 the largest equivalence relation, i.e., A × A, is a congruence: it is the kernel equivalence of the unique homomorphism ⟦α⟧. However, this is not a bisimulation.

5.10. Example. (i) For labeled transition systems the above definition of bisimilarity agrees with that of Example 5.1: given a span of homomorphisms r_{i}: R [figure] A_{i}, i = 1, 2, then the relation of all (r_{1}x, r_{2}x), x ∈ R, fulfils (ii) and (iii).

(ii) For HX = X + 1 (see 3.8), given partial unary algebras A_{1} and A_{2}, then elements a_{1} ∈ A_{1} and a_{2} ∈ A_{2} are bisimilar iff the final homomorphisms ⟦α⟧: A_{i} [figure] \overline{ℕ} fulfils

⟦α_{1}⟧a_{1} = ⟦α_{2}⟧a_{2}.

That is, iff the operations α_{i}: A_{i} [figure] A_{i} + 1 fulfil:

α_{1}^{n}(a_{1}) is defined ⟺ α_{2}^{n}(a_{2}) is defined

for all n = 1, 2, 3, …

(iii) For HA = A × A + 1 we consider two deterministic systems, A_{1} and A_{2}, having inputs 0, 1 and deadlock states. States a_{1} ∈ A_{1} and a_{2} ∈ A_{2} are bisimilar iff the unfoldings of a_{1} and a_{2} are equal. Example:

[figure: A_{1}; x; y; 0; z; 1; 0,1]

[figure: A_{2}; p; q; 0; 1; 1; r; 0; 0,1]

The states y and q are bisimilar, but no state of A_{2} is bisimilar to x.

(iv) A terminal coalgebra of

𝒫_{f}

(the finite power-set functor, see 2.7) has been described by M. Barr [B2] as the quotient coalgebra of the coalgebra of all finitely branching trees modulo bisimilarity. A simpler description is due to J. Worrell [W1]: A nonordered finitely branching tree is called strongly extensional if two children of one parent defining bisimilar subtrees are always equal. (Recall that trees are considered up-to tree isomorphism, and being 𝒫_{f}-coalgebras, see 2.7, we have the concept of bisimilarity for them.)

The set T of all finitely branching, strongly extensional trees has a natural dynamics α: T [figure] 𝒫_{f}T assigning to every tree the set of all maximum proper subtrees. This coalgebra is terminal.

5.11. Corecursion. This is a method of constructing morphisms from an object A into a terminal coalgebra T by equipping A with a “suitable” dynamics α: A [figure] HA for which the desired morphism is ⟦α⟧: A [figure] T.

The following examples stem from [R1].

5.12. Example. Corecursive definition of addition. Recall the terminal coalgebra \overline{ℕ} of HX = X + 1, 3.8(i), and search for a dynamics

add: \overline{ℕ} × \overline{ℕ} [figure] \overline{ℕ} × \overline{ℕ} + 1

such that

⟦add⟧: \overline{ℕ} × \overline{ℕ} [figure] \overline{ℕ}

is the usual addition + of natural numbers extended with ∞. That is, such that the following square, where ∗ is the unique element of 1,

[figure: \overline{ℕ}; \overline{ℕ} ∪ \{∗\}; τ; \overline{ℕ} × \overline{ℕ}; \overline{ℕ}; (+); \overline{ℕ} × \overline{ℕ}; \overline{ℕ} × \overline{ℕ} ∪ \{∗\}; add; \overline{ℕ} × \overline{ℕ} ∪ \{∗\}; \overline{ℕ} ∪ \{∗\}; (+)∪id_{1}]

commutes. That is, for (n, m) ≠ (0, 0) the result (n′, m′) of add fulfils n+m−1 = n′ +m′. It is not difficult to see that the following dynamics “works”:

add(n, m) = \begin{cases}(n − 1, m) & if n > 0; \\ (0, m − 1) & if n = 0 and m > 0; \\ ∗ & if m = n = 0. \end{cases}

5.13. Example. Corecursive definitions of infinite streams. Here we use the terminal coalgebra Σ^{ω} of HX = Σ × X, see 3.8(ii). For every symbol a ∈ Σ we can define the element a^{ω} of Σ^{ω} (the stream of all a’s) by using the obvious dynamics on the set 1:

a: 1 [figure] Σ ≅ Σ × 1.

Then

⟦a⟧: 1 [figure] Σ^{ω}

is the desired stream. In fact, since the following square

[figure: Σ^{ω}; Σ × Σ^{ω}; ⟨head,tail⟩; 1; Σ^{ω}; ⟦α⟧; 1; Σ^{ω}; a; Σ^{ω}; Σ × Σ^{ω}; id ×⟦a⟧]

commutes, we have

head⟦a⟧ = a

and

tail⟦a⟧ = ⟦a⟧

which is precisely (a coinductive) definition of a^{ω}.

How can we define e.g. (a b a b a b …) = (ab)^{ω}?

Here we use a dynamics on 1 + 1:

a + b: 1 + 1 [figure] Σ + Σ ≅ Σ × (1 + 1).

Then

⟦a + b⟧: 1 + 1 [figure] Σ^{ω}

is easily seen to have components (ab)^{ω} and (ba)^{ω}, respectively.

5.14. Example. Corecursive definition of zipping. We want to define the binary operation on Σ^{ω} which zips two streams v and w into one by taking successively an element of v, then an element of w, then one of v etc. For that, we want to find a dynamics

zip: Σ^{ω} × Σ^{ω} [figure] Σ × Σ^{ω} × Σ^{ω}

with the property that

⟦zip⟧: Σ^{ω} × Σ^{ω} [figure] Σ^{ω}

is the desired zipping operation.

The general strategy for describing α from ⟦α⟧ is: α does the first step which ⟦α⟧ infinitely repeats. This suggests to try

zip(v, w) = (head v, w, tail v)

or, more succinctly (using projections π_{1} and π_{2} of Σ^{ω} × Σ^{ω}):

zip = ⟨head ·π_{1}, π_{2}, tail ·π_{1}⟩.

In fact, since ⟦zip⟧ is a coalgebra homomorphism we have that

head(⟦zip⟧(v, w)) = head v

and

tail(⟦zip⟧(v, w)) = ⟦zip⟧(w, tail v)

which is the desired operation.

5.15. Coinduction. This is a method of proofs using the fact that no two states of a terminal coalgebra T [figure: τ] HT are bisimilar. Thus, in order to verify the equality of two states of T, it is sufficient to find a bisimulation on T under which they are related.

5.16. Example. Commutativity of addition. We want to prove

⟦add⟧(n, m) = ⟦add⟧(m, n).

We are looking for a bisimulation R on the terminal coalgebra \overline{ℕ} of HA = A + 1 with

⟦add⟧(n, m) R ⟦add⟧(m, n).

In fact, we will find a bisimulation equivalence ∼ which means that the canonical epimorphism e: \overline{ℕ} [figure] \overline{ℕ}/∼ carries a homomorphism (for some α). This is equivalent to the statement that if i ∼ j then τi ∼ τ(j), i.e., if one of i, j is zero, then both are, else, i − 1 ∼ j − 1. From the coinductive definition of ⟦add⟧ we get

[figure: \overline{ℕ}/∼; \overline{ℕ}/∼ + 1; α; \overline{ℕ}; \overline{ℕ}/∼; e; \overline{ℕ}; \overline{ℕ} + 1; τ; \overline{ℕ} + 1; \overline{ℕ}/∼ + 1; e+id_{1}]

⟦add⟧(n, m) − 1 = \begin{cases}⟦add⟧(n − 1, m) & if n > 0; \\ ⟦add⟧(0, m − 1) & if n = 0, m > 0 \end{cases}

and we conclude that the smallest equivalence relation ∼ with ⟦add⟧(n, m) ∼ ⟦add⟧(m, n) for all m, n is indeed a bisimulation of \overline{ℕ}. This proves that ∼ is the identity relation, i.e., that ⟦add⟧ is commutative.

5.17. Example. The equality ⟦zip⟧(a^{ω}, b^{ω}) = (ab)^{ω}. We try to define a bisimulation equivalence ∼ on the terminal coalgebra Σ^{ω} satisfying

(2)  ⟦zip⟧(a^{ω}, b^{ω}) ∼ (ab)^{ω}.

To say that ∼ is a bisimulation equivalence means that the following square

[figure: Σ^{ω}/∼; Σ × Σ^{ω}/∼; α; Σ^{ω}; Σ^{ω}/∼; e; Σ^{ω}; Σ × Σ^{ω}; ⟨head,tail⟩; Σ × Σ^{ω}; Σ × Σ^{ω}/∼; id ×e]

commutes for some α. Equivalently: given streams v ∼ w then

head v = head w

and tail v ∼ tail w.

¿From the coinductive definitions of a^{ω}, b^{ω}, (a, b)^{ω} and zip it clearly follows that

head⟦zip⟧(a^{ω}, b^{ω}) = a = head(ab)^{ω},

and

tail⟦zip⟧(a^{ω}, b^{ω}) = ⟦zip⟧(b^{ω}, a^{ω}),
tail(a, b)^{ω} = (ba)^{ω}.

Thus, let ∼ be the equivalence relation on Σ^{ω} whose only nontrivial equivalence classes are given by (2) and

(3)  ⟦zip⟧(b^{ω}, a^{ω}) ∼ (ba)^{ω}.

Then ∼ is a bisimulation equivalence. By coinduction, this proves

⟦zip⟧(a^{ω}, b^{ω}) = (ab)^{ω} and ⟦zip⟧(b^{ω}, a^{ω}) = (ba)^{ω}.

5.18. Remark. Corecursion and coinduction have been used in a number of beautiful applications, e.g., a coinductive calculus of streams, automata and power series in [R2], equivalence of applicative structures in [HL], coinductive combinatorics in [R3], or in connection with distributive laws in [Br]. It is only due to lack of space that we refrain from giving any details of these applications.

6. Iterative Algebras

6.1. Remark. In the “classical world” of Σ-algebras in Set the concept of iterative algebra was introduced by Evelyn Nelson[N] in her attempt to simplify the (very complex) proof of the description of free iterative theories provided by Calvin Elgot and his collaborators [E], [BE], [EBT]. A similar concept of iterative algebra was studied by Jerzy Tiurin [T].

Recently this has been generalized to every finitary functor H: 𝒜 [figure] 𝒜 where 𝒜 is a locally presentable category: A free iterative theory on H has been described in [AMV3] as the theory of free iterative H-algebras. We indicate the procedure here.

6.2. Example. (E. Nelson) Given a Σ-algebra (or H_{Σ}-algebra) of a finitary signature Σ

α: H_{Σ}A [figure] A

by a recursive system of equations in A is meant a system

(4)  x_{1} = t_{1}(x_{1}, …, x_{n}, a_{1}, …, a_{k}) ; ⋮ ; x_{n} = t_{n}(x_{1}, …, x_{n}, a_{1}, …, a_{k})

whose right-hand sides are Σ-terms over X + A where X = {x_{1}, …, x_{n}} is a set of (bound) variables and the parameters a_{1}, …, a_{k} are elements of A. A solution of (4) is an interpretation x_{i} [figure] x_{i}^{†} ∈ A of the variables in A in such a way that the formal equations become equalities

x_{i}^{†} = t_{i}(x_{1}^{†}, …, x_{n}^{†}, a_{1}, …, a_{k}) (i = 1, …, n)

in A. There are equations which automatically have many solutions, e.g., x_{1} = x_{1}. To exclude these, we restrict ourselves to guarded systems (4) which are those such that

no t_{i} is a single variable in X (i = 1, …, n).

6.3. Definition. (See [N].) A Σ-algebra is called iterative if every guarded system (4) of equations has a unique solution.

6.4. Example. Unary algebras. If Σ consists of a single unary symbol then for every iterative algebra σ: A [figure] A we have a unique fixed point of σ: consider the guarded recursive equation

x_{1} = σ(x_{1}).

Also σ^{2} has a unique fixed point (i.e., σ has no 2-cycles): consider

\begin{matrix}x_{1} = & σ(x_{2}) \\ x_{2} = & σ(x_{1}) \end{matrix}

etc. Conversely, it is not hard to prove that every algebra such that each of σ, σ^{2}, σ^{3}, … has a unique fixed point is iterative. See [AMV3].

6.5. Example. Binary algebras. If Σ consists of a single binary symbol, the iterativity of an algebra σ: A × A [figure] A does not have a simple description. Observe that σ has a unique idempotent, due to

x = σ(x, x).

Moreover, for every a ∈ A there exists a unique ā ∈ A with ā = σ(a, ā), due to

x = σ(a, x),

etc.

“Classical” algebras are usually not iterative. For example, an iterative group (G, ∗, e) is trivial due to the unique solution of x = x ∗ e.

An example of a nice iterative algebra is the algebra T of all (finite and infinite) binary trees. The following example demonstrates the general procedure of finding solutions of recursive systems of equations: consider

\begin{matrix}x_{1} = & σ(x_{2}, a) \\ x_{2} = & σ(x_{1}, b) \end{matrix}

for binary trees a, b ∈ T. The solution x_{1}^{†} has the right-hand child a. The left-hand child is x_{2}, thus, it has b as the right-hand child, etc. Here is the whole tree

(5)  x_{1}^{†} = [figure: b; •; •; a; •; •; b; •; •; a; •; •; •; .; .; .]

Analogously for x_{2}^{†}.

6.6. Definition. (S. Ginali, see [Gi].) A Σ-tree on X (see 3.16) is called rational if it has, up-to isomorphism, only finitely many subtrees. Denote by

R_{Σ}X

the subalgebra of T_{Σ}X of all rational trees.

6.7. Example. The tree (5) is rational whenever a and b are: all subtrees of x_{1}^{†} are isomorphic to subtrees of a or b, or to x_{1}^{†} or x_{2}^{†}.

6.8. Proposition. (See [G], [N].) The rational-tree algebra R_{Σ}X is a free iterative algebra on X. That is, R_{Σ}X is iterative and for every iterative Σ-algebra A and every

function f: X  [figure] A there exists a unique homomorphism f̄: R_{Σ}X  [figure] A extending f.

6.9. Example. Let Σ be a unary signature. Then a free Σ-algebra on X is the algebra Σ^{∗} × X of all trees

[figure: σ_{n}; x; ⋮; σ_{2}; σ_{1}]

with σ_{1} … σ_{n} in Σ^{∗} and x ∈ X. The algebra T_{Σ}X = Σ^{∗} × X + Σ^{∞} consists of adding to Σ^{∗} × X all infinite sequences over Σ. And the rational-tree algebra R_{Σ}X adds to Σ^{∗} × X precisely those sequences Σ^{∞} which are “eventually periodical” (i.e., periodical after removing a finite prefix).

6.10. Remark. Let us call a system of equations (4) flat if each of the right-hand sides t_{1}, …, t_{n} is either a single element of A, or a flat term

σ(y, z, …) ∈ X^{k}

for some operation symbol σ ∈ Σ_{k} and for k (not necessarily distinct) variables y, z, … in X. E. Nelson observed in [N] that a Σ-algebra is iterative iff every flat system of equations (4) has a unique solution. This serves for us as a basis for a categorical generalization: a flat recursive equation system in A is, obviously, represented by a function

e: X [figure] H_{Σ}X + A

where X is the (finite) set of variables. In fact, e assigns to every variable the appropriate right-hand side. This leads us to the following generalization using finite presentability (see 3.15c):

6.11. Definition.  Given an endofunctor H, an H-algebra α: HA  [figure] A is called

iterative provided that every finitary flat equation morphism

e: X  [figure] HX + A  (X finitely presentable)

there exists a unique solution, i.e., a unique morphism

e^{†}: X [figure] A

such that the square

(6)  [figure: HX + A; HA + A; He^{†}+A; X; HX + A; e; X; A; e^{†}; A; HA + A; [α,A]]

commutes.

6.12. Remark. For polynomial endofunctors and flat systems

(i) guardedness is not mentioned explicitly: flat implies guarded, and

(ii) the square (6) precisely expresses the condition that the function e^{†}: x_{i} [figure] x_{i}^{†} from X to A is a solution: if the right-hand side t_{i} is an element a ∈ A, then x_{i}^{†} = a, and if t_{i} is a flat term t_{i} = σ(y, z, …), then x_{i}^{†} = σ(y^{†}, z^{†}, …) means e^{†}(x_{i}) = α·H_{Σ}e^{†}·e(x_{i}).

6.13. Example. (See [Mo] or [AAMV].) Terminal coalgebras are iterative. More

precisely, if T [figure: τ] HT is a terminal coalgebra, then HT [figure: τ^{−1}] T is an iterative algebra. Applied to H(−) + Y (compare 2.9) this tells us that whenever a terminal coalgebra T Y of H(−) + Y exists then the corresponding H-algebra T Y is iterative.

6.14. Proposition. (See [AMV3].) Iterative algebras are closed in Alg H under limits and filtered colimits. Consequently, the category of iterative algebras and homomorphisms is reflective in Alg H.

6.15. Corollary. Free iterative algebras exist.

In fact, since H is a finitary functor, free H-algebras exist, see [A0], in other words, the canonical forgetful functor U: Alg H [figure] 𝒜 has a left adjoint. Since the embedding E: Alg_{it} H [figure]Alg H of the full subcategory of all iterative algebras also has a left adjoint (by 6.14), the forgetful functor UE: Alg_{it} H [figure] 𝒜 also has a left adjoint.

6.16. Remark. The above proposition takes all homomorphisms as the choice of morphisms for iterative algebras. The reader may wonder whether a more appropriate choice should be considered, involving “preservation of solutions”. In fact, the interpretation of the latter is rather obvious: given iterative algebras α: HA [figure] A and β: HB [figure] B and a morphism h: A [figure] B, then for every flat equation morphism in A, say e: X [figure] HX +A, we have the canonical equation morphism in B:

h • e ≡ X [figure: e] HX + A [figure: HX+h] HX + B.

We say that h preserves solutions if that for every flat equation morphism e: X [figure] HX + A the triangle

[figure: A; B; h; X; A; e^{†}; X; B; (h•e)^{†}]

commutes. Luckily, this coincides with the concept of homomorphism:

6.17. Lemma. [AMV3] Given iterative algebras (A, α) and (B, β), then a morphism h: A [figure] B preserves solutions iff it is a homomorphism.

6.18. Definition. The monad of all free iterative H-algebras is called the rational monad of H. Notation:

(R, η, μ).

Explicitly, for every object X we form a free iterative algebra RX with the algebra structure

ϱ_{X}: HRX [figure] RX

and the universal arrow

η_{X}: X [figure] RX.

And we denote by

μ_{X}: R(RX) [figure] RX

the unique homomorphism with μ_{X}·η_{RX} = id.

6.19. Examples. (See [A3].)

(1) For the polynomial functors H_{Σ} in Set, the rational monad R_{Σ} is the rational-tree monad, see 6.8.

(2) Let 𝒫_{2} : Set [figure] Set denote the functor assigning to a set X the set 𝒫_{2}X of all non-ordered pairs in X, defined on maps f: X [figure] Y by 𝒫_{2}f: {x, y} [figure] {f(x), f(y)}. Observe that 𝒫_{2}-algebras are just binary algebras whose operation is commutative.

The rational monad assigns to a set X the set RX of all nonordered rational binary trees with leaves labeled in X. This is an obvious quotient monad of the rational monad R_{Σ} where Σ consists of one binary operation.

(3) The rational monad of 𝒫_{f}, the finite-power-set functor, is the monad of all strongly extensional (see 5.10(iv)) rational, finitely branching trees.

6.20. Remark. The above examples demonstrate the following general description of rational monads on Set:

Given a finitary endofunctor H there exists a finitary signature Σ such that H is a quotient of H_{Σ}. (For example, in case of 𝒫_{f} consider Σ having a single n-ary operation σ_{n} for every n = 0, 1, 2, …) There are equations between flat (see 6.10) Σ-terms such that H is obtained from H_{Σ} by applying these equations finitely many times—we call these equations basic. (Example: for 𝒫_{f} the basic equations are all the equations

σ_{n}(x_{1}, …, x_{n}) = σ_{k}(y_{1}, …, y_{k})

where {x_{1}, …, x_{n}} = {y_{1}, …, y_{k}}.)

Then the rational monad R of H is obtained from the rational monad R_{Σ} as a quotient modulo the congruence obtained by applying the basic equations finitely or infinitely many times. See [A3] for a precise definition of infinite application of equations (and a precise proof of the above description of R).

6.21. Remark. (See [AMV3].) (1) Observe that the morphisms ϱ_{X}: HRX [figure] RX and η_{X}: X [figure] RX of 6.18 form natural transformations

ϱ: HR  [figure] R and η: Id  [figure] R

with the property that R is a coproduct

R = HR + Id with injections ϱ and η.

(2) Every iterative Σ-algebra allows for a canonical computation of rational terms, i.e., terms expressed by rational trees. This is the special case of the following general phenomenon:

Given an iterative algebra HA [figure: α] A, we obtain the unique homomorphism

α̂: RA [figure] A

of H-algebras with α̂·η_{A} = id. Then (A, α̂) is an Eilenberg-Moore algebra of the rational monad.

However, iterative algebras are not monadic on 𝒜; the category of Eilenberg-Moore algebras of R is described in [AMV4] as the category of all Elgot algebras. These are algebras with specified solutions of flat equation morphisms such that the specification satisfies two (rather simple) axioms.

7. Iterative Theories

7.1. Remark. What is the connection of Section 6 to coalgebra? It turns out that there is one that is deep, technically difficult to prove, and useful:

7.2. Theorem. (See [AMV3].) Let H be a finitary endofunctor of a locally finitely presentable category. Then the initial iterative algebra, RO, can be constructed as a filtered colimit of all H-coalgebras on finitely presentable objects.

7.3. Corollary. Let Eq_{Y} be the diagram of all coalgebras of H(−) + Y on finitely presentable objects (that is, all finitary, flat equation morphisms e: X [figure] HX + Y). Then the objectwise description of the rational monad on H is

RY = colim Eq_{Y} .

7.4. Remark. One consequence of Theorem 7.2 is the fact that, precisely as in the case of Σ-algebras (see Remark 6.9), every iterative algebra A allows for unique solutions of non-flat equation morphisms if they are guarded.

Generalizing flat equation morphism (see 6.10), let us call a morphism

e: X [figure] R(X + A) X finitely presentable

a rational equation morphism. It is guarded if it factorizes through the first summand of R(X + A) = [HR(X + A) + A] + X (see 6.21):

[figure: X; R(X + A); e; HR(X + A) + A; X; HR(X + A) + A; R(X + A); [ϱ_{X+A},η_{X+A}· inr]]

This generalizes, in case of H_{Σ}, the equation system (4) of 6.2 by allowing the righthand sides to be not only terms, i.e., finite Σ-trees, but also rational Σ-trees. Now the concept of solution in Example 6.2 generalizes as follows (using the notation α̂ of Remark 6.21):

7.5. Theorem. For every iterative algebra HA [figure: α] A and every guarded rational equation morphism e: X [figure] R(X + A) there exists a unique solution e^{†}: X [figure] A i.e., a unique morphism such that the square

commutes.

[figure: R(X + A); RA; R[e^{†},A]; X; R(X + A); e; X; A; e^{†}; A; RA; α̂]

7.6. Remark. In the language of algebraic theories (i.e., finitary monads on Set) the above Theorem together with Remark 6.21 tell us that the rational monad is an iterative algebraic theory for every finitary endofunctor of Set. Recall the concept of an iterative theory of C. Elgot [E] as rephrased categorically in [AAMV] for monads over locally finitely presentable categories:

(a) A monad (S, η, μ) is called ideal if S has a subfunctor σ: S′ [figure] S such that

(i) S is a coproduct S = S′ + Id (with injections σ: S′ [figure] S and the unit η: Id [figure] S) and

(ii) μ has a restriction to a natural transformation

μ′: S′S [figure] S′ with σ·μ′ = μ·σS.

More precisely, the sixtuple (S, η, μ, S′, σ, μ) is called an ideal monad.

Example: let 𝒜 be a locally finitely presentable category in which coproduct injections are monic. The rational monad R = HR + Id (see 6.20) is ideal w.r.t. the subfunctor ϱ: HR [figure] R and μ′ = Hμ.

(b) Given an ideal monad, by a finitary equation morphism is meant a morphism

e: X [figure] S(X + Y)

where X is a finitely presentable object, and Y is an arbitrary object; e is called guarded if it factorizes through the first summand of S(X + Y) = [S′(X + Y) + Y] + X.

(c) The ideal monad is called iterative provided that for every guarded finitary equation morphism e there exists a unique solution e^{†}, i.e., a unique morphism e^{†}: X [figure] SY such that the square

[figure: S(X + Y); SSY; S[e^{†},η_{Y} ]; X; S(X + Y); e; X; SY; e^{†}; SY; SSY; μ_{Y}]

commutes.

(d) Given an ideal monad S, by an ideal natural transformation from a functor H to S is called a natural transformation H [figure] S which factorizes through σ. Example: if R is the rational monad of H (w.r.t. ϱ: HR [figure] R, see 6.21), then the canonical natural transformation κ from H to R:

κ ≡ H [figure: Hη] HR [figure: ϱ] R

is ideal.

For two ideal monads (S, η, μ, S′, σ, μ′) and (\overline{S}, \overline{η}, \overline{μ}, \overline{S}′, \overline{σ}, \overline{μ}′) we will call a given monad morphism h: (S, η, μ) [figure](\overline{S}, \overline{η}, \overline{μ}) ideal if it has a domain-codomain restriction h′: S′ [figure] \overline{S}′.

7.7. Theorem. (See [AMV3].) The rational monad R is a free iterative monad on H. That is

(i) R is an iterative monad,

(ii) for every iterative monad S and every ideal natural transformation h: H [figure] S there exists a unique ideal monad morphism h̄: R [figure] S with h = h̄·κ.

8. Complete Iterativity

8.1. Assumption. In this section H denotes an endofunctor of a category 𝒜 having finite coproducts with monic injections.

The present section is distinguished from the previous two by dropping the assumption, for all equation morphisms X [figure] HX + A or X [figure] R(X + A) etc., that X be finitely presentable.

8.2. Definition. An H-algebra HA [figure: α] A is completely iterative provided that for every flat equation morphism e: X [figure] HX + A, where X is an arbitrary object, there exists a unique solution e^{†}: X [figure] A (defined, again, by the commutativity of the square (6) see 6.11).

8.3. Example. (See [Mo] or [AAMV].) (i) If T [figure: τ] HT is a terminal H-coalgebra,

then HT [figure: τ^{−1}] T is an initial completely iterative H-algebra.

(ii) More generally: let us call H iteratable, i.e., for every object Y a terminal coalgebra, T Y, of H(−) + Y exists. It follows that T Y is a coproduct

T Y = HT Y + Y  with injections τ_{Y} : HT Y  [figure] T Y, η_{Y} : Y  [figure] D

and the H-algebra (T Y, τ_{Y}) is completely iterative.

8.4. Theorem. (See [Mi].) If H is iteratable, then T Y is a free completely iterative H-algebra on Y. Conversely, whenever free completely iterative H-algebras exist, then H is iteratable.

8.5. Example. (See [AAMV].) If 𝒜 is locally presentable, then every accessible endofunctor (see 3.15) is iteratable. But there exist iteratable functors which are not accessible.

8.6. Remark. We can define completely iterative monads precisely as in Remark 7.6, just dropping the assumption of X being finitely presentable (everywhere). Then analogously to 7.7 we obtain the result that the monad T of free completely iterative algebras is a free completely iterative monad on H; see [AAMV].

8.7. Example. For polynomial endofunctors H_{Σ} of Set the above monad is the monad T_{Σ} of all Σ-trees. This is the original example of a free completely iterative monad on Σ introduced in [EBT].

9. Parametrized Iterativity

9.1. Remark. Tarmo Uustalu proposed in [U] a generalization of the environment in which iterativity is studied: in place of a finitary functor H: 𝒜 [figure] 𝒜 he considers a finitary functor H: 𝒜 [figure] F M(𝒜),

where F M(𝒜) is the category of finitary monads

on 𝒜. We briefly sketch the basic situation of Σ-algebras with parametrized iterativity which this environment is capable to represent, and then formulate the appropriate generalization of the results of Section 7.

9.2. Example. (See [AMV5].) Consider first one binary operation σ. In the original concept of iterative algebras of E. Nelson (see Example 6.5) both variables x_{1} and x_{2} in σ(x_{1}, x_{2}) can be used for iteration in the equational systems (4) of Example 6.2. This leads to the rational monad R_{Σ} of all rational binary trees.

Now let us decree that x_{1} can be used for iteration, but x_{2} cannot. This corresponds to equation systems (4) where the right-hand sides t_{i} all have the form

(7)  [figure: x′; a; x; x; a; a; ,; ,; ,; etc]

for variables x, x′, … in X and an element a ∈ A.

Again, we call an algebra A × A [figure: σ] A iterative if every such guarded system of equations has a unique solution. This is strictly weaker than the original concept of iterativity—e.g., here an iterative algebra does not need to posses an idempotent element.

We can formalize this weaker iterativity by introducing, for every set X, the “derived” signature of all operation symbols σ(x, −) (unary), for x ∈ X. Let us denote by

X □ A

a free algebra of this signature on A—this is precisely where the right-hand sides (7) lie. That is, the current form of finitary equation morphisms is

e: X [figure] X □ A (X is finite).

Now X □ − is a monad of Set, the free-algebra monad of the derived signature given by X ↦ X^{∗} × A. Thus □ is the uncurried version of a functor from Set to F M(Set) (assigning to every set X the monad A ↦ X □ A). Also, every binary algebra σ: A × A [figure] A defines an Eilenberg-Moore algebra

σ̂: A □ A [figure] A

of the monad A □ −: the function σ̂: A^{∗} × A [figure] A computes the terms of A □ A in A. (Conversely, every Eilenbderg-Moore algebra of A□− on the set A is uniquely determined by some σ.)

An algebra σ: A × A [figure] A is now called iterative if for every finitary equation morphism e: X [figure] X □ A there exists a unique solution e^{†}: X [figure] A given by the commutativity of

[figure: X □ A; A □ A; e^{†}□A; X; X □ A; e; X; A; e^{†}; A; A □ A; σ̂]

A free iterative algebra in the present sense is the algebra of all rational binary trees on X which are right-wellfounded, i.e., the right-most path from any node is always finite.

9.3. Example. (See [AMV5].) The previous example is a special case of a parametrized signature, i.e., a signature Σ with an additional function assigning to every symbol σ of arity n a number

it(σ) = 0, 1, …, n (the iterativity of σ).

This additional function does not play any role for the concept of Σ-algebra and homomorphism. But it influences our concept of recursive system of equations, see 6.2: we allow, for every node of a right-hand side tree t_{i} labeled by σ, only the first it(σ) children to be iteratable. More precisely, for (4) in 6.2 we request that

(i) every leaf of t_{i} labeled by a variable x_{1}, …, x_{n} has a parent labeled by σ ∈ Σ, and the leaf is one of the first it(σ) children

and

(ii) every inner node of t_{i} labeled by σ ∈ Σ has the first it(σ) children labeled by a variable x_{1}, …, x_{n}.

A Σ-algebra is called iterative (w.r.t. the parametrized signature) if every such guarded system of recursive equations has a unique solution.

An elegant way of getting rid of the complicated conditions (i) and (ii) is to form, for every set X of variables, the derived signature of all symbols

σ(x_{1}, …, x_{i}, −) for σ ∈ Σ, i = it(σ) and (x_{1}, …, x_{i}) ∈ X^{i}

having arity ar(σ) − i. Denote by

X □ A

a free algebra of A of the last signature. Then (i) and (ii) precisely describe the trees that naturally form X □ A. In other words, a recursive system of equations is now expressed by a morphism

e: X  [figure] X □ A,  X finite.

Observe also that by fixing X we obtain a monad

X □ − in F M(Set).

Namely: the free-algebra monad of the above derived signature. And every function f: X [figure] Y defines a canonical morphism f □ −: (X □ −) [figure] (Y □ −). Thus, X □ − is an uncurried version of a functor

□: Set [figure] F M(Set).

It is easy see that □ is finitary (in both variables) and thus is a special case of the following

9.4. Definition. (1) (See [U].) By a base, or parametrized finitary monad, on 𝒜 is meant a finitary functor from 𝒜 to F M(𝒜). We use the uncurried notations of □: 𝒜 × 𝒜 [figure] 𝒜, a functor of two variables defining a monad in the second variable.

(2) (See [AMV5].) A base algebra is an object A together with a morphism α: A □ A [figure] A forming an Eilenberg-Moore algebra of the monad A □ −.

More detailed, a base consists of a functor

X □ A (X, A ∈ 𝒜)

of two variables together with natural transformations

u_{A}^{X}: A [figure] X □ A (monad unit)

and

m_{A}^{X}: X □ (X □ A) [figure] X □ A (monad multiplication)

satisfying the usual axioms of a monad (X □ −, u^{X}, m^{X}), and coherence conditions for the variable object X.

9.5. Example. Binary algebras in Set lead to three bases (corresponding to the three ways of deciding the iterativity it(σ): two, one, or none).

(a) The base corresponding to the classical concept of E. Nelson (it(σ) = 2, i.e., both variables can be iterated) uses the derived signature of constant symbols indexed by X × X. The free algebra on A is

X □ A = (X × X) + A.

The monadic structure is given by u_{A}^{X} = right injection and m_{A}^{X} = ▽_{X×X} +A: (X ×X)+ (X × X) + A [figure] (X × X) + A.

(b) The base corresponding to iterating x_{1} but not x_{2} (it(σ) = 1) uses the derived signature of unary operations σ(x, −) indexed by x ∈ X. The free algebra on A is

X □ A = X^{∗} × A

where (X^{∗}, 1 [figure: u] X^{∗}, X^{∗} × X^{∗} [figure: m] X^{∗}) is a free monoid. The monadic structure is given by the neutral element:

u_{A}^{X} ≡ A = 1 × A [figure: u×A] X^{∗} × A

and by the concatenation c: X × X^{∗} [figure] X^{∗}:

m_{A}^{X}: X^{∗} × X^{∗} × A [figure: c×A] X^{∗} × A.

(c) The base corresponding to iterating neither x_{1} nor x_{2} (it(σ) = 0) is

X □ A = Â, free binary algebra on A

(independent of X).

9.6. Definition. (See [AMV5].) A base algebra α: A □ A [figure] A is called iterative provided that for every finitary equation morphism

e: X  [figure] X □ A  (X finitely presentable)

there exists a unique solution, i.e., a morphism e^{†}: X [figure] A such that the square

[figure: X □ A; A □ A; e^{†}□A; X; X □ A; e; X; A; e^{†}; A; A □ A; σ̂]

commutes.

9.7. Example. For the base X □ A = (X × X) + A this is precisely the concept of E. Nelson. The base X □ A = X^{∗} × A yields the iterative algebras of Example 9.2. And for the last base X □ A = Â every algebra is iterative.

9.8. Remark. The theory of free iterative algebras and the corresponding free iterative monad, as presented in Sections 6 and 7 above, extend fully to base algebras (but the proofs are technically more involved). In particular:

(a) free iterative base algebras exist,

(b) they can be constructed coalgebraically (as filtered colimits of categories of equations),

(c) the corresponding monad R on 𝒜, called the rational monad of the base □, is iterative in the appropriate sense, and

(d) the rational monad can be characterized by a universal property.

See [AMV5].

10. Coalgebra in Classes

10.1. Remark. All the basic examples of systems mentioned above are coalgebras for endofunctors of Set, the category of small sets. Here we extend this category to the category Class of classes, and we show how life simplifies with this extension. Our concern is not with questions of foundations of set theory: we work in the “classical” setting with the Axiom of Choice and with a specified universe Set of small sets. The Axiom of Choice (assumed for all, not necessarily small, sets) yields a cardinal of the collection of all small sets which we denote by

ℵ_{∞}.

This cardinal is strongly inaccessible, i.e., an uncountable cardinal such that k < ℵ_{∞} implies 2^{k} < ℵ_{∞}. Thus, our foundations are the common classical ones: ZFC with a choice of a strongly inaccessible cardinal ℵ_{∞}. Observe that the category Set is equivalent to the category of all sets of cardinality less than ℵ_{∞} (simply because ℵ_{∞} is the first large cardinal). This allows us to work with “small” as meaning: smaller than ℵ_{∞}. Thus, we take Set to be the category of all sets of cardinality less than ℵ_{∞}.

A class is a property of sets, i.e., a subset of the (large) set Set. Every class is either of cardinality ℵ_{∞}, or it lies in Set. Thus, we take as

Class

the category of all sets of cardinality at most ℵ_{∞}, equivalent to the usual category of classes.

10.2. Definition. (See [AM].) An endofunctor H of Class is called set-based provided that for every class X and every element b ∈ HX there exists a small subset m: Y [figure] X such that b lies in the image of Hm: HY [figure] HX.

Equivalently: H is accessible (see 3.15) for λ = ℵ_{∞}.

10.3. Theorem. (See [AMV1].) Every endofunctor of Class is set-based.

10.4. Corollary. ([See [AM].) Every endofunctor of Class has an initial algebra and a terminal coalgebra.

In the terminology of P. Freyd [F], this says that Class is algebraically complete and cocomplete.

10.5. Corollary. Every endofunctor of Set has an extension to an endofunctor of Class, unique up-to a natural isomorphism.

10.6. Example. The power-set functor 𝒫 has the extension 𝒫′: Class [figure]Class assigning to every class X the class 𝒫′X of all small subsets of X.

An initial algebra of 𝒫′ can be described as the class I of all small sets with the algebraic structure 𝒫′I [figure] I given by assigning to every subset X ⊆ I the same X, as an element of I.

A terminal coalgebra was described in [RT] as the coalgebra of all nonordered trees modulo bisimilarity. In the non-wellfounded set theory the terminal coalgebra is the coalgebra of all small non-wellfounded sets, see [Ac] or [BM].

10.7. Corollary. Every endofunctor of Class is iteratable (see 8.3).

In fact, the completely iterative monad generated by any endofunctor of Class can be described as a quotient of the tree-monad T_{Σ} for some signature Σ, as proved in [AMV1].

10.8. Theorem. (See [A2].) Every endofunctor of Class satisfies Birkhoff’s Covariety Theorem: a collection of coalgebras is presentable by coequations (see 4.18) iff it is closed under coproducts, subcoalgebras, and quotients.

10.9. Remark. Surprisingly, Birkhoff’s Variety Theorem does not hold in Class without limitations: the assumption needed is that the cardinal ℵ_{∞} is not measurable, see [AT2].

References

[Ac] P. Aczel, Non-Well-Founded Sets, CSLI Lecture Notes 14, Stanford University, 1988.

[AAMV] P. Aczel, J. Adámek, S. Milius and J. Velebil, Infinite Trees and Completely Iterative Theories: A Coalgebraic View, Theor. Comp. Sci. 300(2003), 1–45.

[AM] P. Aczel and P. F. Mendler, A Final Coalgebra Theorem, in: Category Theory and Computer Science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, A. Poigné (eds.), LNCS 389, Springer-Verlag, 1989, 357–365.

[A0] J. Adámek, Free algebras and automata realization in the language of categories, Comment. Math. Univ. Carolinae 15(1974), 589–602.

[A1] J. Adámek, Colimits of algebras revisted, Bull. Austral. Math. Soc. 17(1977), 433–450.

[A2] J. Adámek, Birkhoff’s covariety theorem without limitations, to appear in Commentationes Mathem. Universitatis Carolinae.

[A3] J. Adámek, On a description of terminal coalgebras and iterative theories, Electron. Notes Theor. Comput. Sci. 82(1)(2003).

[AHS] J. Adámek, H. Herrlich and G. E. Strecker, Abstract and Concrete Categories, Wiley Publ., New York 1990, see online version at

        http://katmat.math.uni-bremen.de/acc

[AMV1] J. Adámek, S. Milius and J. Velebil, On coalgebra based on classes, Theor. Comput. Sci. 316(2004), 2–23.

[AMV2] J. Adámek, S. Milius and J. Velebil, Free iterative theories—a coalgebraic view, Math. Structures Comput. Sci. 13(2003), 259–320.

[AMV3] J. Adámek, S. Milius and J. Velebil, ¿From iterative algebras to iterative theories, Electron. Notes Theor. Comput. Sci., to appear; full version available via

http://www.iti.cs.tu-bs.de/~milius.

[AMV4] J. Adámek, S. Milius and J. Velebil, On iterative algebras and Elgot algebras, submitted.

[AMV5] J. Adámek, S. Milius and J. Velebil, Iterative algebras for a base, Electron. Notes Theor. Comput. Sci., to appear, full version available at

http://www.iti.cs.tu-bs.de/~milius.

[AP1] J. Adámek and H.-E. Porst, On varieties and covarieties in a category, Math. Structures Comput. Sci. 13(2003), 201–232.

[AP2] J. Adámek and H.-E. Porst, On tree coalgebras and coalgebra presentations, Theor. Comput. Sci. 311(2004), 257–283.

[AR] J. Adámek and J. Rosický, Locally Presentable and Accessible Categories, Cambridge University Press, 1994.

[AT1] J. Adámek and V. Trnková, Automata and Algebras in a Category, Kluwer Publishing Company, Dordrecht, 1990.

[AT2] J. Adámek and V. Trnková, On the limitations of Birkhoff’s variety theorem, submitted.

[AMa] M. A. Arbib and E. G. Manes, Parametrized data types do not need highly constrained parameters, Information and Control 52(1982), 139–158.

[BH] B. Banaschewsky and H. Herrlich, Subcategories defined by implications, Houston J. Mathem. 2(1976), 149–171.

[B1] M. Barr, Coequalizers and free triples, Mathem. Zeitschrift 116(1970), 307–322.

[B2] M. Barr, Terminal Coalgebras in Well-Founded Set Theory, Theor. Comput. Sci. 124(1994), 182–192.

[Br] F. Bartels, Generalized coinduction, Math. Structures Comput. Sci. 13(2003), 321–348.

[BM] J. Barwise and L. Moss, Vicious circles, CSLI Lecture Notes, Vol. 60, Stanford University, Stanford, CA, 996.

[BE] S. L. Bloom and C. C. Elgot, The existence and construction of free iterative theories, J. Comput. System Sci. 12(1974), 305–318.

[BÉ] S. L. Bloom and Z. Ésik, Iterative Theories: The Equational Logic of Iterative Processes, EATCS Monograph Series on Theoretical Computer Science, Springer-Verlag, 1993.

[E] C. C. Elgot, Monadic Computation and Iterative Algebraic Theories, in: Logic Colloquium ‘73 (eds: H. E. Rose and J. C. Shepherdson), North-Holland Publishers, Amsterdam, 1975.

[EBT] C. C. Elgot, S. L. Bloom and R. Tindell, On the Algebraic Structure of Rooted Trees, J. Comp. Syst. Sciences 16(1978), 361–399.

[F] P. Freyd, Algebraically complete categories, Lecture Notes Math. 1488, Springer-Verlag 1991, 95–104.

[GU] P. Gabriel and F. Ulmer, Local präsentierbare Kategorien, Lecture Notes in Math. 221, Springer-Verlag 1971.

[Gi] S. Ginali, Regular trees and the free iterative theory, J. Comput. System Sci. 18(1979), 228–242.

[G] H. P. Gumm, Universelle Koalgebra, in T. Ihringer “Allgemeine Algebra”, Heldermann Verlag 2003.

[GS1] H. P. Gumm and T. Schröder, Products of coalgebras, Algebra Universalis 46(2001), 163–185.

[GS2] H. P. Gumm and T. Schröder, Coalgebraic structure from weak limit preserving functors, Electron. Notes Theor. Comput. Sci. 33(2000).

[HL] F. Hanzel and M. Lenisa, Coinductive characterization of applicative structures, Math. Tructures Comput. Sci. 9(1999), 403–435.

[J] B. Jacobs, Comprehension for Coalgebras, Electron. Notes Theor.Comput. Sci. 65(2002)

[JR] B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction, EATCS Bulletin 62(1997), 222–259.

[JPTW] P. Johnstone, J. Power, T. Tsujishita, H. Watanabe and J. Worrell, On the structure of categories of coalgebras, Theor. Comput. Sci. 260(2001), 87–117.

[KM] Y. Kawahara and M. Mori, A small final coalgebra theorem, Theor. Comput. Sci. 233(2000), 129–145.

[KR] A. Kurz and J. Rosický, Modal predicates and coequations, Electron. Notes Theor. Comput. Sci. 65(2002). Full version to appear in Information and Computation.

[L] J. Lambek, A Fixpoint Theorem for Complete Categories, Math. Zeitschrift 103(1968), 151–161.

[Li] F. E. J. Linton, Coequalizers in categories of algebras, in: Lecture Notes in Math., Vol. 80, Springer, Berlin 1969, 75–90.

[M] R. Milner, Communication and Concurrency, Prentice Hall, 1989.

[Mi] S. Milius, Completely iterative algebras and completely iterative monads, Inform. and Comput., to appear.

[MM] S. Milius and L. S. Moss, The category theoretic solution of recursive program schemes, submitted.

[Mo] L. Moss, Parametric Corecursion, Theor. Comput. Sci. 260(2001), 139–164.

[N] E. Nelson, Iterative algebras, Theor. Comput. Sci. 25(1983), 67–94.

[R1] J. J. M. M. Rutten, Universal coalgebra: a theory of systems, Theor. Comput. Sci. 249(1)(2000), 3–80.

[R2] J. J. M. M. Rutten, Behavioral differential equations: a coinductive calculus of streams, automata, and power series, Theor. Comput. Sci. 308(2003), 1–53.

[R3] J. J. M. M. Rutten, Coinductive counting with weighted automata, J. Autom. Lang. Comb. 8(2003), 319–352.

[RT] J. J. M. M. Rutten and D. Turi, On the foundations of final coalgebra semantics: non-well-founded sets, partital orders, metric spaces, Math. Structures Comput. Sci. 8(1998), 481–540.

[T] J. Tiurin, Unique fixed points vs. least fixed points, Theor. Comput. Sci. 12(1980), 229–254.

[U] T. Uustalu, Generalizing substitution, Theoretical Informatics and Appl., to appear.

[W1] J. Worrell, On the final sequence of a finitary set functor, Theor. Comput. Sci., to appear.

[W2] J. Worrell, Toposes of coalgebras and hidden algebras, Electron. Notes Theor. Comput. Sci. 11(1998)

Technical University of Braunschweig

Email: adamek@tu-bs.de

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/14/8/14-08.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: mbarr@barrs.org

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@mathstat.uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com

Ezra Getzler, Northwestern University: getzler(at)math(dot)northwestern(dot)edu

Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca