1 Introduction

A number of important types of state-based systems can be expressed as coalgebras for finitary endofunctors F of \(\mathbf{Set}\). That is, endofunctors such that every element of FX lies in the image of Fm for some finite subset . Examples include deterministic automata, dynamic systems and finitely branching LTS. The terminal coalgebra \(\nu F\) carries a canonical ultrametric, see [2] or [4]. Recall from [12] that \(\nu F\) represents the set of all possible state behaviors, and given a system as a coalgebra A for F, the unique homomorphism \(h:A \rightarrow \nu F\) assigns to every state its behavior. We are going to prove that whenever F is grounded, i.e., \(F\emptyset \ne \emptyset \), then the initial algebra \(\mu F\) forms a dense subspace of the ultrametric space \(\nu F\). And the coalgebra structure of \(\nu F\) is determined as the unique continuous extension of the inverted algebra structure of \(\mu F\). Moreover, for every coalgebra A we present a canonical Cauchy sequence of morphisms \(h_k:A\rightarrow \mu F\) (\(k<\omega \)) converging to h in the power space \((\nu F)^A\). We thus see that given state-based systems represented by a finitary set functor, (infinite) behaviour of states has canonical finite approximations, see Proposition 18.

All this generalizes from \(\mathbf{Set}\) to every strongly locally finitely presentable category. These categories, introduced in [3] and recalled in Sect. 2 below, include vector spaces, posets and all locally finite varieties (e.g., boolean algebras or \(\mathbb {S}\)-\(\mathbf{Mod}\), semimodules over finite semirings \(\mathbb {S}\)). Every such category has a natural forgetful functor U into \(\mathbf{Set}\). And the underlying set \(U(\nu F)\) of the terminal coalgebra \(\nu F\) carries a canonical ultrametric for every finitary endofunctor preserving monomorphisms. For example, consider the endofunctor of \(\mathbb {S}\)-\(\mathbf{Mod}\) representing weighted automata, \(FX = \mathbb {S} \times X^\varSigma \) (where \(\varSigma \) is a finite set of inputs). It has the terminal coalgebra \(\nu F = \mathbb {S}^{\varSigma ^*}\), the semimodule of weighted languages. The ultrametric assigns to distinct languages \(L_1\), \(L_2\) the distance \(2^{-k}\) for the least k such that for some word \(w\in \varSigma ^*\) of length k the two weights are different, see Example 13(4).

If F is grounded, we again define, for every coalgebra A, a canonical sequence of morphisms \(h_k:A\rightarrow \mu F\) converging to the unique coalgebra homomorphism \(h:A\rightarrow \nu F\) in the power of the above ultrametric space. A concrete example: for every object \(\varSigma \) consider the endofunctor \(FX = X\times \varSigma +1\) where 1 is the terminal object. The underlying set of \(\nu F\) is the set of all finite and infinite words over \(U\varSigma \). And in case U preserves finite coproducts, the underlying set of \(\mu F\) is the set of all finite words. The distance of two distinct words is \(2^{-k}\) for the least k such that their prefixes of lengths at most k are distinct.

Recursive equations in the terminal coalgebra (considered as an algebra) have a unique solution. That is, the algebra \(\nu F\) is completely iterative, see [11]. We define, analogously, a canonical Cauchy sequence of approximate solutions into the initial algebra. And we prove that this sequence converges to the unique solution in \(\nu F\). We recall from Milius [11] the concept of an algebra A for F being completely iterative in Sect. 4. Shortly, this means that for every object X (of recursion variables) and every equation morphism \(e:X\rightarrow FX + A\) there exists a unique solution, which is a morphism \(e^\dag :X\rightarrow A\) satisfying a simple recursive condition. Milius proved that the free completely iterative algebra \(\varPsi B\) on an object B is precisely the terminal coalgebra for the endofunctor \(F(-) + B\):

$$\begin{aligned} \varPsi B = \nu X {.} FX + B. \end{aligned}$$

The functor \(F(-)+B\) is grounded whenever B has a global element. Thus we have the canonical ultrametric on the underlying set of \(\varPsi B\). Moreover, the free algebra \(\varPhi B\) for F on B is well-known to be the initial algebra for the functor \(F(-)+B\):

$$\begin{aligned} \varPhi B = \mu X {.} FX +B. \end{aligned}$$

We are going to present, for every recursive equation e in \(\varPsi B\), a canonical Cauchy sequence of ‘approximate solutions’ \(e^\ddag _k :X\rightarrow \varPhi B\) in the free algebra which converges to the solution \(e^\dag \) in the power space of \(\nu F\), see Theorem 31.

Finally, the same result is proved for the free iterative algebra RB: solutions are limits of sequences of approximate solutions. Recall that ‘iterative’ is the weakening of ‘completely iterative’ by restricting the objects X (of recursion variables) to finitely presentable ones.

Related Work. For finitary set functors preserving \(\omega ^{{\text {op}}}\)-limits Barr proved that the canonical ultrametric of \(\nu F\) is complete, and in case F is grounded this is the Cauchy completion of the subspace \(\mu F\), see [10]. This was generalized to strongly lfp categories in [3]. The fact that preservation of \(\omega ^{op}\)-limits is not needed is new, and so is the fact that the algebra structure of \(\mu F\) determines the coalgebra structure of \(\nu F\).

The idea of approximate homomorphisms and approximate solutions has been used for set functors in the recent paper [5] where instead of ultrametrics complete partial orders were applied. It turns out that the present approach is much more natural and needs less technical preparations.

2 Strongly lfp Categories

Throughout the paper we work with a finitary endofunctor F of a locally finitely presentable (shortly lfp) category. In this preliminary section we recall basic properties of lfp categories and introduce strongly lfp categories.

Recall that an object A of a category is called finitely presentable if its hom-functor preserves filtered colimits. And a category is called lfp, or locally finitely presentable , if it has colimits and a set of finitely presentable objects whose closure under filtered colimits is all of . Every lfp category is complete ([8], Remark 1.56).

Recall further that an endofunctor is called finitary if it preserves filtered colimits.

Example 1

(See [6]). (1) \(\mathbf{Set}\) is lfp. An endofunctor F is finitary iff every element of FX lies in the image of Fm for some finite subset .

(2) K-\(\mathbf{Vec}\), the category of vector space over a field K, is lfp. An endofunctor F is finitary iff every element of FX lies in the image of Fm for some finite-dimensional subspace .

Remark 1

(1) In an lfp category, given a filtered colimit \(a_t:A_t \rightarrow A\) (\(t\in T\)) of a diagram D with all connecting morphisms monic, it follows that

   (a) each \(a_t\) is monic, and

   (b) for every cocone \(f_t:A_t \rightarrow X\) of monomorphisms for D the unique factorization morphism \(f:A\rightarrow X\) is monic.

See [8], Proposition 1.62.

(2) In any category the corresponding statement is true for limits \(a_t :A \rightarrow A_t, t< \lambda \), of \(\lambda \)-chains of monomorphisms for all limit ordinals \(\lambda \):

   (a) each \(a_t\) is monic, and

   (b) for every cone \(f_t:X \rightarrow A_t\) of monomorphisms the factorization morphism \(f:X\rightarrow A\) is monic.

Indeed, (a) follows from the fact that the cone of all \(a_s\) with \(t \le s\) is collectively monic. And (b) is trivial: since \(a_0 \cdot f\) is monic, so is f.

(3) Every lfp category has (strong epi, mono)-factorizations of morphisms, see [8], Proposition 1.61. An epimorphism \(e:A\rightarrow B\) is called strong if for every monomorphism \(m:U\rightarrow V\) the following diagonal fill-in property holds: given a commutative square \(v\cdot e= m\cdot u\) (for some \(u:A\rightarrow U\) and \(v:B\rightarrow V\)) there exists a unique ‘diagonal’ morphism \(d:B\rightarrow U\) with \(u= d\cdot e\) and \(v= m\cdot d\).

