Theory and Applications of Categories, Vol. 19, No. 5, 2008, pp. 61–92.

ITERATIVE ALGEBRAS: HOW ITERATIVE ARE THEY?

J. ADÁMEK, R. BÖRGER, S. MILIUS, AND J. VELEBIL^{∗}

Abstract. Iterative algebras, defined by the property that every guarded system of recursive equations has a unique solution, are proved to have a much stronger property: every system of recursive equations has a unique strict solution. Those systems that have a unique solution in every iterative algebra are characterized.

1. Introduction

Iterative algebras are those algebras in which every “guarded” system of recursive equations has a unique solution. This concept, introduced by Evelyn Nelson [N] and Jerzy Tiurin [T], is important for the study of Elgot’s iterative theories. The condition of guardedness serves to exclude bad guys such as x = x. In the present paper we prove that iterative algebras are “very” iterative: every system of recursive equations has a solution, in fact, a canonical one. For the latter we need a choice of a global element ⊥ in the given iterative algebra—then we can introduce the concept of a strict solution. For example, the unique strict solution of x = x is x ↦ ⊥. We prove that every recursive equation system has a unique strict solution. We also fully characterize those systems of equations which have unique solutions in all iterative algebras; we call them preguarded.

We prove our results for all finitary endofunctors of well-behaved categories. These are the locally finitely presentable categories of Gabriel an Ulmer in which every object is a coproduct of connected objects. It turns out that each such category is extensive, but not conversely: there are locally finitely presentable, extensive categories in which an equation can have infinitely many strict solutions. We demonstrate this by an example in the category of Jónsson-Tarski algebras. Section 2 is devoted to a discussion of the base categories we need throughout the paper.

In our later research we plan to use the above “stronger iterativity” of iterative algebras for characterizing monadic algebras of the monad of free iteration theories on the category of endofunctors. And we will also use it for the first step in a “reconciliation” of iterative algebras and iteration algebras of Stephen Bloom and Zoltán Ésik [BÉ]. The latter are algebras where all systems of recursive equations have solutions, and a choice of solutions subject to axioms is performed; the motivation stems from continuous algebras on CPO’s, where recursive equations always have the least solution. The “reconciliation” mentioned above has two steps: one, the subject of the present paper, is to show that every iterative algebra has canonical solutions of all systems of recursive equations. The other step, which we attend to in the paper [ABM], is to show that these canonical solutions satisfy the axioms of iteration algebras. Related Work. This paper is a (substantially expanded) version of the extended abstract published previously [AMV_{2}]. The results of Section 2 are new, the concept of strict solution has been simplified, and Example 6.10 and Theorem 5.17 is also new. For endofunctors of Set the unique existence of strict solutions was proved by Larry Moss [Mo] and Stephen Bloom et al. [BEW_{1}], [BEW_{2}]. Our purely categorical proof is independent. Acknowledgement. We are grateful to Walter Tholen, Peter Johnstone, Francis Borceux and the referee for their interesting comments.

* Support by the grant MSM 6840770014 of the Ministry of Education of the Czech Republic is

acknowledged.

Received by the editors 2007-01-24 and, in revised form, 2008-01-07.

Transmitted by Jiří Rosický. Published on 2008-01-20.

2000 Mathematics Subject Classification: 68Q65, 18A15.

Key words and phrases: iterative algebra, guarded equation, strict solution, extensive category.

\begin{matrix}c \\ ◯ \end{matrix} J. Adámek, R. Börger, S. Milius, and J. Velebil^{∗}, 2008. Permission to copy for private use granted.

2. Hyper-Extensive Categories

In this section we introduce the categories for which the main results will be proved: they are the locally finitely presentable categories (see [GU]) which are hyper-extensive. The latter is stronger than extensivity, and for locally finitely presentable categories it states precisely that every object is a coproduct of connected objects. We recall all the concepts needed and illustrate them by examples. Since local presentability is not needed for all our results, we formulate hyper-extensivity more generally first: this turns out to be a slightly stronger condition than extensivity, see [CLW].

2.1. Remark. (i) Recall from [GU] that an object A is called finitely presentable if hom(A, −) preserves filtered colimits.

(ii) We call A connected if hom(A, −) preserves coproducts. For example, in Set the finitely presentable objects are the finite sets and the connected ones are the terminal (one-element) sets only. In the category Gra of graphs finitely presentable objects are the finite graphs, and the connected ones are the graphs with precisely one (connected) component.

(iii) It is easy to verify that a directed colimit of connected objects is always connected. (iv) Recall that a category 𝒜 is called locally finitely presentable, see [GU] or [AR],

if it has colimits and a set 𝒜_{fp} of finitely presentable objects such that every object is a filtered colimit of objects in 𝒜_{fp}. Examples: Set, Set^{I}, Gra and Pos (posets and order-preserving maps) are finitely presentable categories.

2.2. Definition. [CLW]. A category is called extensive if it has finite coproducts which are

(a) disjoint, i.e., coproduct injections are monomorphisms and the intersection of two distinct coproduct injections is always 0 (the initial object), and (b) universal, i.e., for every morphism f: C [figure] A_{1} + A_{2} the pullbacks of the coproduct injections along f exist and turn C into the corresponding coproduct:

[figure: A_{1}; A_{1} + A_{2}; inl; A′_{1}; A_{1}; A′_{1}; C = A′_{1} + A′_{2}; C = A′_{1} + A′_{2}; A_{1} + A_{2}; f; A_{1} + A_{2}; A_{2}; inr; C = A′_{1} + A′_{2}; A_{1} + A_{2}; C = A′_{1} + A′_{2}; A′_{2}; A′_{2}; A_{2}]
2.3. Notation. We denote, for every coproduct injection i: A  [figure] C, by ī: \overline{A}  [figure] C the

complementary coproduct injection, i.e., C = A + \overline{A} with injections i and ī. A subobject A [figure] B is called trivial if A is an initial object.

2.4. Remark. Let 𝒜 be an extensive category.

(i) A coproduct A + B is finitely presentable iff A and B are finitely presentable. In fact, sufficiency is trivial, for necessity assume that c_{i}: C_{i} [figure] C (i ∈ I) is a filtered colimit and f: A [figure] C a morphism. If A + B is finitely presentable, we are to verify that f factors through some c_{i}, and the factorization is essentially unique (i.e., given u, v: A [figure] C_{i} with c = c_{i}·u = c_{i}·v then u, v are merged by some connecting morphism of the filtered diagram). We know that f +id_{B}: A+B [figure] colim_{i∈I}(C_{i} +B) factors through some c_{i} + id_{B}; due to extensivity the factorizing morphism has the form u + id_{B} for some u: A [figure] C_{i}. It then follows that f = c_{i}·u, and the essential uniqueness w.r.t. A follows from that w.r.t. A + B.

(ii) An object of 𝒜 is connected iff it is non-initial and indecomposable, that is, it is not a coproduct of two objects unless one of them is initial.

(iii) In an extensive category given disjoint subobjects a_{i}: A_{i} [figure] B, i = 1, 2, each of which is a coproduct injection, then [a_{1}, a_{2}]: A_{1} + A_{2} [figure] B is also a coproduct injection. This property does not generalize to countable coproducts, see Example 2.9(3), therefore, we formulate it separately:

2.5. Definition. A category is called hyper-extensive if it has countable coproducts which are (a) disjoint, (b) universal, and (c) given pairwise disjoint subobjects a_{i}: A_{i} [figure] B, i ∈ ℕ, each of which is a coproduct injection, then [a_{i}]: ∐_{i∈ℕ} A_{i} [figure] B is also a coproduct injection.

2.6. Examples. (1) Set is hyper-extensive. The category of finite sets is an example of an extensive category that is not hyper-extensive because it does not have countable coproducts.

(2) Posets, graphs, and unary algebras form hyper-extensive categories.

(3) Free completions Fam ℬ of categories ℬ under coproducts (which can be described as the category of families of objects of ℬ) are hyper-extensive. Also free completions under countable coproducts are always hyper-extensive.

(4) If 𝒦 is hyper-extensive then so is each functor category [𝒜 , 𝒦 ], 𝒜 small.

(5) The category of compact Hausdorff spaces is extensive but not hyper-extensive: its countable coproducts are not universal.

2.7. Theorem. A locally finitely presentable category is hyper-extensive iff every object is a coproduct of connected objects.

Proof. (1) Let 𝒜 be a locally finitely presentable, hyper-extensive category.

(1a) We prove that in 𝒜 all, not necessarily finite, coproducts are universal, i.e., given a morphism f: C [figure]∐_{i∈I} A_{i}, then pullbacks c_{i}: C_{i} [figure] C of coproducts injections a_{i} along f form a coproduct C = ∐_{i∈I} C_{i}. If C is finitely presentable, then this follows from extensivity because f factors through a finite subcoproduct. If C is arbitrary, express it as a filtered colimit of finitely presentable objects D_{t} with a colimit cocone d_{t}: D_{t} [figure] C (t ∈ T). For each t form pullbacks d_{t,i}: D_{t,i} [figure] D_{t} of the coproduct injections a_{i} along f·d_{t}, then we know that D_{t} = ∐_{i∈I} D_{t,i}. Since pullbacks commute with filtered colimits, see [AR], 1.59, we have C_{i} = colim_{t∈T} D_{t,i} for every i ∈ I. Therefore, we get canonical isomorphisms

∐_{i∈I} C_{i} ≅ ∐_{i∈I} colim_{t∈T} D_{t,i}