(4) An object A of an lfp category is called finitely generated if it is a strong quotient of a finitely presentable object. Equivalently: preserves filtered colimits of monomorphisms, see [8], Proposition 1.69.

(5) The initial object of is denoted by 0. We call it simple if it has no proper strong quotients or, equivalently, if the unique morphism from it to any given object is monic. This holds e.g. in \(\mathbf{Set}\) and K-\(\mathbf{Vec}\). In the lfp category \(\mathbf{Alg}_{1,0}\) of unary algebras with a constant the intial object is the algebra of natural numbers with the successor operation, and it is not simple.

Notation 2

(1) We denote by \(F^n0\) (\(n<\omega \)) the initial-algebra \(\omega \)-chain

$$\begin{aligned} 0 \xrightarrow {\ !\ } F0 \xrightarrow {\ F!\ }F^20 \xrightarrow {\ F^2!\ } \cdots \end{aligned}$$

with connecting maps \(w_{n,k} :F^n0 \rightarrow F^k0\), where \(w_{0,1} = ! \) is unique and \(w_{n+1, k+1} = Fw_{n,k}\). The colimit cocone \(w_{n,\omega } :F^n0 \rightarrow F^\omega 0\) (\(n<\omega \)) of this chain yields, since F is finitary, a colimit cocone \(F w_{n, \omega } :F^{n+1} 0 \rightarrow F (F^\omega 0)\). Consequently, we obtain a unique morphism

$$\begin{aligned} \varphi :F(F^\omega 0) \rightarrow F^\omega 0 \quad \text {with}\quad \varphi \cdot F w_{n,\omega } = w_{n+1, \omega } \quad (n<\omega ). \end{aligned}$$

Then \(F^\omega 0\) is the initial algebra with the algebra structure \(\varphi \), see the second proposition of [1].

(2) We denote by \(F^i1\) () the terminal-coalgebra chain indexed by all ordinals, dually ordered:

$$\begin{aligned} 1 \xleftarrow {\ !\ } F1 \xleftarrow {\ F!\ }FF1 \xleftarrow {\ F^2 !\ } \cdots \quad F^i 1 \leftarrow \quad \cdots \end{aligned}$$

It is given by transfinite recursion: \(F^0 1=1\), \(F^{i+1} 1= F(F^i1)\) and, for limit ordinals i, \( F^i 1 =\lim _{j<i} F^j1\). The connecting maps \(v_{ij} :F^i 1 \rightarrow F^j 1\) (for \(i\ge j\) in ) are determined by transfinite recursion as follows:

$$\begin{aligned} v_{1,0} = ! :F 1\rightarrow 1 \quad \text {(unique)},\qquad v_{i+1, j+1} = F v_{i,j} \end{aligned}$$

and for limit ordinals i the above limit \(F^i 1\) has limit projections \(v_{ij}\) (\(j<i\)).

(3) In case F preserves limits of \(\omega ^{op}\)-sequences the morphism \(v_{\omega +1,\omega }\) is invertible, thus

$$\begin{aligned} \nu F = F^\omega 1, \end{aligned}$$

with the coalgebra structure given by \({\tau } = v_{\omega +1,\omega }^{-1}\).

Theorem 3

([9], Thm. 2.6). If a finitary endofunctor F of an lfp category preserves monomorphisms, then it has a terminal coalgebra \(\nu F = F^i 1\) for some ordinal \(i\ge \omega \) with \(v_{i+1, i}\) invertible. The coalgebra structure is \(\tau = v_{i+1, i}^{-1} :F^i 1 \rightarrow F (F^i 1)\).

Proposition 4

Let be an lfp category with a simple initial object. For every finitary endofunctor F preserving monomorphisms the initial algebra is a canonical subobject of the terminal coalgebra: the unique algebra homomorphism

$$\begin{aligned} m :(\mu F, \varphi ) \rightarrow (\nu F, \tau ^{-1}) \end{aligned}$$

is monic.

Proof

The initial-algebra \(\omega \)-chain has a unique cocone \(m_k:F^k 0 \rightarrow \nu F\) (\(k<\omega \)) satisfying the following recursion

$$\begin{aligned} m_{k+1} \equiv F(F^k 0) \xrightarrow {\ Fm_k\ } F(\nu F) \xrightarrow {\ \tau ^{-1}\ } \nu F \quad (k<\omega ). \end{aligned}$$

Since \(m_0 :0 \rightarrow \nu F\) is monic and F preserves monomophisms, each \(m_k\) is monic. Therefore, the unique morphism

$$\begin{aligned} m:F^\omega 0 \rightarrow \nu F \quad \text {with} \quad m\cdot w_{k, \omega } = m_k\quad (k<\omega ) \end{aligned}$$

is monic, see Remark 1(1). And this is an algebra homomorphism, i.e., \(m\cdot \varphi = \tau ^{-1} \cdot Fm :F(\mu F) \rightarrow \nu F\). To verify this, recall that F preserves colimits of chains, hence \((F w_{k,\omega })_{k<\omega }\) is a collectively epic cocone. Thus, we only need to verify

$$\begin{aligned} m\cdot \varphi \cdot F w_{k, \omega } =\tau ^{-1} \cdot F m\cdot F w_{k, \omega } \quad (k<\omega ). \end{aligned}$$

By definition of \(\varphi \), the left-hand side is \( m\cdot w_{k+1, \omega } = m_{k+1}\). The right-hand one is the same: \( \tau ^{-1} \cdot F m_{k} = m_{k+1}\).

Remark 2

An object G of is called a generator if its hom-functor is faithful. Thus becomes a concrete category w.r.t. that hom-functor. For example K is a generator of K-\(\mathbf{Vec}\), and the terminal object 1 is a generator of \(\mathbf{Set}\) or \(\mathbf{Pos}\) (the category of posets). In all these examples the above functor U is naturally isomorphic to the usual forgetful functor.

Definition 5

(See [4]). An lfp category is called strongly lfp provided that

(a) for every limit cone \(a_k:A\rightarrow A_k\) (\(k<\omega \)) of an \(\omega ^{{\text {op}}}\)-chain and every monomorphism \(m:M\rightarrow A\) with M finitely generated there exists k with \(a_k \cdot m :M\rightarrow A_k\) monic, and

(b) a generator G is given.

In [4] the generator was assumed to be projective, but we do not need this assumption. Moreover, in that paper instead of our present factorization system (strong epi, mono) the system (epi, strong mono) was used.

Example 6

(1) \(\mathbf{Set}\) is strongly lfp. Indeed, given an \(\omega ^{{\text {op}}}\)-limit \(a_k:A\rightarrow A_k\) (\(k<\omega \)) and a finite subset \(m:M\rightarrow A\), for every pair \(x\ne y\) in M there exists k with \(a_k (x) \ne a_k(y)\). Since \(M\times M\) is finite, k can be chosen independent of x, y. Thus, \(a_k \cdot m\) is monic.

(2) Every variety of algebras which is locally finite (i.e., finitely generated algebras are finite) is strongly lfp. The free algebra G on one generator is a generator. And since limits are formed on the level of sets, the \(\omega ^{{\text {op}}}\)-limit condition is verified precisely as in (1).

Examples include semilattices, boolean algebras, categories \(\mathbb {S}\)-\(\mathbf{Mod}\) of left semimodules over a finite semiring \(\mathbb {S}\), and categories M-\(\mathbf{Set}\) of sets with an action of a finite monoid M.