≅ colim_{t∈T} ∐_{i∈I} D_{t,i}

≅ colim_{t∈T} D_{t}

≅ C.

(1b) Every finitely presentable object A is a coproduct of connected objects. In fact, for A initial use empty coproduct. If A ≇ 0, we use Remark 2.4(ii):

Assuming that the object A is not a finite coproduct of indecomposable objects, we derive a contradiction. There clearly exists a decomposition A = A_{0}+A_{1} where A_{0}, A_{1} are non-initial objects and A_{1} is not indecomposable. Then A_{1} has a decomposition A_{1} = A_{10} + A_{11} where A_{10}, A_{11} are non-initial and A_{11} is not indecomposable, etc. We get decompositions

A = A_{0} + A_{1} = A_{0} + A_{10} + A_{11} = A_{0} + A_{10} + A_{110} + A_{111} = ⋯

and the coproduct injections

a_{1^{n}0} : A_{1^{n}0} [figure] A = A_{0} + A_{10} + A_{110} + ⋯ + A_{1^{n}0} + A_{1^{n+1}}

are pairwise disjoint. By assumption, the morphism

a = [a_{0}, a_{10}, a_{110}, …]: ∐_{n∈ℕ}A_{1^{n}0} [figure] A

is a coproduct injection. The “complementary” coproduct injection (see 2.3)

b: B [figure] A with A = ∐_{n∈ℕ}A_{1^{n}0} + B

is disjoint with each a_{1^{n}0}. However, A is a filtered colimit of the finite coproducts A_{0} + A_{10} + ⋯ + A_{1^{n}0} + B, and since A is finitely presentable, id_{A} factors through one of the colimit morphisms c = [a_{0}, a_{10}, …, a_{1^{n}0}, b]. Thus, c is an isomorphism (being a split epimorphism and a coproduct injection). This is the desired contradiction: a_{1^{n+1}0} factors through c, in spite to being disjoint with each component.

(1c) Every object A is a coproduct of connected objects. In fact, express A as a directed colimit

a_{i}: A_{i} [figure] A (i ∈ I)

of finitely presentable objects, and let

A_{i} = ∐_{j∈J_{i}} B_{i,j} with injections b_{ij}

be a coproduct of connected objects B_{i,j}. Then since coproducts and directed colimits commute, we obtain A_{i} as a coproduct of directed colimits of the objects B_{i,j}; the latter directed colimits are connected by Remark 2.1(ii).

More detailed: for every element of

∐_{i∈I} J_{i} = {(i, j); i ∈ I, j ∈ J_{i}}

define a diagram

𝒟_{ij} indexed by all i′ ∈ I with i′ ≥ i

whose object of index i′ is the unique object B_{i′,j′} (j′ ∈ J_{i′}) for which a_{i,i′}·b_{i,j} factors through b_{i′,j′}:

[figure: A_{i}; A_{i′}; a_{i,i′}; B_{i,j}; A_{i}; b_{i,j}; B_{i,j}; B_{i′,j′}; b_{i,j}^{i′}; B_{i′,j′}; A_{i′}; b_{i′,j′}]

Let

C_{ij} = colim_{i′≥j} B_{i′,j′}

be the directed colimit of 𝒟_{ij}. By 2.1(iii), for all i, j

C_{ij} are connected objects.

We denote the colimit cocone by

c_{ij}^{i′}: B_{i′,j′}  [figure] C_{i,j}  (i′ ≥ i).

Let ∼ be the equivalence relation on ∐ J_{i} generated by

(i, j) ∼ (ī, j̄) iff 𝒟_{i,j} and 𝒟_{i′,j′} have the same object B_{i′,j′} for some upper bound i′ of i, ī.

Observe that this implies that also all objects indexed by any i′′ ≥ i′ are common. The desired coproduct is

A = ∐_{(i,j)∈S} C_{i,j}

for any set S ⊆ ∐ J_{i} of representatives of ∼. In fact, given (i, j) ∈ S the diagram 𝒟_{i,j} has a cone formed by all a_{i′}·b_{i′,j′}: B_{i′,j′} [figure] A, thus, we have a unique morphism

f_{i,j}: C_{i,j} [figure] A

such that all the squares

[figure: C_{i,j}; A; f_{i,j}; B_{i′,j′}; C_{i,j}; c_{i,j}^{i′}; B_{i′,j′}; A_{i′}; b_{i′,j′}; A_{i′}; A; a_{i′}; (i′ ≥ i)]

commute. It is easy to check that the morphism

f = [f_{i,j}]: ∐_{i,j∈S} C_{i,j} [figure] A

is an isomorphism.

(2) Let all objects of a locally finitely presentable category 𝒜 be coproducts of connected objects.

(2a) Coproduct injections a_{i}: A_{i} [figure] A_{1}+A_{2} are monomorphisms, and they are disjoint (for i = 1, 2). In fact, to prove the former, consider morphisms p, q: B [figure] A_{i} merged by a_{i} for i = 1 or 2. If B is connected, then clearly p = q. If B is arbitrary, express it as a coproduct of connected objects and use the individual coproduct injections.

Let c: C [figure] A_{1} + A_{2} be the intersection of a_{1} and a_{2}. To prove that C is the initial object, it is sufficient to observe that it is an empty coproduct (of connected objects). In fact, given a morphism b: B [figure] C then B cannot be conncted: since hom(B, A_{i}) ≠ ∅ for i = 1, 2 the coproduct A_{1} + A_{2} is not preserved by hom(B, −).

(2b) Coproducts are universal. In fact, let A = ∐_{i∈I} A_{i} be a coproduct with injections a_{i}, and let f: B [figure] A be a morphism. We first assume that B is connected. Then for the pullbacks of a_{i}’s along f there exists a unique i such that f factorizes though a_{i}, in other word, there exists a morphism d: B [figure] B_{i} with b_{i}·d = id.

[figure: B; A; f; B_{i}; B; b_{i}; B_{i}; A_{i}; f_{i}; A_{i}; A; a_{i}; B; B_{i}; d]

Since a_{i} is a monomorphism, so is b_{i}, consequently, b_{i} is an isomorphism. Thus, B is (by default) a coproduct of B_{j}’s; as B is connected: we clearly have B_{j} initial for all j ≠ i in I.

If B is not connected, apply the above argument to all connected component of B. (2c) Suppose that a_{i}: A_{i} [figure] B (i ∈ I) are pairwise disjoint coproduct injections.

Thus for every i we have a coproduct

A_{i} [figure: a_{i}] B = A_{i} + \overline{A}_{i} [figure: ā_{i}] \overline{A}_{i}.

Then we are to prove that the morphism [a_{i}]_{i∈I}: ∐_{i∈I} A_{i} [figure] B is also a coproduct injection. In fact, express B as a coproduct

B = ∐_{t∈T} B_{t} with injections b_{t}

of connected objects B_{t}. For every i ∈ I, since hom(B_{t}, −) preserves the coproduct A_{i}+\overline{A}_{i}, we see that b_{t} factorizes through either a_{i} or ā_{i}. Then A_{i} is the coproduct of all B_{t} for which b_{t} factorizes through a_{i}. Thus, for the set