(3) The category K-\(\mathbf{Vec}\) of vector spaces is strongly lfp for every (possibly infinite) field K, see [3], Example 4.5(5).

(4) The category \(\mathbf{Pos}\) of posets is strongly lfp whose terminal object is a generator. The \(\omega ^{{\text {op}}}\)-limit condition is verified as in (1) above.

(5) The category \(\mathbf{Gra}\) of graphs (sets with a binary relation) and graph homomorphisms is strongly lfp. The single-vertex graph G without edges is a generator, and the \(\omega ^{{\text {op}}}\)-limit condition is verified as in (1).

Notation 7

Given a strongly lfp category with a generator G, we denote by

the hom-functor of G. This is a faithful functor preserving limits (in particular, it preserves monomorphisms).

Remark 3

(1) In contrast to examples (2) and (3) above, the categories \(\mathbb {Z}\)-\(\mathbf{Mod}\) of abelian groups and \(\mathbb {Z}\)-\(\mathbf{Set}\) of unary algebras on one operation are not strongly lfp, see [3], Example 4.5.

(2) Worrell [13] proved that for every finitary set functor F all the connecting maps \(v_{i, \omega }\), \(i>\omega \), are monic. This can be generalized as follows.

Theorem 8

Let be a strongly lfp category. For every finitary endofunctor F preserving monomorphisms the terminal coalgebra \(\nu F = F^i 1\) (see Theorem 3) is a canonical subobject of \(F^\omega 1\): the morphism \(v_{i\omega }\) is monic.

Proof

We prove that for all ordinals \(j>\omega \) the connecting maps \(v_{j\omega }\) are monic by transfinite induction.

(1) \(v_{\omega +1, \omega } :F(F^\omega 1)\rightarrow F^\omega 1\) is monic. To prove this, use the fact that is lfp and choose a filtered diagram D of finitely presentable objects \(A_t\) (\(t\in T\)) with a colimit cocone \(a_t :A_t \rightarrow F^\omega 1\). Due to Remark 1(3) we have a factorization \(a_t = b_t\cdot e_t\) for a strong epimorphism \(e_t:A_t \rightarrow B_t\) and a monomorphism \(b_t :B_t \rightarrow F^\omega 1\). The objects \(B_t\) (\(t\in T\)) form a filtered diagram \(\bar{D}\) whose connecting morphisms are derived via diagonal fill-in: given a connecting morphism \(a_{t,t'} :A_t \rightarrow A_{t'}\) in D, we obtain a connecting morphism \(b_{t, t'} :B_t \rightarrow B_{t'}\) of \(\bar{D}\) by means of the following diagonal:

figure a

It is easy to verify that \(\bar{D}\) a filtered diagram (since D is) and the morphisms \(b_t :B_t \rightarrow F^\omega 1\) (\(t\in T\)) form the colimit cocone of \(\bar{D}\). Moreover, each connecting morphism \(b_{t, t'}\) is monic (since its composite with \(b_{t'}\) is). Hence, our assumption that F is finitary and preserves monomorphisms implies that we have a filtered diagram \(F\bar{D}\) of all \(FB_t\) (\(t\in T\)) whose connecting morphisms are monic and whose colimit is \((Fb_t)_{t\in T}\). Using Remark 1(1) it is sufficient, for proving that \(v_{\omega +1, \omega }\) is monic, to verify that (for every \(t\in T\))

$$\begin{aligned} v_{\omega +1, \omega } \cdot F b_t :FB_t \rightarrowtail F^\omega 1 \quad \text {is monic}. \end{aligned}$$

Since our category is strongly lfp and \(B_t\) is finitely generated (being a strong quotient of the finitely presentable object \(A_t\)), it follows that for the monomorphism \(b_t\) there exists \(k<\omega \) with \(v_{\omega , k}\cdot b_t\) monic. Thus, the morphism \( F v_{\omega , k} \cdot F b_t = v_{\omega , k+1} \cdot v_{\omega +1, \omega } \cdot F b_t= v_{\omega +1, \omega } \cdot Fb_t\) is monic, as desired.

(2) Each \(v_{i, \omega }\) for \(i>\omega \) is monic. This is easily seen by transfinite induction on i. The case \(i= \omega +1\) has just been proved. If \(v_{i, \omega }\) is monic, so is \(F v_{i, \omega } = v_{i+1, \omega +1}\), therefore, the composite \( v_{i+1, \omega } = v_{\omega +1, \omega } \cdot v_{i+1, \omega +1} \) is also monic. And given a limit ordinal \(i>\omega \), then each connecting map \(v_{k,j}\), where \(\omega \le j\le k<i\) is monic, since \(v_{j, \omega } \cdot v_{k,j} = v_{k, \omega }\) is monic, see Remark 1(2). Now \(F^i1\) is a limit of the chain \(F^j 1\) for all \(\omega \le j<i\) whose connecting morphisms are monic. This implies that the limit cone consists of monomorphisms. In particular, \(v_{i, \omega }\) is monic, as required.

Lemma 9

For i in Theorem 8 the following squares commute:

figure b

Proof

We proceed by induction, the case \(k=0\) is clear. Recall that m is an algebra homomorphism:

$$\begin{aligned} m\cdot \varphi = \tau ^{-1} \cdot F m = v_{i+1, i} \cdot Fm. \end{aligned}$$
(2.1)

By definition of \(\varphi \) we have \(\varphi \cdot Fw_{k, \omega }= w_{k+1, \omega }\) (Notation 2(1)), thus,

$$\begin{aligned} m\cdot w_{k+1, \omega } = v_{i+1, i} \cdot Fm \cdot F w_{k, \omega }. \end{aligned}$$
(2.2)

Assuming the above square commutes for k, we prove it for \(k+1\):

$$\begin{aligned} F^{k+1} !&= F( v_{i,k} \cdot m \cdot w_{k, \omega })&\text {induction hypothesis}\\&= v_{i+1, k+1} \cdot Fm\cdot Fw_{k, \omega }&v_{i+1, k+1}= Fv_{i,k}\\&= v_{i, k+1} \cdot v_{i+1, i}\cdot Fm \cdot Fw_{k, \omega }&\\&= v_{i, k+1} \cdot m \cdot w_{k+1, \omega }&\text {by }(2.2) \end{aligned}$$

Since \(v_{i,k}\) is the composite \(v_{\omega , k} \cdot v_{i, \omega }\), we obtain the following corollary of Theorem 8:

Corollary 10

If the initial object is simple, then the following monomorphism

$$\begin{aligned} \bar{u} \equiv \mu F \xrightarrow {\ m\ } F^i 1 \xrightarrow {\ v_{i, \omega \ }} F^\omega 1 \end{aligned}$$

makes the squares below commutative

figure c

3 Approximate Homomorphisms

Assumption 11

Throughout the rest of the paper denotes a strongly lfp category with a simple initial object, and F a finitary endofunctor preserving monomorphisms.

Recall that the initial algebra \(\mu F\) is a canonical subobject of the terminal coalgebra \(\nu F\) (Proposition 4). For the forgetful functor of Notation 7 we present a canonical ultrametric on the underlying set \(U(\nu F)\) of the terminal coalgebra. Then \(U(\mu F)\) is a subspace of that ultrametric space, since U preserves monomorphisms. We prove that those two ultrametric spaces have the same Cauchy completion. Moreover, given an arbitrary coalgebra \(\alpha :A\rightarrow FA\), the unique homomorphism into \(\nu F\) is determined by a Cauchy sequence of (approximate) morphisms from A to \(\mu F\).

Remark 4

(1) Recall that a metric d is called an ultrametric if the triangle inequality can be strengthened to \(d(x,z) \le \max \big (d(x,y), d(y,z)\big )\). We denote by \(\mathbf{UMet}\) the category of ultrametric space with distances at most 1 and nonexpanding functions. That is, functions \(f:(X,d) \rightarrow (X', d')\) with \(d(x,y) \ge d'\big (f(x), f(y)\big )\) for all x, \(y\in X\).

(2) The category \(\mathbf{UMet}\) has products w.r.t. the supremum metric. In particular, for every set M the power \((X,d)^M\) is the ultrametric space of all functions \(f:M\rightarrow X\) with distances given by

$$\begin{aligned} d(f, f') =\sup _{m\in M} \big (d(f(m), f'(m)\big ) \quad \text {for }\ \ f, f'\in X^M. \end{aligned}$$

(3) Completeness of an ultrametric space means that every Cauchy sequence has a limit. Every \(\omega ^{{\text {op}}}\)-sequence of morphisms \(a_{k+1, k} :A_{k+1} \rightarrow A_k\) (\(k<\omega \)) in \(\mathbf{Set}\) carries a canonical complete ultrametric on its limit \(A=\lim \limits _{k<\omega }A_k\) in \(\mathbf{Set}\) (with limit projections \(a_k:A\rightarrow A_k\))): Given elements \(x\ne y\) of A, their distance is defined by

$$\begin{aligned} d(x,y) = 2^{-k} \end{aligned}$$

for the least k with \({a}_k (x) \ne {a}_k(y)\). It is easy to verify that (Ad) is a complete ultrametric space, see also [4], Lemma 32.

(4) We apply this to the limit \(F^\omega 1= \lim \limits _{n<\omega } F^n 1\) of Notation 2(2). Since the forgetful functor preserves limits, \(U(F^\omega 1)\) is a limit with projections \(U v_{\omega , k}\) (\(k<\omega \)).

Corollary 12

The underlying set of \(F^\omega 1\) carries the following complete ultrametric: given distinct elements x, \(y:G\rightarrow F^\omega 1\) of \(U(F^\omega 1)\), their distance is \(2^{-k}\) for the least k with \(v_{\omega , k}\cdot x \ne v_{\omega , k}\cdot y\).

The monomorphisms

$$\begin{aligned} m:\mu F \rightarrow \nu F \quad \text {and} \quad v_{i, \omega }:\nu F \rightarrow F^\omega 1 \end{aligned}$$

of Proposition 4 and Theorem 3 are preserved by U, thus we have ultrametric subspaces \(U(\mu F) \subseteq U (\nu F) \subseteq U(F^\omega 1)\).

Example 13

(1) For the set functor \(FX =\varSigma \times X+1\) (whose coalgebras are dynamic systems with inputs from \(\varSigma \) and terminating states) the terminal-coalgebra chain

$$\begin{aligned} 1\leftarrow \varSigma +1 \leftarrow \varSigma \times \varSigma +\varSigma +1 \leftarrow \ \cdots \end{aligned}$$

is given by \(F^k1=\) words of length \(\le k\). And \(v_{k+1,k}\) deletes the first letter in every word of length \(k+1\). The limit of this \(\omega ^{{\text {op}}}\)-sequence is

$$\begin{aligned} \nu F= F^\omega 1 = \varSigma ^\omega + \varSigma ^*. \end{aligned}$$

The projection \(v_{\omega ,k}\) leaves words of length \(\le k\) unchanged and otherwise forms prefixes of length k. Thus the distance of distinct words is \(2^{-k}\) for the least k for which their prefixes of length at most k are distinct.

The initial-algebra chain

$$\begin{aligned} 0\rightarrow 1\rightarrow \varSigma +1\rightarrow (\varSigma \times \varSigma ) +\varSigma +1\rightarrow \ \ \cdots \end{aligned}$$

is given by \(F^k0=\) words of length less than k. And \(w_{k, k+1}\) is the inclusion. This yields the colimit

$$\begin{aligned} \mu F =\varSigma ^*\end{aligned}$$

with the above ultrametric.

(2) More generally, given a set B, then \(FX =\varSigma \times X +B\) has the terminal coalgebra \(\nu F =\varSigma ^\omega +\varSigma ^*\times B\). Words in \(\varSigma ^*\times B\) with distinct B-components have distance 1, otherwise the ultrametric is analogous to (1). And \(\mu F=\varSigma ^*\times B\).

(3) Deterministic automata with the input alphabet \(\varSigma \) are coalgebras of the set functor \(FX =\{0,1\} \times X^\varSigma \). The terminal-coalgebra chain

$$\begin{aligned} 1\leftarrow \{0,1\} \leftarrow \{0,1\}^{1+\varSigma } \leftarrow \{0,1\}^{1+\varSigma +\varSigma ^2} \leftarrow \ \cdots \end{aligned}$$

is given by powers of \(\{0,1\}\) to \(\coprod \limits _{n=0}^k \varSigma ^n\). Thus, \(F^k 1\) are all formal languages using words of length at most k. And \(v_{k+1,k}\) deletes the first letter in every word of length \(k+1\). Since F preserves limits of \(\omega ^{op}\)-sequences, we have

$$\begin{aligned} \nu F = F^\omega 1 = \text {all formal languages.} \end{aligned}$$

The distance of distinct languages is \(2^{-k}\) for the least k such that there is a word of length k lying in precisely one of those languages. Here \(\mu F=\emptyset \).

(4) Weighted automata with weights in a finite semiring \(\mathbb {S}\) and the input alphabet \(\varSigma \) are coalgebras for the endofunctor of \(\mathbb {S}\)-\(\mathbf{Mod}\) defined by \(FX= \mathbb {S}\times X^\varSigma \). The terminal-coalgebra chain is given by left-hand projections \(\pi _1\):

$$\begin{aligned} 1 \xleftarrow {\ \pi _1=0\ } \mathbb {S}\xleftarrow {\ \pi _1\ }\mathbb {S}\times \mathbb {S}^\varSigma \xleftarrow {\ \pi _1\ } (\mathbb {S}\times \mathbb {S}^\varSigma )\times \mathbb {S}^{\varSigma \times \varSigma } \simeq \mathbb {S}^{1+\varSigma +\varSigma ^2} \xleftarrow {\ \pi _1\ } \ \cdots \end{aligned}$$

This yields as \(F^k 1\) the set of all weighted languages with weight 0 for all words longer than k. And \(v_{k+1, k}\) changes weights of words of length \(k+1\) to 0. Here, again, F preserves limits of \(\omega ^{op}\)-sequences, thus

$$\begin{aligned} \nu F = F^\omega 1 = {\mathbb {S}}^{\varSigma ^*} \end{aligned}$$

the set of all weighted languages. The distance of distinct languages is \(2^{-k}\) for the least k with their k-components distinct.

The initial-algebra chain has the same objects, and \(w_{k, k+1}\) are the coproduct injections (using that in \(\mathbb {S}\)-\(\mathbf{Mod}\) we have \(A+B=A \times B\)). Thus the initial algebra is

$$\begin{aligned} \mu F= \text {all bounded weighted languages,} \end{aligned}$$

where bounded means that for some number k all words of nonzero weight have length at most k.

(5) Let \(\varGamma \) be a signature, \(\varGamma = (\varGamma _n)_{n\in \mathbb {N}}\). The polynomial set functor \(H_\varGamma X = \underset{n\in \mathbb {N}}{\coprod } \varGamma _n \times X^n\) has the terminal coalgebra \(\nu H_\varGamma \) consisting of all \(\varGamma \)-trees, i.e., trees labelled by \(\varGamma \) so that a node with a label in \(\varGamma _n\) has n successors. (We always consider trees up to isomorphism.) We can represent \(H_\varGamma ^k 0\) by the set of all \(\varGamma \)-trees of height less than k, thus the colimit