T_{0} = {t ∈ T; b_{t} factorizes through a_{i} for some i ∈ I

we obviously have

∐_{i∈I} A_{i} = ∐_{t∈T_{0}} B_{t} and [a_{i}]_{i∈I} = [b_{t}]_{t∈T_{0}}.

The morphism b = [b_{t}]_{t∈T_{0}} is a coproduct injection with the complementary injection b̄ = [b_{t}]_{t∈T −T_{0}}.

2.8. Remark. It follows rather easily from the above theorem that locally finitely presentable, hyper-extensive categories have the form Fam ℬ of Example 2.6(3). In fact, they are precisely the categories of the form Fam ℬ where ℬ is finitely accessible and has connected colimits.

The proof of this fact is relatively straightforward but rather long and we omit it.

2.9. Examples. (1) All examples of 2.6(1)–(4) are locally finitely presentable.

(2) The category Vec of real vector spaces is locally finitely presentable (since it is a variety of algebras) and every vector space is a coproduct of copies of ℝ. But although ℝ is indecomposable, it is not connected. And, in fact, Vec is not extensive.

(3) The category

𝒥𝒯

of Jónsson-Tarski algebras has as objects binary algebras (A, ∗) such that ∗: A×A [figure] A is a bijection. This is a variety which is not only extensive, it is a topos, see [J], A1.2.1.11(i). However, 𝒥𝒯 is not hyper-extensive. In fact, let

Φ(1) denote the Jónsson-Tarski algebra on one generator g. There is a unique decomposition g = g′ ∗ g′′. It is easy to see that Φ(1) is also the the free Jónsson-Tarski algebra on the two generators g′ and g′′. Consequently,

Φ(1) = Φ(1) + Φ(1)

where the coproduct injections l, r: Φ(1) [figure] Φ(1) send g to g′ and g′′, respectively. This implies that Φ(1) is not a coproduct of connected objects: since Φ(1) is finitely presentable, such a coproduct would have to be finite, which is clearly impossible.

3. Equation Morphisms and Solutions

In this section we recall the concepts of algebra, equation morphism and solution for a given endofunctor

H: 𝒜 [figure] 𝒜 .

We do not require any property of 𝒜 besides having finite coproducts.

3.1. Remark. (i) Algebras an endofunctor for H are objects A of 𝒜 together with morphisms a: HA [figure] A; the corresponding morphisms are called homomorphisms, they are defined via obvious commutative squares. Coalgebras for H are objects A of 𝒜 together with morphisms a: A [figure] HA, coalgebra homomorphisms are also given by obvious commutative squares.

(ii) The functor H is called finitary if it preserves filtered colimits. Every finitary functor has free algebras, and as proved by Michael Barr in [B], this yields a monad F of free H-algebras which is a free monad on H. We have

F Z = HF Z + Z,  (1)

where the coproduct injections are the H-algebra structure and the universal arrow.

3.2. Definition. Given an endofunctor H, a flat equation morphism in an object A is a morphism of the form

e: X  [figure] HX + A.  (2)
A solution of e in an algebra a: HA  [figure] A is a morphism e^{†}: X  [figure] A such that the

square

[figure: HX + A; HA + A; He^{†}+A; X; HX + A; e; X; A; e^{†}; A; HA + A; [a,A]]

commutes. The algebra A is called completely iterative (or, shortly cia), see [M], if every flat equation morphism has a unique solution.

3.3. Examples. (i) Let H = Id be the identity endofunctor of Set. Then algebras are the usual algebras on one unary operation α. An algebra is a cia iff α has a fixed point a, and for every infinite path

⋯ [figure: α] x_{2} [figure: α] x_{1} [figure: α] x_{0}

we have x_{i} = a for all i. See [M].

(ii) Let 𝒜 be an extensive category and consider the constant functor C_{1} with the value 1, a terminal object. An algebra is an object A together with a global element a: 1 [figure] A. Every algebra is a cia. In fact, given a flat equation morphism e: X [figure] 1+A we have a decomposition

e = e_{l} + e_{r}: X_{l} + X_{r} [figure] 1 + A.

It easy to verify that the unique solution e^{†} is

e^{†} = [a·e_{l}, e_{r}]: X_{l} + X_{r} [figure] A.

(iii) If H has a terminal coalgebra τ: T [figure] HT then τ is invertible and the algebra τ^{−1} : HT [figure] T is a cia.

More generally: let T Z be the terminal coalgebra for H(−) + Z. Then the coalgebra structure

α_{Z}: T Z  [figure] HT Z + Z  (3)

is invertible, whence T Z is a coproduct of HT Z and Z

T Z = HT Z + Z  (4)

with injections

τ_{Z}: HT Z  [figure] T Z  (“T Z is an H-algebra”)
η_{Z}: Z  [figure] T Z  (“embedding of variables”).

That is, [τ_{Z}, η_{Z}] = α_{Z}^{−1}. In fact, T Z is a free cia on Z with η_{Z} as the universal arrow. We denote by T the monad of free cias for H. Its unit is η and the multiplication μ is given by the unique homomorphism μ_{Z} : T T Z [figure] T Z extending identity on T Z. This monad is characterized in [AAMV, M] as a free completely iterative monad on H.

3.4. Definition. [AAMV]. An endofunctor H is called iteratable if T Z, a terminal coalgebra for H(−) + Z, exists for every Z.

3.5. Example. (i) Let Σ be a signature, i.e., a sequence of sets (Σ_{n})_{n∈ℕ}. Then Σ-algebras in Set are H-algebras for the polynomial functor H_{Σ} : Set [figure]Set:

H_{Σ}Z = Σ_{0} + Σ_{1} × X + Σ_{2} × X^{2} + ⋯

H_{Σ} is iteratable, and T_{Σ}Z can be described as the algebra of all Σ-trees on Z, i.e., rooted and ordered trees with leaves labelled in Z + Σ_{0} and nodes with n > 0 successors labelled in Σ_{n}.

A flat equation morphism e: X [figure] H_{Σ}X + A with the set X = {x_{1}, x_{2}, … } of variables represents a system of recursive equations, one for every variable x_{i}, of the form

x_{i} ≈ s(x_{i_{1}}, …, x_{i_{n}}) for s ∈ Σ_{n}

or

x_{i} ≈ a for a ∈ A.

A solution in an algebra A is a substitution of elements x_{i}^{†} of A for variables x_{i} such that the formal equations become identities in A. It turns out that in every cia much more general recursive systems have unique solutions: the right-hand sides can be terms (or finite Σ-trees) on X + A, or even infinite Σ-trees, i.e., elements of T_{Σ}(X + A):

(ii) Every finitary endofunctor (more generally, every accessible endofunctor) of a locally finitely presentable category is iteratable, see [AAMV].

3.6. Definition. Let H be an iteratable endofunctor. An equation morphism in a cia A is a morphism of the form

e: X [figure] T (X + A).

It is called guarded if it factors through the coproduct injection of T (X + A) ≅ HT (X + A) + X + A ≅ X + [A + HT (X + A)]:

[figure: X; T (X + A); e; X; HT (X + A) + A; T (X + A); HT (X + A) + A; [τ_{X+A},η_{X+A}· inl]]

3.7. Example. For H_{Σ} an equation morphism e represents equations

x_{i} ≈ t(x_{1}, x_{2}, …, a_{1}, a_{2}, …)

whose right-hand sides are Σ-trees on X + A. And e is guarded if the right-hand sides are not single variables. This excludes trivial cases such as x_{i} ≈ x_{i} where solutions are almost never unique.

3.8. Notation. If A is a cia, we denote by ã: T A [figure] A the unique homomorphism with

ã·η_{A} = id .

The following theorem (whose proof is a straightforward adaptation of Theorem 3.9 in [M]) states that flat and guarded make no difference:

3.9. Theorem. [M]. In a cia A every guarded equation morphism e: X [figure] T (X + A) has a unique solution, i.e., there exists a unique e^{†}: X [figure] A such that the square

[figure: T (X + A); T A; T [e^{†},A]; X; T (X + A); e; X; A; e^{†}; A; T A; ã]  (5)

commutes.

3.10. Definition. Let H be a finitary endofunctor. A finitary equation morphism in A is a morphism of the form

e: X [figure] F (X + A),

where X is finitely presentable. It is called guarded if it factors through the right-hand coproduct injection of F (X + A) = X + [A + HF (X + A)].

3.11. Definition. An H-algebra is called iterative if every finitary flat equation morphism, i.e., (2) with X finitely presentable, has a unique solution.

3.12. Example. [AMV_{1}]. For H = Id_{Set} a unary algebra is iterative iff its operation α: A [figure] A has a unique fixed point x and no other cycle. It is a cia if, moreover, the graph of α^{−1} has no infinite path other than x, x, x, . . ..

3.13. Example. [N]. For H = H_{Σ} the subalgebra R_{Σ}Z ⊆ T_{Σ}Z of the Σ-tree algebra formed by all rational trees, i.e., trees which have up to isomorphism only finitely many subtrees, is iterative. This is a free iterative Σ-algebra on Z.

3.14. Remark. (i) For every finitary functor H free iterative algebras exist and the monad R they form, called the rational monad of H, is characterized in [AMV_{1}] as a free iterative monad on H. Analogously to (4) we have

R = HR + Id .  (6)

(ii) In analogy to Definition 3.6 a rational equation morphism is a morphism

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

It is called guarded if it factors through the coproduct injection of HR(X + A) + A. (iii) For every iterative algebra (A, a) we denote by

â: RA [figure] A

the unique homomorphism extending the identity on A.

3.15. Theorem. [AMV_{1}]. In an iterative algebra A every guarded rational equation morphism e: X [figure] R(X+A) has a unique solution, i.e., there exists a unique e^{†}: X [figure] A such that the square

commutes.

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

4. Preguarded Equation Morphisms

4.1. Assumption. Throughout this section H denotes an iteratable endofunctor of a hyper-extensive category, see Definitions 3.4 and 2.5. Coproduct injections of binary coproducts are called inl and inr.

4.2. Notation. Let

e: X [figure] T (X + A)

be an equation morphism and

i_{0} ≡ X [figure: inl] X + A [figure: η_{X+A}] T (X + A)

be the “standard” embedding of variables. Recall that this is a coproduct injection of T (X +A) = HT (X +A)+X +A, see (4). Let us form inverse images of the two coproduct injections, i_{0} and ī_{0} (see 2.3), along e:

[figure: X; T (X + A); i_{0}; X_{1}; X; e_{1}; X_{1}; X; i_{1}; X; T (X + A); e; T (X + A); HT (X + A) + A; ī_{0}; X; T (X + A); X; ^{\overline{X}^{1}}; ī_{1}; ^{\overline{X}^{1}}; HT (X + A) + A; ē_{1}]

Then the extensivity of our base category implies

X = X_{1} + \overline{X}_{1} with injections i_{1} and ī_{1}.

Recall that e is called guarded iff X_{1} = 0, or, equivalently,

X ≅ \overline{X}_{1} (ī_{1} an isomorphism).

4.3. Definition. Let e: X [figure] T (X+A) be an equation morphism. A subobject m: M [figure] X is called ungrounded provided that e has a restriction to an endomorphism

e′: M [figure] M,

in other words, the square

[figure: M; M; e′; M; X; m; X; T (X + A); e; M; X; m; X; T (X + A); i_{0}]  (1)

commutes. (Example: the trivial subobject 0 [figure] X is ungrounded.) We call an equation morphism e preguarded if it has no nontrivial ungrounded subobjects.

4.4. Example. Let Σ consist of a binary operation A. The system

x = y ∗ z
y = t
z = x
t = y

has the ungrounded subobject {y, t} [figure] {x, y, z, t}. Here e′ is just the domain-codomain restriction of e.

4.5. Definition. Given an equation morphism e: X [figure] T (X + A) the derived subobjects X_{n} [figure] X, n = 1, 2, 3, … are defined by the following pullbacks

[figure: X_{2}; X_{1}; i_{2}; X_{3}; X_{2}; e_{3}; X_{3}; X_{2}; i_{3}; X_{2}; X_{1}; e_{2}; X_{1}; X; i_{1}; X_{2}; X_{1}; X_{2}; X_{1}; i_{2}; X_{1}; X; e_{1}; X; T (X + A); i_{0}; X_{1}; X; X_{1}; X; i_{1}; X; T (X + A); e; X_{3}; X_{2}; …]  (2)

4.6. Remark. (i) Since i_{0} is a coproduct injection, so is i_{1}, and e_{1} is a domain-codomain restriction of e. Analogously, since i_{1} is a coproduct injection, so is i_{2}, and e_{2} is a domaincodomain restriction of e_{1}, etc. We denote by i_{n}^{∗}: X_{n} [figure] X the corresponding composites

i_{0}^{∗} = id_{X}  and i_{n+1}^{∗} = i_{n}^{∗}·i_{n+1} : X_{n+1}  [figure] X.  (3)

(ii) For every n ≥ 1 we denote by

ī_{n}: \overline{X}_{n} [figure] X_{n−1} (n = 1, 2, 3, …)

(where X_{0} = X) the complementary coproduct injection of i_{n}, thus, X_{n−1} = X_{n} + \overline{X}_{n} for n = 1, 2, 3, … We consider \overline{X}_{n} as a subobject of X via

ī_{n}^{∗} ≡ \overline{X}_{n} [figure: ī_{n}] X_{n−1} [figure: i_{n−1}^{∗}] X  (n ≥ 1).  (4)

(iii) In the base category Set the variables of X_{1} = e^{−1}(X_{0}) are precisely those x_{i} where t_{i} is a single variable in X. That is, those x_{i} where the corresponding equation has the form x_{i} ≈ x_{i′}. We conclude that X_{1} are precisely the unguarded variables. To put it positively, \overline{X}_{1} consists of all the guarded variables. Here we have e_{1} : X_{1} [figure] X, x_{i} [figure] x_{i′}, and thus x_{i} lies in X_{2} = e_{1}^{−1}(X_{1}) if and only if x_{i′} is unguarded. Consequently, for every x_{i} ∈ X_{2} we have equations x_{i} ≈ x_{i′} and x_{i′} ≈ x_{i′′}. In other words, \overline{X}_{2} consists of all variables reaching a guarded variable in one step (of applying e). Analogously, x_{i} ∈ X_{3} if and only if we have equations x_{i} ≈ x_{i′}, x_{i′} ≈ x_{i′′} and x_{i′′} ≈ x_{i′′′} or, equivalently, \overline{X}_{3} consists of all variables reaching a guarded variable in two steps, etc. To say

X = \overline{X}_{1} + \overline{X}_{2} + \overline{X}_{3} + ⋯

means that every variable reaches a guarded variable in finitely many steps. More generally:

4.7. Proposition. Every equation morphism has the greatest ungrounded subobject which is (a) the intersection of all derived subobjects and (b) the complementary subobject of ∐_{n≥1} \overline{X}_{n}.

Proof. Since ī_{k}^{∗}: \overline{X}_{k} [figure] X (k ≥ 1) are pairwise disjoint coproduct injections, they form a coproduct injection [ī_{k}^{∗}]: ∐_{k≥1} \overline{X}_{k} [figure] X, see 2.5. We denote by

m: M [figure] X

the complementary coproduct injection and prove that this is the largest ungrounded subobject of e—this proves the proposition since X = X_{k} + \overline{X}_{k} for every k ≥ 1, implies that the subobject m: M [figure] X is just the intersection of all derived subobjects.

(a) m: M [figure] X is ungrounded. In fact, denote by

m_{k}: M  [figure] X_{k}  with i_{k}^{∗}·m_{k} = m

the corresponding embeddings. Then the morphisms e′_{k} = e_{k+1}·m_{k+1} : M [figure] X_{k} form a compatible cone, i.e., i_{k}·e′_{k} = e′_{k−1} for k = 1, 2, 3, . . .. Thus, there exists a unique

e′: M [figure] M (= ⋂_{k≥1} X_{k}) with e′_{k} = m_{k}·e′ (k ≥ 1).

The diagram (1) commutes since for m = i_{1}·m_{1} we get

e·m = e·i_{1}·m_{1} = i_{0}·e_{1}·m_{1} = i_{0}·e′_{0}

as well as

i_{0}·m·e′ = i_{0}·i_{1}·m_{1}·e′ = i_{0}·i_{1}·e′_{1} = i_{0}·e′_{0}.

(b) Let m̂: M̂ [figure] X be an ungrounded subobject with

e·m̂ = i_{0}·m·ê for ê: M̂ [figure] M̂.

To prove M̂ ⊆ M we need to show M̂ ⊆ X_{k} for all k ≥ 1: this is an obvious induction on k using the pullbacks of (2).

4.8. Corollary. An equation morphism e: X [figure] T (X + A) is preguarded iff X = ∐_{n≥1} \overline{X}_{n}.

4.9. Remark. (i) Even if our base category is not hyper-extensive, every ungrounded subobject m: M [figure] X factorizes through the intersection of all derived subobjects: use the morphisms e′_{k} in the proof of Proposition 4.7.

(ii) From Example 3.5 we see that the intuition behind the subobjects \overline{X}_{1}, \overline{X}_{2}, \overline{X}_{3}, … is such that \overline{X}_{1} consists of all guarded variables. If e is a guarded equation morphism, then X = \overline{X}_{1}. If e is preguarded, we always have a passage \overline{X}_{n} [figure] \overline{X}_{1}, for all n ≥ 1, which to every variable assigns the guarded variable eventually reached by applying e finitely many times. To formulate this categorically, we need the following 4.10. Notation. We form a pullback of e_{n}: X_{n} [figure] X_{n−1} along the complement ī_{n} of i_{n}, see Remark 4.6:

[figure: _{\overline{X}_{n}}; X_{n−1}; ī_{n}; ^{\overline{X}^{n+1}}; _{\overline{X}_{n}}; ē_{n+1}; ^{\overline{X}^{n+1}}; X_{n}; ī_{n+1}; X_{n}; X_{n−1}; e_{n}; X_{n−1}; X_{n}; i_{n}; X_{n}; X_{n−1}; X_{n}; X_{n+1}; i_{n+1}; X_{n+1}; X_{n}; e_{n+1}  (n ≥ 1)]

The canonical passage from \overline{X}_{n} to \overline{X}_{1} is the composite ē_{2}· · · · ·ē_{n}. This defines a morphism

u = [id, ē_{2}, ē_{2}·ē_{3}, …]: \overline{X}_{1} + \overline{X}_{2} + \overline{X}_{3} + ⋯  [figure] \overline{X}_{1}.  (5)

4.11. Definition. For every preguarded equation morphism e: X [figure] T (X+A) we define an equation morphism as follows

f ≡ \overline{X}_{1} [figure: ī_{1}] X [figure: e] T (X + A) [figure: T (u+A)] T (\overline{X}_{1} + A).  (6)

We call f the guarded modification of e.

4.12. Theorem. The guarded modification f of an equation morphism e is guarded, and has the same solutions as e. More precisely: for every cia with the underlying object A:

(a) If e^{†} is a solution of e, then e^{†}·ī_{1} : \overline{X}_{1} [figure] A is a solution of f.

(b) If f^{†} is a solution of f, then f^{†}·u: X [figure] A is a solution of e.

[figure: X; A; e^{†}; ^{\overline{X}^{1}}; A; f^{†}; u; ī_{1}]

Proof. (1) We verify that f is guarded. Put

j_{0} = inl: \overline{X}_{1} [figure] T (\overline{X}_{1} + A) = \overline{X}_{1} + A + HT (\overline{X}_{1} + A)

and compute a pullback of f along j_{0}:

[figure: _{\overline{X}_{1}}; T (\overline{X}_{1} + A); j_{0}=inl; X; _{\overline{X}_{1}}; u; X; T (X + A); i_{0}=inl; T (X + A); T (\overline{X}_{1} + A); T (u+A)=u+[A+HT (u+A)]; X; T (X + A); X_{1}; X; e_{1}; X_{1}; X; i_{1}; X; T (X + A); e; X_{1}; X; 0; X_{1}; 0; ^{\overline{X}^{1}}; ^{\overline{X}^{1}}; X; ī_{1}]

(2) Proof of (b). Given a solution f^{†}: \overline{X}_{1}  [figure] A of f, we prove that f^{†}·u: X  [figure] A

is a solution of e, i.e., f^{†}·u = ã·T [f^{†}·u, A]·e: X [figure] A. This equation will be proved by considering the individual components of X = ∐ \overline{X}_{n}, see (4). For n = 1 we use the definition (6) of f and obtain the commutative diagram

[figure: T (X + A); T (\overline{X}_{1} + A); T (u+A); X; T (X + A); e; X; ^{\overline{X}^{1}}; u; ^{\overline{X}^{1}}; T (\overline{X}_{1} + A); f; T (\overline{X}_{1} + A); T A; T [f^{†},A]; ^{\overline{X}^{1}}; T (\overline{X}_{1} + A); ^{\overline{X}^{1}}; A; f^{†}; A; T A; ã; ^{\overline{X}^{1}}; X; ī_{1}; ^{\overline{X}^{1}}; ^{\overline{X}^{1}}]

For n = 2, the coproduct injection is i_{1}·ī_{2} : \overline{X}_{2} [figure] X; thus we consider the diagram

[figure: T (X + A); T (\overline{X}_{1} + A); T (u+A); X; T (X + A); e; X; ^{\overline{X}^{1}}; u; ^{\overline{X}^{1}}; T (\overline{X}_{1} + A); f; ^{\overline{X}^{2}}; ^{\overline{X}^{1}}; ē_{2}; ^{\overline{X}^{2}}; X_{1}; ī_{2}; X_{1}; X; i_{1}; X_{1}; X; e_{1}; ^{\overline{X}^{2}}; ^{\overline{X}^{1}}; ē_{2}; ^{\overline{X}^{1}}; ^{\overline{X}^{1}}; ^{\overline{X}^{1}}; ^{\overline{X}^{1}}; ^{\overline{X}^{1}}; X; ī_{1}; X; T (X + A); inl; ^{\overline{X}^{1}}; T (\overline{X}_{1} + A); inl; X; ^{\overline{X}^{1}}; u; T (\overline{X}_{1} + A); T A; T [f^{†},A]; ^{\overline{X}^{1}}; T (\overline{X}_{1} + A); ^{\overline{X}^{1}}; A; f^{†}; A; T A; ã; (∗)]

All the inner parts except the one denoted by (∗) clearly commute. The part (∗) commutes when composed with the passage to A, ã·T [f^{†}, A]: T (\overline{X}_{1} + A) [figure] A, i.e., this morphism merges the parallel pair f, inl: \overline{X}_{1} [figure] T (\overline{X}_{1} + A). In fact, by the commutativity of the right-hand square in the above diagram it suffices to observe that f^{†} = ã·T [f^{†}, A]· inl:

[figure: T (\overline{X}_{1} + A); T A; T [f^{†},A]; ^{\overline{X}^{1}}; T (\overline{X}_{1} + A); inl; ^{\overline{X}^{1}}; A; f^{†}; A; T A; η_{A}; T A; A; ã; A; A]

The cases n = 3, 4, … are analogous to the case n = 2.

(3) Proof of (a). Let e^{†}: X [figure] A be a solution of e. We are to prove that the outward square of the following diagram

[figure: ^{\overline{X}^{1}}; T (\overline{X}_{1} + A); f; ^{\overline{X}^{1}}; X; ī_{1}; X; T (X + A); e; T (X + A); T (X + A); T (X + A); T (\overline{X}_{1} + A); T (u+A); T (\overline{X}_{1} + A); T (X + A); T (ī_{1}+A); T (\overline{X}_{1} + A); T A; T [e^{†}·ī_{1},A]; X; A; e^{†}; T A; A; ã; T (X + A); T A; T [e^{†},A]; T (X + A); T A; T [e^{†},A]; (∗)]

commutes. All the inner parts except that denoted by (∗) commute. For (∗) it is sufficient to prove that T [e^{†}, A] merges id and T (ī_{1}+A)·T (u+A). Therefore, the proof of (a) will be finished by proving the equation e^{†} = e^{†}·ī·u. We consider the individual components \overline{X}_{n} of X = \overline{X}_{1} + \overline{X}_{2} + \overline{X}_{3} + ⋯, see (4):

For n = 1 use u·ī_{1} = id to obtain e^{†}·ī_{1} = (e^{†}·ī_{1}·u)·ī_{1}.

For n = 2 we are to prove the equation e^{†}·i_{1}·ī_{2} = (e^{†}·ī_{1}·u)·i_{1}·ī_{2}. Consider the diagram

[figure: ^{\overline{X}^{2}}; X_{1}; ī_{2}; X_{1}; X; i_{1}; X; _{\overline{X}_{1}}; u; _{\overline{X}_{1}}; X; ī_{1}; X; A; e^{†}; ^{\overline{X}^{2}}; X_{1}; ī_{2}; ^{\overline{X}^{2}}; _{\overline{X}_{1}}; ē_{2}; X_{1}; X; e_{1}]

from which the right-hand side of the desired equation is expressed as e^{†}·e_{1}·ī_{2}. It remains to verify e^{†}·i_{1} = e^{†}·e_{1} which follows from the next diagram

[figure: X_{1}; X; i_{1}; X_{1}; X; e_{1}; T (X + A); T A; T [e^{†},A]; X; T (X + A); e; X; A; e^{†}; A; T A; ã; X; T (X + A); i_{0}; X; X + A; inl; X; A; e^{†}; X + A; T (X + A); η; X + A; A; [e^{†},A]; A; T A; η; A; A]

Cases n = 3, 4, … are analogous.

4.13. Remark. Within the proof of Theorem 4.12 we proved that if e^{†} is a solution of the preguarded equation morphism e: X [figure] T (X + A), then

e^{†} = e^{†}·ī·u.  (7)

4.14. Corollary. In every cia all preguarded equation morphisms have unique solutions.

In fact, the morphism u is an epimorphism, due to u·ī_{1} = id, thus the unique existence of e^{†} follows from the unique existence of f^{†} via (a) and (b) above.

4.15. Remark. How about the converse: if e: X [figure] T (X + A) has unique solutions in all cia’s, is e preguarded? The answer is affirmative whenever T satisfies mild side conditions: see Proposition 5.12 below.

5. Strict Solutions

5.1. Assumption. Throughout this section 𝒜 denotes a hyper-extensive category with a terminal object, 1. Moreover, H denotes an iteratable endofunctor of 𝒜, see Definition 3.4, for which a morphism

⊥: 1 [figure] H0

has been chosen.

5.2. Notation. For every equation morphism the intersection of the derived subobjects i_{n}^{∗}: X_{n} [figure] X (see (3)) is denoted by

i_{∞}: X_{∞} [figure] X.

5.3. Remark. By Proposition 4.7 the intersection exists and we have X = X_{∞}+∐_{n≥1} \overline{X}_{n} (with i_{∞} and (4) as injections) and X_{∞} is greatest ungrounded subobject.

5.4. Notation. ⊥ is a global constant of H, i.e., every H-algebra HA [figure: a] A obtains the corresponding global element

⊥_{A} ≡ 1 [figure: ⊥] H0 [figure: H!] HA [figure: a] A.

All homomorphisms h: A [figure] B preserve this global constant: h·⊥_{A} = ⊥_{B}. In fact, consider the commutative diagram below:

[figure: 1; H0; ⊥; H0; HA; H!; H0; HB; H!; HA; HB; HB; B; β; HA; HB; Hh; HA; A; a; A; B; h]

In particular for every object Y we have a global element of T Y see Example 3.3(iii) which we denote by ⊥ for short:

⊥ ≡ 1 [figure] H0 [figure: H!] HT Y [figure: τ_{Y}] T Y

5.5. Definition. Let A be a cia and e: X [figure] T (X + A) an equation morphism with a solution e^{†}: X [figure] A (see (5)). We call e^{†} strict if its restriction to every ungrounded subobject m: M [figure] X (see 4.3) is ⊥_{A}. Equivalently, the square below commutes:

[figure: X; A; e^{†}; X_{∞}; X; i_{∞}; X_{∞}; 1; 1; A; ⊥_{A}]  (1)

5.6. Definition. Let A be a cia. For every equation morphism

e: X [figure] T (X + A)

we define an equation morphism

f: X [figure] T (X + A)

by changing the left-hand component of e: X_{∞} + ∐ \overline{X}_{n} [figure] T (X + A) to ⊥:

f·i_{∞} ≡ X_{∞} [figure: !] 1 [figure: ⊥] T (X + A)
f·ī_{∞} = e·ī_{∞}: ∐_{n≥1} \overline{X}_{n}  [figure] T (X + A).

We call f the preguarded modification of e.

5.7. Theorem. The preguarded modification f of an equation morphism e is preguarded and has the same strict solutions. That is:

(a) every strict solution of e is a solution of f, and

(b) every solution of f is a strict solution of e.

Proof. (1) f is preguarded. Let Z_{0} = ∐ \overline{X}_{n} and let j_{k}: Z_{k} [figure] Z_{k−1}, k ≥ 1, denote the derived subobjects of f; we have j_{0} = ī_{∞}. We will prove that

Z_{k} = \overline{X}_{k+1} + \overline{X}_{k+2} + ⋯ and j_{k} = inr: Z_{k} [figure] \overline{X}_{k} + Z_{k},

and that the corresponding morphism opposite f_{k−1} is

f_{k} = ē_{k+1} + ē_{k+2} + ⋯: Z_{k} [figure] Z_{k−1} (k ≥ 1).

This proves obviously that f is preguarded since ⋂_{k∈ℕ} Z_{k} = 0.

Case k = 1: To find a pullback of f = [⊥!, e·j_{0}] along i_{0} : X [figure] T (X + A), we just compute a pullback of e·j_{0} along i_{0}: in fact the component ⊥! contributes nothing to the pullback because it factors through ī_{0}, the complement of i_{0}, and 𝒜 is extensive. Here is the pullback of e·j_{0} along i_{0}:

[figure: X; T (X + A); i_{0}; X_{∞} + \overline{X}_{2} + \overline{X}_{3} + ⋯ = X_{1}; X; e_{1}; X_{∞} + \overline{X}_{2} + \overline{X}_{3} + ⋯ = X_{1}; X = X_{∞} + \overline{X}_{1} + \overline{X}_{2} + \overline{X}_{3} + ⋯; i_{1}=inr; X = X_{∞} + \overline{X}_{1} + \overline{X}_{2} + \overline{X}_{3} + ⋯; T (X + A); e; X_{1}; X; \overline{X}_{2} + \overline{X}_{3} + ⋯ = Z_{1}; X_{1}; inr; \overline{X}_{2} + \overline{X}_{3} + ⋯ = Z_{1}; ^{\overline{X}^{1} + \overline{X}_{2} + \overline{X}_{3} + ⋯}; inr; ^{\overline{X}^{1} + \overline{X}_{2} + \overline{X}_{3} + ⋯}; X; j_{0}=inr]

Consequently, we have Z_{1} = \overline{X}_{2} + \overline{X}_{3} + ⋯ with j_{1} = inr: Z_{1} [figure] X = X_{∞} + \overline{X}_{1} + Z_{1}, and the corresponding morphism f_{1} : Z_{1} [figure] X is

f_{1} ≡ Z_{1} [figure: inr] X_{∞} + Z_{1} [figure: e_{1}] X.

Case k = 2: We compute a pullback of f_{1} = e_{1}· inr along j_{1}:

[figure: ∐_{n≥2} \overline{X}_{n} = Z_{1}; X; j_{1}; ^{∐_{n≥2} \overline{X}^{n+1}}; ∐_{n≥2} \overline{X}_{n} = Z_{1}; ^{∐_{n≥2} \overline{X}^{n+1}}; X_{1}; X_{1}; X; e_{1}; ^{∐_{n≥2} \overline{X}^{n+1}}; X_{1}; Z_{2}; ^{∐_{n≥2} \overline{X}^{n+1}}; Z_{2}; Z_{1}; Z_{1}; X_{1}; inr]

by computing first a pullback P_{n} of e_{1} along the n-th component \overline{X}_{n} [figure] X, n ≥ 2, of j_{1}, see (4)

[figure: _{\overline{X}_{n}}; X_{n−1}; ī_{n}; ^{P_{n} = \overline{X}^{n+1}}; _{\overline{X}_{n}}; ē_{n+1}; ^{P_{n} = \overline{X}^{n+1}}; X_{n}; ī_{n+1}; X_{n}; X_{n−1}; e_{n}; X_{n}; ⋯; i_{n}; X_{n−1}; ⋯; i_{n−1}; ⋯; X_{2}; i_{3}; ⋯; X_{1}; i_{2}; X_{1}; X; i_{1}; X_{2}; X_{1}; e_{2}; X_{2}; X_{1}; i_{2}; X_{1}; X; e_{1}]
The connecting maps are ē_{n}: P_{n}  [figure] \overline{X}_{n} and i_{2}· · · · ·i_{n}·ī_{n+1} : P_{n}  [figure] X_{1}. Thus, due

to extensivity, a pullback of e_{1} along j_{1} is ∐_{n≥2} \overline{X}_{n+1} = Z_{2} with the connecting maps ∐_{n≥2} ē_{n+1} : Z_{2} [figure] Z_{1} and inr: Z_{2} [figure] X_{1} = X_{∞} + \overline{X}_{2} + Z_{2}. The pullback of f_{1} = e_{1}· inr along j_{1} is thus

[figure: \overline{X}_{3} + \overline{X}_{4} + \overline{X}_{5} + ⋯ = Z_{2}; X_{1} = X_{∞} + \overline{X}_{2} + \overline{X}_{3} + \overline{X}_{4} + ⋯; \overline{X}_{3} + \overline{X}_{4} + \overline{X}_{5} + ⋯ = Z_{2}; \overline{X}_{3} + \overline{X}_{4} + \overline{X}_{5} + ⋯ = Z_{2}; \overline{X}_{3} + \overline{X}_{4} + \overline{X}_{5} + ⋯ = Z_{2}; Z_{1} = \overline{X}_{2} + \overline{X}_{3} + \overline{X}_{4} + ⋯; inr; Z_{1} = \overline{X}_{2} + \overline{X}_{3} + \overline{X}_{4} + ⋯; X_{1} = X_{∞} + \overline{X}_{2} + \overline{X}_{3} + \overline{X}_{4} + ⋯; inr; Z_{1}; X; j_{1}; Z_{2}; Z_{1}; ^{∐_{n≥2} ē_{n+1}}; Z_{2}; X_{1}; inr; X_{1}; X; e_{1}]

We obtain Z_{2} = \overline{X}_{3} + \overline{X}_{4} + \overline{X}_{5} + ⋯, j_{2} = inr, and f_{2} = ∐_{n≥2} ē_{n+1}.

Case k ≥ 3: Here we use the obvious pullbacks

[figure: ⋯ Z_{3}; Z_{2}; ⋯ Z_{4}; ⋯ Z_{3}; ^{∐_{n≥4} ē_{n+1}}; ⋯ Z_{4}; Z_{3}; Z_{3}; Z_{2}; ^{∐_{n≥3} ē_{n+1}}; Z_{2}; Z_{1}; inr; Z_{3}; Z_{2}; Z_{3}; Z_{2}; inr; Z_{2}; Z_{1}; ^{∐_{n≥2} ē_{n+1}}]

(2) Proof of (b). If f^{†} is a solution of f, then f^{†} is strict. Observe first that the diagram below commutes:

[figure: T (X + A); T A; T [f^{†},A]; X; T (X + A); f; X; A; f^{†}; A; T A; ã; ⋂ X_{n}; X; i_{∞}; ⋂ X_{n}; 1; !; 1; T (X + A); ⊥; 1; H0; ⊥; H0; HT (X + A); H!; HT (X + A); T (X + A); τ; HT (X + A); HT A; HT [f^{†},A]; HT A; T A; τ; HT A; HA; Hã; HA; A; a]

We see that the passage from H0 to HA is H! (because ã·T [f^{†}, A]·! = !: 0 [figure] A), thus f^{†}·i_{∞} = a·H!·⊥·! = ⊥_{A}·! as required.

And f^{†} is a solution of e, i.e., the equation

ã·T [f^{†}, A]·e = f^{†}: X_{∞} + ∐_{n≥1} \overline{X}_{n}  [figure] A  (2)

holds (see (5) in the introduction). In fact for the right-hand component j_{0} : ∐ \overline{X}_{n} [figure] X this follows from e·j_{0} = f·j_{0}. For the left-hand component use the commutative diagram

[figure: X; T (X + A); e; X_{∞}; X; i_{∞}; X_{∞}; X_{∞}; e′; X_{∞}; X; i_{∞}; X; T (X + A); i_{0}; X_{∞}; 1; !; X; A; f^{†}; 1; A; ⊥_{A}; X; A; f^{†}; T (X + A); T A; T [f^{†},A]; 1; A; ⊥_{A}; A; A; A; A; T A; η_{A}; T A; A; ã; X_{∞}; 1; !; 1; 1; 1; A; ⊥_{A}]

whose left-hand square commutes for some e′ by 5.3.

(3) Proof of (a). If e^{†} is a strict solution of e, then we are to prove that the equation ã·T [e^{†}, A]·f = e^{†} holds (cf. (5)): for the right-hand component with domain ∐ \overline{X}_{n} this follows from the fact that f·j_{0} = e·j_{0}. For the left-hand component use the fact that both e^{†} and f yield ⊥ (in A and T (X +A), respectively) and that ã·T [e^{†}, A] preserves ⊥, being a homomorphism (see Notation 5.4).

5.8. Notation. For every equation morphism e: X [figure] T (X + A) we denote by

⟨e⟩: \overline{X}_{1} [figure] T (\overline{X}_{1} + A)

the guarded modification of the preguarded modification of e.

5.9. Corollary. In every cia every equation morphism has a unique strict solution, viz., the unique solution of the guarded morphism ⟨e⟩.

5.10. Remark. We will now turn our attention to the question of whether an equation having a unique solution in every cia must be preguarded. In the case of 𝒜 = Set, the answer is affirmative whenever H1 has at least two elements. In general categories we need the following

5.11. Definition. We say that the free completely iterative cia monad T is nontrivial if it preserves monomorphisms and has at least two global constants:

card 𝒜 (1, T 0) ≥ 2.

5.12. Proposition. Suppose that morphisms from non-initial objects to 1 are epimorphisms. If the free cia monad is nontrivial, then every equation morphism e: X [figure] T (X+ A) with a unique solution in T A is preguarded.

5.13. Remark. We consider e as an equation in T A via X [figure: e] T (X +A) [figure: T (X+η)] T (X + T A).

Proof. Suppose that e is not preguarded. For every global element b: 1 [figure] T 0 we can find a solution e_{b}^{†}: X [figure] T A such that

e_{b}^{†}·i_{∞} ≡ X_{∞} [figure] 1 [figure: b] T 0 [figure: T!] T A.

The proof is precisely the proof of Theorem 5.7 where a: HA [figure] A is the replaced by τ_{A}: HT A [figure] T A (with τ̃_{A} = μ_{A}) and ⊥ is replaced by b. We will prove that e has more than one solution by showing that e_{b}^{†} determines b; for that we just observe that T!: T 0 [figure] T A is a monomorphism. In fact, !: 0 [figure] A is a monomorphism since in every extensive category initial objects are strict, and T preserves monomorphisms.

5.14. Example. Suppose that our base category is 𝒜 = Set.

(1) Whenever H1 has more than one element then H has a nontrivial free completely iterative cia monad. In fact, T preserves monomorphisms by Proposition 6.1 in [AMV_{1}]. And to prove card T 0 ≥ 2, we decompose H = H′ + H′′ with H′1 ≠ ∅ and H′′1 ≠ ∅. This can be done by choosing any a ∈ H1 and defining H′X and H′′X as the inverse images of {a} and H1 − {a}, respectively, under H!: HX [figure] H1. Consider the coalgebras

A ≡ 1 [figure: const a] H′1 [figure] H1 and B ≡ 1 [figure: const b] H′′1 [figure] H1

(a ∈ H′1, b ∈ H′′1), and recall that T 0 is the final coalgebra for H. It is clear that the unique homomorphism A [figure] T 0 is disjoint with the unique homomorphism B [figure] T 0. Therefore, card T 0 ≥ 2.

(2) Conversely, whenever for every equation morphism e the implication

e has unique solution ⟹ e is preguarded

holds, then H1 must have more than one element. In fact, card H1 = 1 implies that T 0 has a unique element. Then the equation x ≈ x has a unique solution in T 0.

5.15. Remark. The previous results of the present section only hold for a functor with a chosen morphism 1 [figure] H0. The last assumption can be dropped: we now work with an arbitrary iteratable endofunctor H. And we apply the previous results to the endofunctor

H′ = H(−) + 1 with injections γ: H  [figure] H′, ⊥: 1  [figure] H′.

5.16. Definition. By a strict H-algebra is meant an H-algebra α: HA [figure] A together with a morphism ⊥_{A}: 1 [figure] A. Let (A, α) be a cia. Given an equation morphism e: X [figure] T (X + A), a strict solution is a solution e^{†}: X [figure] A (i.e., (5) commutes) such that its restriction to every ungrounded subobject is ⊥_{A} (i.e., (1) commutes).

5.17. Theorem. Let H be an iteratable endofunctor. In every strict cia every equation morphism has a unique strict solution.

Proof. (1) Since H is iteratable (i.e., H(−) + X has a terminal coalgebra for every X), it follows that H′ is iteratable—in fact, substitute X + 1 for X. Let T′ denote the free completely iterative monad of H′.

(2) If α: HA [figure] A is a cia, then for every ⊥_{A}: 1 [figure] A the corresponding H′-algebra [α, ⊥_{A}]: HA+1 [figure] A is a cia. In fact, given a flat equation morphism e: X [figure] HX+1+A denote

f ≡ X [figure: e] HX + 1 + A [figure: HX+[⊥_{A},id]] HX + A;

we prove that a morphism f^{†}: X [figure] A is a strict solution of e w.r.t. H (see 5.16) iff f^{†} is a strict solution of f w.r.t H′ (see 5.5). This follows from the commutative diagram

[figure: HX + 1 + A; HA + 1 + A; Hf^{†}+1+A; X; HX + 1 + A; e; X; A; f^{†}; A; HA + 1 + A; [α,⊥_{A},id]; HX + A; HA + A; Hf^{†}+id; HX + 1 + A; HX + A; HX+[⊥_{A},id]; HX + 1 + A; HA + 1 + A; HA + 1 + A; HA + A; HA+[⊥_{A},id]; HA + A; A; [α,id]; X; HX + A; f; (∗)]

More detailed: if f^{†} is a solution of f, then the outward part commutes, and since all inner parts without denotation commute, it follows that (∗) commutes. Thus, f^{†} is a solution of e. Conversely, if f^{†} is a solution of e, then (∗) commutes—thus the diagram above commutes, proving that f^{†} is a solution of f.

(3) Let us recall the notation (3)

α_{Z}: T Z [figure] HT Z + Z

of the structure of a terminal coalgebra for H(−) + Z, and let us use the analogous notation for H′:

α′_{Z}: T′Z [figure] HT′Z + 1 + Z.

We obtain a natural transformation

δ: T [figure] T′

whose components are the unique coalgebra homomorphisms δ_{Z} for H′(−) + Z:

[figure: T Z; HT Z + Z; α_{Z}; HT Z + Z; HT Z + 1 + Z; T Z; T′Z; δ_{Z}; T′Z; HT′Z + 1 + Z; α′_{Z}; HT Z + 1 + Z; HT′Z + 1 + Z; Hδ_{Z}+id]

For every strict cia A we have the homomorphism

α̃: T A [figure] A with α̃·η_{A} = id

of Notation 3.8, as well as the corresponding homomorphism, say,

ᾱ: T′A [figure] A with ᾱ·η′_{A} = id.

The uniqueness makes it clear that the triangle

[figure: T A; A; α̃; T A; T′A; δ_{A}; A; T′A; ᾱ]

commutes.

(4) To prove the theorem, let A be a strict cia (for H) and let e: X [figure] T (X + A) be an equation morphism. For the equation morphism

g ≡ X [figure: e] T (X + A) [figure: δ_{X+A}] T′(X + A)

there is, due to Corollary 5.9, a unique strict solution g^{†}: X [figure] A in the sense of Definition 5.5. We show that g^{†} is the unique strict solution of e in the sense of Definition 5.16. It is not difficult to prove that the largest ungrounded subobject of g and e coincide. Thus, the two notions of strictness (according to Definition 5.5 and 5.16, respectively) coincide. Finally, the diagram below shows that solutions of g and e coincide:

[figure: T (X + A); T A; T [g^{†},id]; X; T (X + A); e; X; A; g^{†}; A; T A; α̃; T (X + A); T′(X + A); δ_{X+A}; T′(X + A); T′A; T′[g^{†},id]; T A; T′A; δ_{A}; T′A; A; ᾱ]

5.18. Remark. Theorem 5.17 extends from objects to morphisms in the following natural

sense. Given cias α: HA  [figure] A and β: HB  [figure] B, every homomorphism of H-algebras

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

preserves solutions of the flat equation morphisms, and conversely, every solution-pre-serving morphism is a homomorphism of H-algebras, as proved in [AMV_{1}]. Preservation of solutions means that given a flat equation morphism e: X [figure] HX + A and forming the corresponding equation morphism

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

then the triangle

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

commutes.

Now assume that A and B are strict cias, and f is a strict homomorphism, i.e., a homomorphism preserving the chosen global elements (h·⊥_{A} = ⊥_{B}). It follows that h preserves strict solutions of non-flat equation morphisms, too. That is, given an equation morphism

e: X [figure] T (X + A)

and forming

h • e ≡ X [figure: e] T (X + A) [figure: T (id +h)] T (X + B)
then the following holds: the unique strict solutions e^{†}: X  [figure] A and (h • e)^{†}: X  [figure] B

form a commutative triangle (3). This follows from the commutative diagram

[figure: T (X + A); T A; T [h·e^{†},η]; X; T (X + A); e; X; A; e^{†}; A; T A; α̃; T (X + A); T (X + B); T (id +h); A; B; h; T (X + B); T B; T [h·e^{†},η]; T B; B; β̃; T A; T B; T h]

and the fact that the largest ungrounded subobjects of e and h • e coincide.

6. Iterative Algebras

6.1. Assumption. In this section 𝒜 is a hyper-extensive locally finitely presentable category and H is a finitary endofunctor for which a morphism

⊥: 1 [figure] H0

has been chosen. (Or, alternatively, we work with pointed algebras, see Section 4.)

6.2. Definition. For a rational equation morphism e: X [figure] R(X + A) (see Remark 3.14 (ii)), we define derived subobjects X_{n} [figure] X precisely as in Definition 4.5, just replacing T by R everywhere.

6.3. Remark. We thus have pullbacks

[figure: X_{2}; X_{1}; i_{2}; X_{3}; X_{2}; e_{3}; X_{3}; X_{2}; i_{3}; X_{2}; X_{1}; e_{2}; X_{1}; X; i_{1}; X_{2}; X_{1}; X_{2}; X_{1}; i_{2}; X_{1}; X; e_{1}; X; R(X + A); i_{0}=inr; X_{1}; X; X_{1}; X; i_{1}; X; R(X + A); e; X_{3}; X_{2}; …]
We also use the remaining notation ī_{n}: \overline{X}_{n}  [figure] X_{n−1} and ē_{n}: \overline{X}_{n}  [figure] X_{n−1} etc. as in

Section 3.

6.4. Lemma. Every rational equation morphism e has the greatest ungrounded subobject equal to the least derived subobject: there exists n such that i_{n} is an isomorphism, and then i_{n}^{∗}: X_{n} [figure] X, see (3) is the greatest ungrounded subobject.

Proof. Let e: X [figure] R(X +A) be a rational equation morphism. By assumption, X is a coproduct of k indecomposable objects, X = Y_{1} + ⋯ + Y_{k}. For every coproduct injection z: Z [figure] X we obtain the corresponding morphisms z_{i}: Z_{i} [figure] Y_{i} with Z = Z_{1} + ⋯ + Z_{k} and z = z_{1} +⋯+z_{k}. Since each z_{i} is a coproduct injection of Y_{i}, either Z_{i} = 0 or Z_{i} = Y_{i}. Consequently, there are (in case Y_{i} ≇ 0 for every i) precisely 2^{k} subjects of X which are coproduct injections. Since the subobjects \overline{X}_{n} [figure] X, n ∈ ℕ, are pairwise disjoint, it follows that there exists an m ∈ ℕ such that \overline{X}_{m} ≅ 0. Thus X_{m} ≅ X_{m+1} +\overline{X}_{m+1} ≅ X_{m+1}. The proof that the intersection of derived subobjects is the greatest ungrounded subobject is as in Proposition 4.7.

6.5. Definition. A rational equation morphism e is called preguarded provided that it has no nontrivial ungrounded subobject, i.e., X_{n} ≅ 0 for some n.

6.6. Remark. This is equivalent to X_{∞} = 0, thus, e is preguarded iff X = ∐_{n≥1} \overline{X}_{n}. This is analogous to Proposition 4.7.

6.7. Theorem. In every iterative algebra all preguarded rational equation morphisms have unique solutions.

Proof. This is completely analogous to the proof in Section 3, see Theorem 4.12 and Corollary 4.14. Given the preguarded rational equation morphism e: X [figure] R(X + A), we have n with X_{n} = 0, i.e., X = \overline{X}_{1} + ⋯ + \overline{X}_{n} and we define a guarded equation morphism

f ≡ \overline{X}_{1} [figure: ī_{1}] X [figure: e] R(X + A) [figure: R(u+A)] R(\overline{X}_{1} + A)

where u: X [figure] \overline{X}_{1} has components id_{\overline{X}_{1}}, \overline{e}_{1}, \overline{e}_{1}·\overline{e}_{2}, …, \overline{e}_{1}·\overline{e}_{2}· · · · ·\overline{e}_{n}. Observe that since u is a split epimorphism and X is finitely presentable, so is \overline{X}_{1}. Thus, f is a rational equation morphism. Since f is guarded, it has a unique solution f^{†}: X [figure] A, see Remark 5.6. The rest is as in Section 3.

6.8. Definition. Let e: X [figure] R(X + A) be a rational equation morphism in an iterative algebra A. A solution e^{†}: X [figure] A of e is called strict if its restriction to every ungrounded subobject is ⊥_{A}. Equivalently, the square

[figure: X; A; e^{†}; X_{n}; X; i_{n}; X_{n}; 1; !; 1; A; ⊥_{A}]

where X_{n} is the largest ungrounded subobject, commutes.

6.9. Theorem. In every iterative algebra every finitary equation morphism has a unique strict solution.

Proof. This is completely analogous to Section 4, see Theorem 5.7 and Corollary 5.9: choose n such that X_{n} = X_{n+1}, see Lemma 6.4, then the role of X_{∞} in Section 4 is now played by X_{n}.

6.10. Example. In the category 𝒥𝒯 of Jónsson-Tarski algebras we present a preguarded morphism with infinitely many (strict) solutions. This demonstrates that hyper-extensi-vity is crucial: recall from Example 2.9 that 𝒥𝒯 is a locally finitely presentable topos!

We use the constant endofunctor H with value 1. Thus, an H-algebra is a pointed Jónsson-Tarski algebra (given by an object A of 𝒥𝒯 and a morphism a: 1 [figure] A) or a Jónsson-Tarski algebra A with a specified idempotent a ∈ A. Every algebra is a cia, see Example 3.3(ii). The free H-algebra on A is of course A + 1 and thus equations in an algebra A have the form

e: X [figure] X + A + 1 for X finitely presentable.

In particular we can use as X the free Jónsson-Tarski algebra Φ(1) on one generator g = g′ ∗ g′′, see 2.9, and we have, for every algebra A, the following equation morphism

e_{A}: Φ(1)  [figure] Φ(1) + A + 1,  e_{A}(g) = g′ ∗ ⊥.

(The right-hand side is the result of the operation ∗ applied to g′ ∈ Φ(1) and ⊥, the unique element of 1,)

(a) The equation e_{A} is preguarded. In fact, recall that Φ(1) = Φ(1) + Φ(1) with coproduct injections l, r, see 2.9. The squares

[figure: Φ(1); Φ(1) + A + 1; inl; Φ(1); Φ(1); id; Φ(1); Φ(1); l; Φ(1); Φ(1) + A + 1; e; Φ(1); Φ(1); r; Φ(1); 1; !; 1; A + 1; inr; A + 1; Φ(1) + A + 1; inr]

are pullbacks. This follows from the extensivity of 𝒥𝒯 : observe that both squares clearly commute and the lower and upper horizontal parts are coproducts. Thus, x_{0} = inl implies x_{1} = l. This shows that all derived subobjects are composites of l:

[figure: ⋯ Φ(1); Φ(1); l; ⋯ Φ(1); ⋯ Φ(1); id; ⋯ Φ(1); Φ(1); l; Φ(1); Φ(1); id; Φ(1); Φ(1); l; Φ(1); Φ(1); Φ(1); Φ(1); l; Φ(1); Φ(1); id; Φ(1); Φ(1) + A + 1; inl; Φ(1); Φ(1); Φ(1); Φ(1); l; Φ(1); Φ(1) + A + 1; e_{A}]

The intersection of all of those subobjects is clearly empty. Consequently, e_{A} has no nontrivial ungrounded subobject: by Remark 4.9 every ungrounded subobject factorizes through the empty (initial) object and is thus empty.

(b) For some algebras A there exist infinitely many solutions of e_{A}. For example, choose A = ℤ and let the binary operation be any bijection

∗: ℤ × ℤ [figure] ℤ with n ∗ 0 = n for all n ∈ ℕ.

Since 0 is an idempotent, we consider (ℤ, ∗) as an H-algebra. Every natural number n = n ∗ 0 yields a solution

e_{ℤ}^{†}: Φ(1)  [figure] ℤ,  g [figure] n.

Conclusions and Future Research

Iterative algebras A are more iterative than what follows immediately from their definition: every equation morphism possesses a unique strict solution in A. This has been known for algebras in Set, see the work of L. Moss [Mo] and S. L. Bloom, C. C. Elgot and J. B. Wright [BEW_{1}, BEW_{2}]. In the present paper we proved this in a general setting (by using a new technique): we worked in locally presentable categories where objects are coproducts of connected components. If 𝒜 is such a category, then so is every presheaf category, thus, also the category

Fin[𝒜 , 𝒜]

of all finitary endofunctors on 𝒜.

In the future research we will apply our result to the study of monadic algebras of the monad

Rat  on  Fin[𝒜 , 𝒜]

which assigns to every finitary endofunctor H the free iterative monad Rat(H) on H (in the sense of Elgot). This monad Rat(H) exists as proved in [AMV_{1}]. We hope to describe the monadic algebras for Rat as “Elgot monads” which are analogous to the Elgot algebras studied in [AMV_{3}].

Another application of the results of the present paper is within the analysis of the relationship of iterative algebras and iteration algebras of Zoltán Ésik, see [ABM].

The assumption that objects are coproducts of their connected components is somewhat restrictive. However, it cannot be completely lifted since in the last example we presented a locally finitely presentable category which, although it is a topos, has nonunique strict solutions of equation morphisms.

References

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

[ABM] J. Adámek, S. L. Bloom and S. Milius, On Iteration in Algebras, to appear in J. Logic Comput.

[AMV_{1}] J. Adámek, S. Milius and J. Velebil, Math. Str. Comput. Sci. 16 (2006), 1085–1131.

[AMV_{2}] J. Adámek, S. Milius and J. Velebil, How iterative are iterative algebras?, extended abstract, Electron Notes Theor. Comput. Sci. 164 (2006), 157–175.

[AMV_{3}] J. Adámek, S. Milius and J. Velebil, Elgot algebras, Logical Methods in Computer Science, 2 (2006), 1–31.

[AR] J. Adámek and J. Rosický, Locally presentable and accessible categories, Cambridge University Press, 1994.

[B] M. Barr, Coequalizers and free triples, Math. Z. 116 (1971), 307–322.

[BEW_{1}] S. L. Bloom, C. C. Elgot and J. B. Wright, Solution of the Iteration Equation and Extensions of the Scalar Iteration Operation, SIAM J. Comp. 9 (1980), 25–45.

[BEW_{2}] S. L. Bloom, C. C. Elgot and J. B. Wright, Vector Iteration in Pointed Iterative Theories, SIAM J. Comp. 9 (1980), 525–540.

[BÉ] S. L. Bloom and Z. Ésik, Iteration Theories: The Equational Logic of Iterative Processes, Springer Verlag, 1993.

[CLW] A. Carboni, S. Lack and R. F. C. Walters, Introduction to extensive and distributive categories, J. Pure Appl. Algebra 84 (1993), 145–158.

[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. Comput. System Sci. 16 (1978), 361–399.

[GU] P. Gabriel and F. Ulmer, Lokal präsentierbare Kategorien, Lecture N. Math. 221, Springer-Verlag, Berlin 1971.

[J] P. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Vol. 1, Oxford Science Publications, Oxford 2002.

[M] S. Milius, Completely Iterative Algebras and Completely Iterative Monads, Inform. and Comput. 196 (2005) 1–41.

[Mo] L. Moss, Recursion and Corecursion Have the Same Equational Logic, Theoret. Comput. Sci. 294 (2003) 233–267.

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

[T] J. Tiuryn, Unique Fixed Points vs. Least Fixed Points, Theoret. Comput. Sci. 12 (1980), 229–254.

Jiří Adámek and Stefan Milius Technical University of Braunschweig, Germany

Reinhard Börger Fernuniversität Hagen, Germany

Jiří Velebil Technical University of Prague, Czech Republic

Email: Adamek@iti.cs-tu.bs.de
Reinhard.Boerger@Fernuni-Hagen.de
mail@stefan-milius.eu
Velebil@math.feld.cvut.cz

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/19/5/19-05.{dvi,ps,pdf}

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. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive abstracts of articles by e-mail as they are published. 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, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

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

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown (at) btinternet.com 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)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 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