$$\begin{aligned} \mu H_\varSigma =\underset{k\in \mathbb {N}}{\bigcup } H_\varGamma ^k 0 \end{aligned}$$

is given by all finite \(\varGamma \)-trees.

The distance of trees \(t\ne s\) in \(\nu H_\varGamma \) is \(2^{-k}\) for the least k such that by cutting t and s at level k one obtains distinct trees.

Remark 5

Example (1) above generalizes to all strongly lfp categories whose forgetful functor preserves finite coproducts, e.g. \(\mathbf{Pos}\) and \(\mathbf{Gra}\). Given an object \(\varSigma \), the functor \(FX = X\times \varSigma +1\) is finitary and the forgetful functor U (preserving all limits) takes the terminal-coalgebra chain

$$\begin{aligned} 1 \leftarrow \varSigma +1 \leftarrow \varSigma \times \varSigma +\varSigma +1 \leftarrow \ \cdots \end{aligned}$$

in to the terminal-coalgebra chain of the set-functor \((-)\times U\varSigma +1\). The terminal coalgebra \(\nu F\) has the underlying set \(U(\nu F)= (U\varSigma )^\omega +(U\varSigma )^*\), and the distance of words is as described above. If, moreover, G is a finitely presentable generator (which is true in all of our examples), then U also takes the initial-algebra chain of F to that of the set functor \((-) \times U\varSigma +1\). Thus, \(U(\mu F)= (U\varSigma )^*\).

Definition 14

An endofunctor F is grounded if F0 has a global element, i.e., a morphism \(p:1\rightarrow F0\) is given.

Proposition 15

The ultrametric subspace \(U(\mu F)\) is dense in \(U(\nu F)\) whenever F is grounded. These two spaces have the same Cauchy completion, viz, \(U(F^\omega 1)\).

Proof

(1) We prove that the embedding \(U \bar{u} :U(\mu F) \rightarrow U(F^\omega 1)\), see Corollary 10, is dense. Since \(U(F^\omega 1)\) is complete, both statements above follow from this fact. Thus given an element \(x:G\rightarrow F^\omega 1\) of \(U(F^\omega 1)\), we are to present a sequence \(x_k :G\rightarrow F^\omega 1\) (\(k<\omega \)) of morphisms factorizing through \(\bar{u}\) with \(x =\underset{k\rightarrow \infty }{\lim }x_k\) in the supremum metric of Remark 4(2).

(2) For every \(k<\omega \) consider the following endomorphism of \(F^\omega 1\) using the global element \(p:1\rightarrow F0\):

$$\begin{aligned} r_k \equiv F^\omega 1\xrightarrow {\ v_{\omega , k}\ } F^k 1 \xrightarrow {\ F^k p\ } F^{k+1} 0 \xrightarrow {\ w_{ k+1, \omega }\ } F^\omega 0 \xrightarrow {\ \bar{u}\ }F^\omega 1\,. \end{aligned}$$
(3.1)

It fulfils, due to Corollary 10

$$\begin{aligned} v_{\omega , k+1} \cdot r_k = F^{k+1} ! \cdot F^k p \cdot v_{\omega , k}. \end{aligned}$$
(3.2)

In Notation 2 we see that \(v_{k+1, k} = F^k v_{1,0}\), thus the (obvious) equality yields

(3.3)

Consequently

$$\begin{aligned} v_{\omega , k} \cdot r_k = v_{\omega , k}. \end{aligned}$$
(3.4)

Indeed, by (3.2) and \(v_{\omega , k} = v_{k+1, k} \cdot v_{\omega , k+1}\) we see that the left-hand side is \(v_{k+1, k}\cdot F^{k+1} ! \cdot F^k p\cdot v_{\omega , k}\) which is \(v_{\omega , k}\) by (3.3).

(3) The desired sequence is

$$\begin{aligned} x_k = r_k \cdot x. \end{aligned}$$

It converges to x because (3.4) yields \(v_{\omega , k} \cdot (r_k\cdot x) = v_{\omega , k}\cdot x\), thus \(d (r_k\cdot x, x)< 2^{-k}\). And since \(r_k\) factorizes through \(\bar{u}\), this concludes the proof.

The following corollary was already proved by Barr [10]:

Corollary 16

If, moreover, F preserves limits of \(\omega ^{{\text {op}}}\) sequences, then the ultrametric space corresponding to \(\nu F\) is the Cauchy completion of the subspace \(\mu F\).

For every coalgebra \(\alpha :A \rightarrow FA\) carried by a set \(M=UA\) the unique coalgebra homomorphism \(h:A\rightarrow \nu F\) lies in the metric space \(U(\nu F)^M\), see Remark 4(2). And \(U(\mu F)^M\) is a subspace via the post-composition with m of Proposition 4. We are going to prove that h is the limit of a canonical Cauchy sequence in the subspace \(U(\mu F)^M\).

Definition 17

For every coalgebra \((A, \alpha )\) we define the sequence \(h_k:A\rightarrow \mu F\) (\(k<\omega \)) of approximate homomorphisms by induction as follows

$$\begin{aligned} h_0&\equiv A \xrightarrow {\ ! \ } 1 \xrightarrow {\ p \ } F0 \xrightarrow {\ w_{1,\omega }\ } \mu F \end{aligned}$$

and

$$\begin{aligned} h_{k+1}&\equiv A \xrightarrow {\ \alpha \ } FA \xrightarrow {\ F h_k\ } F(\mu F) \xrightarrow {\ \varphi \ }\mu F\,. \end{aligned}$$
(3.5)

Thus \(h_0\) is a trivial approximation, independent of the given coalgebra structure: it just uses the global element p. Given an approximation \(h_k\), the next one is given by a square similar to the square defining coalagebra homomorphisms:

figure d

Let us remark that we do not claim that \(h_k\) are coalgebra homomorphisms.

Proposition 18

For every coalgebra \((A, \alpha )\) on the set \(M=UA\) the unique coalgebra homomorphism \(h:A \rightarrow \nu F\) is a limit of the approximate homomorphisms. More precisely: in the ultrametric space \(U(\nu F)^M\) we have

$$\begin{aligned} Uh =\lim _{k\rightarrow \infty } U(m\cdot h_k)\,. \end{aligned}$$

Proof

We prove by induction on k that \(d\big ( Uh, U (m\cdot h_k)\big ) \le 2^{-k}\). This is trivial for \(k=0\) (recall that we assume that all distances are at most 1). If this holds for k, we prove it for \(k+1\). Since h is a coalgebra homomorphism and we have an ordinal i with \(\tau ^{-1}= v_{i+1, i}\) (see Theorem 3), we get

$$\begin{aligned} h= v_{i+1, i} \cdot Fh \cdot \alpha . \end{aligned}$$
(3.6)

As m is an algebra homomorphism (see Proposition 4), we have

$$\begin{aligned} m\cdot \varphi = \tau ^{-1} \cdot Fm = v_{i+1,i} \cdot Fm \end{aligned}$$
(3.7)

The induction hypothesis is that \(v_{i, k-1}\) merges h and \(m\cdot h_k\):

$$\begin{aligned} v_{i, k-1} \cdot h = v_{i, k-1} \cdot m\cdot h_k \end{aligned}$$
(3.8)

and our task is to prove that \(v_{i, k}\) merges h and \(m\cdot h_{k+1}\):

$$\begin{aligned} v_{i,k} \cdot h&=v_{i,k} \cdot v_{i+1, i} \cdot Fh \cdot \alpha&\text {by }(3.6)\\&= F v_{i,k-1} \cdot Fh \cdot \alpha&v_{i,k} \cdot v_{i+1, i} = v_{i+1,k} = Fv_{i, k-1}\\&= F \big (v_{i, k-1} \cdot m\cdot h_k\big ) \cdot \alpha&\text {by }(3.8)\\&= v_{i,k} \cdot v_{i+1, i} \cdot Fm \cdot Fh_k\cdot \alpha&\text {as above}\\&=v_{i,k} \cdot m \cdot \varphi \cdot Fh_k\cdot \alpha&\text {by }(3.7)\\&= v_{i,k} \cdot m\cdot h_{k+1}&\text {by }(3.5) \end{aligned}$$

Notation 19

Define morphisms \(\partial _k :\nu F \rightarrow \mu F\) for \(k<\omega \) as the following composites

$$\begin{aligned} \partial _k \equiv F^i 1 \xrightarrow {\ v_{i,k}\ } F^k 1 \xrightarrow {\ F^k p\ } F^{k+1}0 \xrightarrow {\ w_{k+1, \omega }\ } F^\omega 0. \end{aligned}$$

We prove below that this sequence (prolonged by the embedding \(m:\mu F \rightarrow \nu F\)) converges to . The following examples give an intuition how these approximations of the identity morphism work.

Example 20

(1) For \(FX = X\times \varSigma +B\) of Example 13(2) with a chosen element \(p\in B\) the map \(\partial _k:\varSigma ^\omega +\varSigma ^*\times B\rightarrow \varSigma ^*\times B\) assigns to an infinite word w the pair \((w', p)\) where \(w'\) is the prefix of length k. And to pairs \((w,b)\in \varSigma ^*\times B\) it assigns analogously \((w', p)\) if \(|w|\ge k\), whereas \(\partial _k (w,b)=(w,b)\) if \(|w|<k\).

(2) For a polynomial functor \(H_\varGamma \) of Example 13(4) we have \(\partial _k:\nu H_\varGamma \rightarrow \mu H_\varGamma \) which cuts every \(\varGamma \)-tree at height k and relabels all leaves of height k by p (the chosen nullary symbol).

Lemma 21

For every \(k<\omega \) we have \(v_{i,k}= v_{i,k}\cdot m\cdot \partial _k\). Therefore, the sequence \(m\cdot \partial _k\) converges to in the ultrametric space of endomorphisms of \(U(\nu F)\):

$$\begin{aligned} \lim _{k\rightarrow \infty } U(m\cdot \partial _k) =id _{U(\nu F)}\,. \end{aligned}$$

Proof

It is sufficient to prove that first identity, since this implies that and \(U(m\cdot \partial _k)\) have distance smaller than \(2^{-k}\).

From Notation 2 we know that \(v_{i,k}= v_{k+1, k} \cdot v_{i, k+1}\). Thus

4 Approximate Solutions

We apply the above results to the finitary endofunctor

$$\begin{aligned} F_B = F(-) +B \end{aligned}$$

for an arbitrary object B. We want \(F_B\) to preserve monomorphisms whenever F does. We therefore need the following (mild) additional assumption:

Assumption 22

Additionally to the assumptions of Sect. 3 we assume that has monic coproduct injections and that \(m+B :X+B \rightarrow Y+B\) is monic for every monomorphism \(m:X\rightarrow Y\). (This holds in all Examples of 6.)

Notation 23

Assume that B is a pointed object, i.e., a global element \(p:1 \rightarrow B\) is given. Then \(F_B\) is a grounded endofunctor w.r.t. the following global element

Definition 24

(See [11]). Let an algebra \(\alpha :FA \rightarrow A\) be given. A (recursive) equation with an object X (of recursive variables) is a morphism \(e:X \rightarrow FX +A\). A solution of e is a morphism \(e^\dag :X\rightarrow A\) making the following square

figure e

commutative.

An algebra in which every equation has a unique solution is said to be completely iterative.

Example 25

(see [11]). (1) The terminal coalgebra \(\nu F\) considered as an algebra (via \(\tau ^{-1}\)) is completely iterative.

(2) Denote by \(\varPsi _B\) the terminal coalgebra of the endofunctor \(F_B = F(-) +B\),

$$\begin{aligned} \varPsi _B = \nu F_B\,. \end{aligned}$$

Its coalgebra structure \(\tau _B :\varPsi B \rightarrow F(\varPsi B)+B\) yields an inverse with components

$$\begin{aligned} \psi _B :F(\varPsi B)\rightarrow \varPsi B \quad \text {and} \quad \eta _B :B \rightarrow \varPsi B. \end{aligned}$$

The resulting algebra \(\varPsi B\) for F is completely iterative.

Indeed, this is the free completely iterative algebra on B. That is, for every completely iterative algebra \(\alpha :FA \rightarrow A\) and every morphism \(f:B\rightarrow A\) there exists a unique algebra homomorphism \(f^{\#} :\varPsi B \rightarrow A\) with \(f= f^{\#} \cdot \eta _B\).

(3) Let us illustrate the iterativity of \(\varPsi B\) on the set functor \(FX =\varSigma \times X\) where \(\varSigma =\{\sigma , \tau \}\). From Example 13(2) we know that \(\varPsi B =\varSigma ^\omega +\varSigma ^*\times B \). Let e be the following equation with recursive variables \(X=\{x,y,z\}\):

$$\begin{aligned} e(x) = (\sigma , y)\,, \ e(y)=(\tau , x) \quad \text {and} \quad e(z) =(\sigma \tau , b). \end{aligned}$$

The solution \(e^\dag :X\rightarrow \varSigma ^\omega +\varSigma ^*\times B \) is, clearly, given by

$$\begin{aligned} e^\dag (x) = (\sigma \tau )^\omega \,,\ e^\dag (y) =(\tau \sigma )^\omega \quad \text {and}\quad e^\dag (z) = (\sigma \tau , b). \end{aligned}$$

For a general equation \(e:X \rightarrow \varSigma \times X +(\varSigma ^\omega +\varSigma ^*\times B)\) the solution \(e^\dag :X \rightarrow \varSigma ^\omega +\varSigma ^*\times B\) is defined by the following corecursion: if e(x) lies in the right-hand summand \(\varSigma ^\omega +\varSigma ^*\times B\) then simply \(e^\dag (x) = e(x)\). Otherwise we have a pair \( (\sigma _1, x_1) \in \varSigma \times X\) with \(e(x) = (\sigma _1, x_1)\) and \(e^\dag \) assigns to x the word assigned to \(x_1\) with the prefix \(\sigma _1\) added:

$$\begin{aligned} e^\dag (x) = \sigma _1 e^\dag (x_1). \end{aligned}$$

(4) Given an arbitrary polynomial functor \(H_\varGamma \) of Example 13(5) the functor \(H_\varGamma (-) + B\) is also polynomial for the signature \(\varGamma +B\), where B consists of constants. Thus \(\varPsi B\) is the algebra for all \(\varGamma \)-trees over B, i.e., leaves are labelled in the set \(\varGamma _0 +B\) and nodes with \(n>0\) successors in \(\varGamma _n\).

A solution of an equation \(e:X \rightarrow H_\varGamma X+(B+\varPsi B)\) is the map \(e^\dag :X \rightarrow B+\varPsi B\) assigning to a variable x with e(x) in the right-hand smmand the value \(e^\dag (x)=e(x)\). For the left-hand summand we have

$$\begin{aligned} e(x)=\sigma (x_1,...,x_n) \end{aligned}$$

for some n-ary symbol \(\sigma \), and \(e^\dag (x)\) is the tree with root labelled by \(\sigma \) and with the n maximum subtrees given by \(e^\dag (x_1))\),..., \(e^\dag (x_n)\).

Remark 6

For the terminal coalgebra \(\nu F\) considered as an algebra we now show how solutions of equations \(e:X\rightarrow FX +\nu F\) can be approximated by sequences of morphisms \(e^\ddag _k :X\rightarrow \mu F\) into the initial algebra. Recall that the morphisms \(\partial _k :\nu F \rightarrow \mu F \) of Lemma 21 converge to . This indicates that the equation morphism e is well approximated by the following sequence of equation morphisms in \(\mu F\):

$$\begin{aligned} e_k \equiv X \xrightarrow {\ e\ } FX + \nu F \xrightarrow {\ FX + \partial _k\ } FX + \mu F \quad (k<\omega )\,. \end{aligned}$$
(4.1)

We use them to define approximate solutions of e:

Definition 26

Let an equation in \(\nu F\) be given, \(e:X\rightarrow FX + \nu F\). We define its approximate solutions \(e^\ddagger _k :X \rightarrow \mu F\) by induction as follows: first put

$$\begin{aligned} e_0^\ddagger \equiv X \xrightarrow {\ !\ } 1 \xrightarrow {\ p\ } F0 \xrightarrow {\ w_{1, \omega }\ } \mu F. \end{aligned}$$
(4.2)

Given \(e_k^\ddagger \) define \(e_{k+1}^\ddagger \) as the following composite:

(4.3)

where \(e_k =(FX + \partial _k)\cdot e\).

Observe that the first approximation \(e^\ddagger _0\) does not use the algebra structure of \(\mu F\). For the subsequent approximations the square defining solutions in Definition 24 is quite analogous to (4.4). We see that, however, \(e_k^\ddagger \) is not a solution of \(e_k\) in \(\mu F\) in general.

Proposition 27

The solution of every equation \(e:X\rightarrow FX +\nu F\) in the terminal coalgebra (considered as algebra) is a limit of approximate solutions. More precisely, we have

$$\begin{aligned} U e^\dag =\lim _{k\rightarrow \infty } U (m\cdot e_k^\ddagger ). \end{aligned}$$

in the power of the ultrametric space \(U(\nu F)\) to UX.

We are going to prove a more general result about approximate solutions for equation in \(\varPsi B\), the free completely iterative algebra, below. Since for \(B=0\) we have \(\nu F = \varPsi 0\), the above proposition then follows.

Example 28

Consider the equation of Example 25(3). We are given a pointed set B with \(p\in B\). Here \(e_0^\ddagger \) is constant with the value \((\varepsilon , p) \in \varSigma ^*\times B\), thus, \(e_1^\ddagger \) takes x and z to \((\sigma , p)\) and y to \((\tau , p)\), using the first letter of the value of \(e^\dag \). Then \(e^\ddag _2\) takes x to \((\sigma \tau , p)\) and y to \((\tau \sigma , p)\), whereas z is taken to \((\sigma \tau , b)\). In general, \(e_k^\ddag \) for \(k\ge 2\) takes x and y to (wp) where w is the prefix of length k of \((\sigma \tau )^\omega \) and \((\tau , \sigma )^\omega \), resp., and it takes z to \((\sigma \tau , b)\).

Notation 29

The free algebra on an object B is denoted by \(\varPhi B\). We show below that this is precisely the initial algebra of \(F_B\):

$$\begin{aligned} \varPhi B = \mu X . FX + B. \end{aligned}$$

The components of the algebra structure \(F(\varPhi B)+ B \rightarrow \varPhi B\) are denoted by \(\varphi _B:F(\varPhi B)\rightarrow \varPhi B\) and \(\eta '_B:B \rightarrow \varPhi B\), resp. The first one makes \(\varPhi B\) an algebra for F.

The algebra \(\varPhi B\) is free on B w.r.t.  \(\eta '_B :B\rightarrow \varPhi B\). Indeed, given an algebra \(\alpha :FA \rightarrow A\) for F together with a morphism \(f :B \rightarrow A\), we obtain an algebra \([\alpha , f] :FA+B \rightarrow A\) for \(F_B\). And a morphism \(h:\varPhi B \rightarrow A\) is a homomorphism for \(F_B\) iff it is a homomorphism for F satisfying \(h \cdot \eta '_B = f\).

We now proceed analogously to Definition 26, defining approximate solutions of equations in \(\varPsi B\). This means that we move from F to \(F_B\). Let \(\partial _k^B :\varPsi B \rightarrow \varPhi B\) be the morphisms of Notation 19 related to \(F_B\). Then every equation morphism \(e:X\rightarrow F_B X +\varPsi B\) yields morphisms

$$\begin{aligned} e_k =(F_B X + \partial _k^B)\cdot e :X \rightarrow FX +\varPhi B \end{aligned}$$

as in (4.1) above.

Definition 30

Let B be a pointed object. For every equation \(e:X\rightarrow FX +\varPsi B\) in the free completely iterative algebra its approximate solutions in the free algebra \(\varPhi B\) are the morphisms \(e_k^\ddagger :X \rightarrow \varPhi B\) defined by induction as follows: first put

$$\begin{aligned} e_0^\ddagger \equiv X \xrightarrow {\ !\ } 1 \xrightarrow {\ p_B\ } F_B0 \xrightarrow {\ w_{1, \omega }\ } \mu F_B= \varPhi B. \end{aligned}$$

Given \(e_k^\ddagger \) define \(e_{k+1}^\ddagger \) as the following composite

(4.4)

We denote by \(m_B :\varPhi B \rightarrow \varPsi B\) the morphism of Proposition 4 related to the functor \(F_B\).

Theorem 31

The solution of every equation \(e:X\rightarrow FX +\varPsi B\) in the free completely iterative algebra \(\varPsi B\) is a limit of the sequence of approximate solutions \(e_k^\ddagger :X \rightarrow \varPhi B\) in the free algebra \(\varPhi B\). More precisely

$$\begin{aligned} U e^\dag =\lim _{k\rightarrow \infty } U(m_B\cdot e_k^\ddagger ). \end{aligned}$$

in the power of the ultrametric space \(U( \varPsi B)\) to UX.

Proof

There is an ordinal i with \(\varPsi B= F_B^i 1\), see Theorem 3 applied to \(F_B\), and for the connecting morphism \(v_{i,k} :F_B^i 1 \rightarrow F_B^k 1 (k < \omega )\) we prove \(v_{i,k} \cdot e^\dag = v_{i,k} \cdot m_B\cdot e_k^\ddagger \). Then the statement follows since \(Ue^\dag \) has distance less than \(2^{-k}\) from \(U(m_B \cdot e^\ddagger _k)\). We proceed by induction, the case \(k=0\) is trivial.

From \(v_{i,k} \cdot m_B \cdot e^\ddagger _k = v_{i,k} \cdot e^\dag \) we derive \(v_{i, k+1} \cdot m_B\cdot e_{k+1}^\ddagger = v_{ i, k+1} \cdot e^\dag \) as follows. By definition of \(e_k\) and \(e_{k}^\ddagger \) the left-hand side is

$$\begin{aligned} v_{i, k+1} \cdot m_B\cdot [\varphi _B, \varPhi B] \cdot (F e_k^\dag + \varPhi B)\cdot (FX + \partial _k^B)\cdot e\,. \end{aligned}$$

Recall from (2.1) that \(m_B \cdot \varphi _B = v_{i+1, i} \cdot F m_B\). Thus,

$$\begin{aligned} v_{i, k+1} \cdot m_B \cdot \varphi _B = v_{i+1, k+1} \cdot F m_B = F( v_{i,k}\cdot m_B)\,. \end{aligned}$$

The left-hand side can thus be simplified to

$$\begin{aligned} \big [ F(v_{i,k} \cdot m_B) , v_{i, k+1} \cdot m_B\big ] \cdot (F e_k^\ddagger +\partial _k^B)\cdot e= \big [ F(v_{i,k} \cdot m_B\cdot e_k^\ddagger ) , v_{i, k+1} \cdot m_B\cdot \partial _k^B\big ]\cdot e. \end{aligned}$$

By induction hypothesis and Lemma 21 this yields

$$\begin{aligned} v_{i,k} \cdot m_B \cdot e^\ddagger _k =\big [ F(v_{i,k}\cdot e^\dag ), v_{i, k+1}\big ] \cdot e. \end{aligned}$$

The right-hand side yields the same result. Indeed, we have

$$\begin{aligned} v_{i, k+1} \cdot e^\dag = v_{i, k+1} \cdot [ \tau _B^{-1}, \varPsi B] \cdot (Fe^\dag + \varPsi B) \cdot e \end{aligned}$$

by definition of \(e^\dag \). Since \(\tau _B^{-1} = v_{i+1, i}\) and \( v_{i+1,k+1} = F v_{i,k}\), we get

$$\begin{aligned} v_{i, k+1} \cdot e^\dag = [F ( v_{i, k} \cdot e^\dag ), v_{i, k+1}] \cdot e. \end{aligned}$$

A completely analogous result holds for solutions in the free iterative algebra on B which we denote by RB. Recall from [7] that the difference between ’iterative’ and ’completely iterative’ is the restriction of the objects X of recursive variables to finitely presentable ones:

Definition 32

(see [7]). An algebra \(\alpha :FA \rightarrow A\) is called iterative if every equation morphism \(e:X\rightarrow FX +A\) wit a finitely presentable object X has a unique solution.

Example 33

(see [7]). (1) In Example 13(3) we have seen that for deterministic automata all formal languages form the terminal coalgebra. Here \(\rho F\) consists of all the regular languages.

(2) The colimit \(\varrho F\) of all coalgebras \(\gamma :C\rightarrow FC\) with C finitely presentable is an iterative algebra. More precisely, denote by \(\gamma ^{\#} :C \rightarrow \varrho F\) the colimit cocone. The unique morphism \(i:\varrho F \rightarrow F(\varrho F)\) making all \(\gamma ^{\#}\) coalgebra homomorphisms is invertible. And the algebra \((\varrho F, i^{-1})\) is iterative. Indeed, this is the initial iterative algebra.

(3) As a concrete example, for the polynomial functor \(H_\varGamma \) we have seen that the terminal coalgebra consists of all \(\varGamma \)-trees. \(\rho H_\varGamma \) is the subcoalgebra of all rational trees, which are those having up to isomorphism only finitely many subtrees. Thus e.g. for the set functor \(FX = \varSigma \times X+B\) we have \(\varrho F\) as the subalgebra of \(\nu F =\varSigma ^\omega + \varSigma ^*\times B\) (see Example 13(2)) consisting of all eventually periodic words in \(\varSigma ^\omega \) (i.e., words of the form \(uv^\omega \)) and all elements of \(\varSigma ^*\times B\).

Notation 34

(1) The initial iterative algebra of \(F_B = F(-) +B\) is denoted by \(RB=\varrho F_B\). Its algebra structure \( F(RB) + B \rightarrow RB\) has components denoted by \(i_B :F(RB) \rightarrow RB\) and \(\hat{\eta } :B\rightarrow RB\).

(2) We denote by \(\bar{m}_B :\varPhi B \rightarrow RB\) the unique algebra homomorphism for \(F_B\) and by \(s_B :RB\rightarrow \varPsi B\) the unique coalgebra homomorphism. Since \(\varPsi B\) is a terminal coalgebra, the homomorphism \(m_B :\varPhi B \rightarrow \varPsi B\) is their composite:

$$\begin{aligned} m_B =s_B \cdot \bar{m}_B. \end{aligned}$$

Since \(m_B\) is monic by Proposition 4, we see that \(\bar{m}_B\) is monic.

For the functor \(H_\varGamma \) of Example 13(5) \(s_B :RB\rightarrow \varPsi B\) is the inclusion of the set of all rational \(\varGamma \)-trees on B.

Proposition 35

([7], 3.9). The algebra \(i_B :F(RB) \rightarrow RB\) is a free iterative algebra for F w.r.t. \(\hat{\eta } :B\rightarrow RB\). If finitely generated objects of coincide with finitely presentable ones, then \(s_B:RB\rightarrow \varPsi B\) is a monomorphism.

Thus, we have subobjects and U(RB) is a canonical ultrametric space, as a subspace of \(U(\varPsi B)\).

Definition 36

Let \(e:X\rightarrow FX +RB\) be an equation in the free iterative algebra with X finitely presentable. We define equations \(e_k\) in the free algebra \(\varPhi B\) as follows:

$$\begin{aligned} e_k \equiv X \xrightarrow {\ e\ } FX + RB \xrightarrow {\ FX + s_B\ } FX + \varPsi B \xrightarrow {\ FX+\partial _k\ } FX + \varPhi B \end{aligned}$$

The approximate solutions \(e_k^\ddagger :X\rightarrow \mu F\) of e are then defined as in Definition 26.

Corollary 37

Suppose that finitely generated and finitely presentable objects coincide. For every equation \(e:X\rightarrow FX + RB\) in the free iterative algebra (X finitely presentable), its solution is a limit of approximate solutions in the free algebra. More precisely

$$\begin{aligned} U e^\dag =\lim _{k\rightarrow \infty } U(\bar{m}_B \cdot e_k^\ddagger ). \end{aligned}$$

in the power of the ultrametric space U(RB) to UX.

This follows from Theorem 31 applied to the equation

$$\begin{aligned} \bar{e} \equiv X \xrightarrow {\ e\ } FX +RB \xrightarrow {\ FX + s_B\ } FX + \varPsi B. \end{aligned}$$

Indeed, on the one hand, we have \(\bar{e}_k^\ddagger = e_k^\ddagger \) for every k (by an easy induction). We verify below that \(\bar{e}^\dag = s_B \cdot e^\dag \). Then the corollary follows from \(m_B = s_B \cdot \bar{m} _B\) since \(s_B\) is monic.

Thus we are to prove that \(s_B\cdot e^\dag \) solves \(\bar{e}\). This is clear from the diagram below

figure f

Indeed, the left-hand square commutes since \(e^\dag \) solves e, the righ-hand part commutes since \(s_B:(RB, i_B^{-1}) \rightarrow (\psi B, \tau _B^{-1})\) is a homomorphism of algebras for \(F_B\). The lower part clearly commutes. Thus, the outward square commutes, and its left-hand vertical arrow is \(\bar{e}\).

5 Conclusions

We have studied colagebras for finitary endofunctors preserving monomorphisms on a wide collection of categories such as sets, vector spaces, posets, boolean algebras etc. Each such endofunctor F carries a canonical ultrametric on the underlying set of the terminal coalgebra \(\nu F\). Moreover, if F is grounded, i.e., F0 has a global element, the underlying set of the initial algebra \(\mu F\) is a dense subspace of that ultrametric space. Given a coalgebra on an object A, we have presented a canonical Cauchy sequence of morphisms from A to \(\mu F\) which converges to the unique coalgebra homomorphism from A to \(\nu F\) in the power of the above ultrametric space \(\nu F\).

For every pointed object B we formed the free iterative algebra RB and the free completely iterative algebra \(\varPsi B\) on B. We derived a canonical ultrametric on the underlying set of each of them. And the free F-algebra \(\varPhi B\) forms a dense subspace of both RB and \(\varPsi B\). Moreover, for every recursive equation e in \(\varPsi B\) we have presented a canonical Cauchy sequence of morphisms into \(\varPhi B\) converging to the unique solution \(e^\dag \) of e in \(\varPsi B\) (again, in the corresponding power of the space \(U(\varPsi B)\)). Analogously for recursive equations with finitely presentable variable-objects in the algebra RB.