数理解析研究所講究録902 巻 1995 年 1-9

1

A final coa..lgebra theorem for concurrent computation$\mathrm{M}\mathrm{a}s$ao MORI*$\mathrm{Y}\mathrm{a}s$uo KAWAHARA*

September 25, 1994

Abstract
This paper presents an elementary and self-contained proof of an existence theorem of final
coalgebras for endofunctors on the category of sets and functions.

1

Introduction

Graphs are fundamental algebraic structures in computer science. Recently labeUed transition systems,
namely, labeUed directed graphs have been considered an appropriate model for concurrent computa.
tions. It is known that graph structures are often represented by coalgebra structures [4, 7, 8]. Manykinds of coalgebras have been considered as objects with circularity in programming semantics, knowledge dynamics and situation theory (Cf. [9]).
1988 Peter Aczel [1] pointed out that the axiomof anti-foundation (AFA) on axiomatic set theory claimms that the universal class ofsets with themembership relation is the final graph structure on classes. Moreover Peter Aczel and Nax Mendler[2] proved a final coalgebra theorem for set-based endofunctors.
fact Michael Barr [3] showed thetheorem of Aczel and Mendler [2] on the existence of final coalgebras for accessibleon thecategory Set of (well-founded) sets and functions.
On the other hand, R. Milner’s CCS is the language for communicating concurrent processes,
which has the equationally axiomatic system. Its semantics is given as labelled transition systems andbisimulation equivalences. The labelled transition systems is expressed as coalgebra structures withrespect to the endofunctor $\Phi X=\wp(A\cross X)$ on Set, for reason of the nondeterministic property ofconcurrency. In general, considering the category of coalgebras and their homomorphisms with respect
to endofunctor on Set, the final coalgebra does not always exist.In the case of powerset functor it iswell-known that nonexistence of the final coalgebra can be proved by the Cantor’s diagonal method.
Rom a point of view for concurrent computation, however, one may restrict the range of transition tosome cardinality.
In this paper we will also discuss with the same
final coalgebra theorem as in [3]. Some detailed
analysis on trees (in other words, the subcoalgebras generated by single elements) and congruences [2](or, bisimulation equivalences) on coalgebras are essential for our results. The discussion of the paper
is elementary and self-contained. The main theorem of the paper is as follows:$\ln$$\mathrm{a}\mathrm{U}$$\ln$endofuncto.rs$\wp$$\mathrm{s}\mathrm{m}\mathrm{a}\mathrm{U}$Theorem 1.1 If an endofunctor : Set
preserves intersections and there is a set $M$ suchthat all trees of -coalgebras are $M$ -bounded, then the category Set
of -coalgebras has a final-coalgebra.
$\Phi$$\Phi$$arrow \mathrm{S}\mathrm{e}\mathrm{t}$$(\Phi)$$\Phi$$\Phi$The paper is as follows. In Section 2 we review the definition of coalgebras for endofunctors on
Set, and only note that the class of all coalgebras defined on subsets of a given set forms a set. In
Section 3 we recaU some basic properties of subcoalgebras for endofunctors on Set. In particular, itturns out that, when the involved endofunctor preserves intersections of subsets, the notion of treesof coalgebras, which are the smallest subcoalgebras containing singleton sets, can be considered. In
Section 4 we discuss congruences on coalgebras initiated by Aczel and Mendler [2]. The notion of*Research Institute of Fundanental lnfonnation Science, Kyushu University 33, Fukuoka 812, Japan.
$\mathrm{E}\mathrm{m}\mathrm{a}\mathrm{i}\mathrm{l}:\{\mathrm{m}\mathrm{a}\mathrm{S}\mathrm{a}, \mathrm{k}\mathrm{a}\mathrm{r}\mathrm{a}\mathrm{h}\mathrm{a}\mathrm{r}\mathrm{a}\}\mathrm{O}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{i}\mathrm{s}.\mathrm{r}\mathrm{y}\mathrm{u}S\mathrm{h}\mathrm{u}-\mathrm{u}.\mathrm{a}\mathrm{c}.\mathrm{j}\mathrm{P}$2congruences is a modification of bisimulation equivalence relations on labelled transition systems due
to D. Park. The aim of this section is to show a usual fact (Cf. [1, theorem 2.4] and [2, Lemma 4.3])
that every coalgebra has the maximum. The fact indicates that the quotient coalgebra of a weak final
coalgebra with respect to the maximum congruence is a final coalgebra (Cf. 4.8). Thus the categoryof coalgebras has a final object if and only if it has a weak final object. In Section 5 we state the main
result of the paper. First we introduce tree congruences on coalgebras using the notion of trees. Then
we show that, whenever all trees of coalgebras are bounded to a set, there is a weak final coalgebra.
Thus by the similar fashion to Aczel and Mendler [2] an existence theorem of final coalgebras is proved.
In section 6 a few examples of coalgebras which satisfy the main theorem are listed.

Coalgebras

2This section defines the notion of coalgebras for endofunctors on the category Set of sets and functions.
denote an endofunctor throughout the paper. A -coalgebra $(A, a)$ is a pair of a:Let
set and a function : $Aarrow\Phi A$ . A homomorphism $f$ : $(A, a)arrow(B,b)$ of a -coalgebra $(A, a)$ intoanother -coalgebra $(B, b)$ is a function $f$ : $Aarrow B$ rendering the following square commutative:$\Phi$$\Phi$$\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$$\Phi$$A$$a$$\Phi$$\underline{f}$$B\downarrow b$$a\downarrow A$$\Phi A$$\Phi B$$rightarrow$.

$\Phi(f)$All -coalgebras and all their homomorphisms form a category Set
of -coalgebras.
$\Phi$$(\Phi)$which is called the category$\Phi$

Proposition 2.1 The category Set$(\Phi)$of$\Phi$-coalgebrus has all small colimits.

. First
Proof. It suffices to prove the existence of coequalizers and coproducts because ofSet
categorytheAs-coalgebras.
homomorphismsof$f,$parallel$(A,a)arrow(B,
b)$
pair
of
be
a
:
let
has all small colimits there is a coequalizer : $Barrow Q$ of a pair of functions and in Set. Noticingthat $\Phi(e)bf=\Phi(e)\Phi(f)a=\Phi(e)\Phi(g)a=\Phi(e)bg$ there is a unique function : $Qarrow\Phi Q$ such that: $(B, b)arrow(Q, q)$ is a coequalizer of and$qe=\Phi(e)b$ . It is an elementary exercise to show thatis a family of -coalgebras indexed by a set A. Let bein Set . Next suppose thatA.
the inclusion of coproducts for:anda coproduct (or disjoint union) of
Define a function : $Aarrow\Phi A$ to be a unique function such that a square$[6, \mathrm{V}2.1]$$\Phi$

$g$

$f$

$e$

$g$

$q$

$f$

$e$

$(\Phi)$$i_{\lambda}$$\{A_{\lambda}\}_{\lambda\in \mathrm{A}}$

$g$

$A$

$\Phi$$\{(A_{\lambda}, a_{\lambda})\}_{\lambda\epsilon}\mathrm{A}$$\lambda\in$$A_{\lambda}arrow A$$a$$\underline{*\cdot \mathrm{x}}$$A\downarrow a$$a_{\lambda}\downarrow A_{\lambda}$$\Phi A_{\lambda}$–$\Phi A$$\Phi(i_{\lambda})$commutes for everyof$\lambda\in$

A. It is also a routine work to show that a -coalgebra $(A, a)$ is a coproduct$\Phi$$\{(A_{\lambda}, a_{\lambda})\}_{\lambda}\in\Lambda\cdot\square$The$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{w}\mathrm{i}\mathrm{n}\mathrm{g}$Lemma 2.2 If
injection.

$f$lemma is a basic fact of functors on Set.

:

$Xarrow \mathrm{Y}$is an injection and $Xisa/$ nonempty set, then$\Phi(f)$:$\Phi Xarrow\Phi \mathrm{Y}$is an

by $g(y)=x\mathrm{i}\mathrm{f}y=f(x)$ for $x\in X$ and $g(y)=x_{0}$ose $x_{0}\in X$ and define a function
Proof.
, whichandif there is no $x\in X$ such that $y=f(x)$ . Then it is clear thatis injective.
shows that$g:\mathrm{Y}arrow X$$\mathrm{C}\mathrm{h}o$$gf=\mathrm{i}\mathrm{d}_{X}$$\Phi(g)\Phi(f)=\mathrm{i}\mathrm{d}_{\Phi X}$$\square$$\Phi(f):\Phi Xarrow\Phi \mathrm{Y}$-coalgebras $(A, a)$ such that
Given a set $M$ the class of$M(\Phi)$. The following proposition points out thatby Set$\mathrm{a}\mathrm{U}\Phi$$A$

is a nonempty subset of $M$ is denoted
constitutes a set.

$\mathrm{S}\mathrm{e}\mathrm{t}_{M}(\Phi)$

3

Proposition 2.3 For every set $M$ the class$\mathrm{S}\mathrm{e}\mathrm{t}_{M}(\Phi)$

is a subset of $\wp(M)\cross\wp(M\cross\Phi M)$ , that is,

Set $M(\Phi)\subseteq\wp(M)\cross\wp(M\cross\Phi M)$ .

and $i:Aarrow M$ the inclusion. Then it is immediate
Proof. Let $(A, a)$ be a -coalgebras inthat $A\in\wp(M)$ and $a\in\wp(M\cross\Phi M)$ since a function : $Aarrow\Phi A$ can be identified with a subset$\text{\^{a}}=\{(x, \Phi(i)a(X))|x\in A\}$ ofby the last lemma.
$\Phi$$\mathrm{S}\mathrm{e}\mathrm{t}_{M}(\Phi)$$a$$M\mathrm{x}\Phi M$$\square$

In a category of coalgebras a final coalgebra is a coalgebra such that there is a unique homomorphismfrom each coalgebra into it. A weak final coalgebra is a coalgebra such that there is at least one
homomorphism from each coalgebra into it. The purpose of the paper is to show an existence theoremof final coalgebras for endofunctors on Set.

Subcoalgebras

3This section is devoted to state the notion and the basic properties of subcoalgebras. Trees, that is,
the smallest subcoalgebras containing singleton sets, play an important role to prove the main theoremof the paper.
Let $(A, a)$ be a -coalgebra. A subset $H$ of is called a subcoalgebra of $(A, a)$ if there is a function: $Harrow\Phi H$ which makes the inclusion $i:Harrow A$ a homomorphism : $(H, h)arrow(A, a)$ of -coalgebras.
(By the definition the empty set is always a subcoalgebra.)$A$$\Phi$$h$$i$$\Phi$$\emptyset$

Lemma 3.1 Let $(A, a)$ be a -coalgebra. A subset $H$ of is a subcoalgebra of $(A, a)$ if and only iffor
each $x\in H$ there is $z\in\Phi H$ such that $a(x)=\Phi(i)(z)$ , where $i:Harrow A$ is the inclusion of $H$ into .
$A$$\Phi$$A$

Proof. Only if part is trivial from the definition of subcoalgebras. We have to show its converse.
the assertion is
Assume that for each $x\in H$ there is $z\in\Phi H$ such that $a(x)=\Phi(i)(z)$ . Whenin the case. So we can assume that $H$ is nonempty. A function $h:Harrow\Phi H$ can be defined by:$H=\emptyset$

For each $x\in H$ : $h(x)=z$ if $a(x)=\Phi(i)(z)$ for some $z\in\Phi H$ .

Since$\Phi(i)$is injective by 2.2$h$is uniquely defined and $\Phi(i)h=ai$ is immediate.

$\square$

Let $(A, a)$ be a -coalgebra and $H$ a subcoalgebra of $(A, a)$ . Then it is easy to see that a subset
of is a sub coalgebra of $H$ if and only if is a subcoalgebra of $(A, a)$ .
$\Phi$

$H$

$S$

$S$

Proposition 3.2 Let$f$: $(A, a)arrow(B, b)$ be a homomorphism of -coalgebras.
$\Phi$(a) If $H$ is a subcoalgebra of $(A, a)$ , then $fH=\{f(x)|x\in H\}$ is a subcoalgebra of $(B, b)$ .

(b) If $H$ is a subcoalgebra of $(A, a)$ and $f$ : $(A, a)arrow(B, b)$ is an injective homomorp hism, then $fH$
is isomorphic to $H$ as -coalgebras.
$\Phi$

Proof. (a) Let : $Harrow A$ and : $fHarrow B$ be inclusions. A function $f’$ : $Harrow fH$ is definedby $f’(x)=f(x)$ for each $x\in H$ . Then $fi=jf’$ . Hence for $x\in H$ there is $z\in\Phi H$ such that$a(x)=\Phi(i)(z)$ and so $b(f(x))=\Phi(f)a(x)=\Phi(f)\Phi(i)(Z)=\Phi(j)\Phi(f’)(z)$ . This means that for each$y\in fH$ there is $w\in\Phi(fH)$ such that $b(y)=\Phi(j)(w)$ , which completes the proof. (b) It suffices to seethat a bijective homomorphism of -coalgebras is an isomorphism. Assume that : $(A, a)arrow(B, b)$
is a bijective homomorphism and let : $Barrow A$ be the inverse set function of $f$ . Thenandand $\Phi(g)b=\Phi(g)bfg=\Phi(g)\Phi(f)ag=ag$ by $bf=\Phi(f)a$ .
$j$$\dot{i}$$\Phi$$f$$gf=\mathrm{i}\mathrm{d}_{A}$$g$$\square$$fg=\mathrm{i}\mathrm{d}_{B}$An endofunctor: Setfamiliesof subsets of a set$\Phi$$arrow \mathrm{S}\mathrm{e}\mathrm{t}$$\{H_{\lambda}\}_{\lambda}$$A$

preserves intersections if
and:, where$i_{\lambda}$$H_{\lambda}arrow A$

Lemma 3.3 Let $(A, a)$ be a -coalgebra. If :familyof subcoalgebras of $(A, a)$ its intersection$\Phi$$\{H_{\lambda}\}_{\lambda}$$\Phi$$\Phi(i)\Phi(\cap\lambda H\lambda)=\bigcap_{\lambda}\Phi(i_{\lambda})\Phi H_{\lambda}$$i: \bigcap_{\lambda}H_{\lambda}arrow A$$\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$for allare inclusions, respectively.

preserves intersections, then for every
is a subcoalgebrvt of $(A, a)$ .

$H= \bigcap_{\lambda}H_{\lambda}$

4

Proof. Let$i$be inclusions, respectively. We have to show that for each:such that $a(x)=\Phi(i)(z)$ . Assume that $x\in H$ . Then for each there isand there is $z\in\Phi H$. Hence: $Harrow A$ and$x\in H$ there is $z\in\Phi H$$H_{\lambda}arrow A$$i_{\lambda}$$\lambda$such thatsuch that $a(x)=\Phi(i)(z)$ .

$a(x) \in\bigcap_{\lambda}\Phi(i_{\lambda})\Phi H_{\lambda}=\Phi(i)\Phi H$$a(x)=\Phi(i_{\lambda})(z_{\lambda})$$z_{\lambda}\in\Phi H_{\lambda}$$\square$be an endofunctor preserving intersections. For a -coalgebra $(A, a)$ and $x\in A$
Let :consider the family of all subcoalgebras of $(A, a)$ containing . Then by the last lemma its intersection
containing , which is called the tree of $(A,a)$ with a root and denotedis the smallest
by.
$\Phi$$\Phi$$\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$

$x$

$x$

$x$

$\mathrm{S}\mathrm{u}\mathrm{b}_{\dot{\mathrm{C}}}\mathrm{o}\mathrm{a}\dot{\mathrm{e}}\mathrm{b}\mathrm{r}\mathrm{a}$$[x]_{A}$

Proposition 3.4 Let$\Phi$:$\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$(a) If $H$ is a subcoalgebm of a$\Phi$

be an endofunctor preserving intersections.

-coalgebra $(A, a)$ , then $[x]_{H}=[x]_{A}$ for $x\in H$ .

(b) If $f$ : $(A, a)arrow(B, b)$ is an injective homomorphism of -coalgebras, then $f[x]_{A}=[f(x)]_{B}$ for$\Phi$$x\in A$.

.
is a subcoalgebra of $(A, a)$ and so. By
Proof. (a) First note that$H$ since
.
.
.
Hence
Set
of
$K=fA$
subcoalgebra
is a
On the other hand$f[x]_{A}=[f(x)]_{K}=[f(x)]_{B}$
$(A,
a)$
$K$
$(B,
b)$
by
(a).
to
.
Then
isomorphic
andofis a subcoalgebra
By 3.2This completes the proof.
$[x]_{A}\subseteq[x]_{H}$$3.2(\mathrm{a})[x]_{H}$$[x]_{H}\subseteq H$$[x]_{H}\subseteq[x]_{A}$$[x]_{A}\subseteq H$$[x]_{A}$$(\mathrm{b})$$\square$Congruences

4

This section discusses the notion of congruences on coalgebras initiated by Aczel and Mendler [2].
The notion of congruences is a modification of bisimulation equivalence relations on labelled transition
systems. Clearly congruences generalize bisimulations and correspond to quotient coalgebras. The aimof this section is to show a usual fact (Cf. [1, theorem 2.4] and [2, Lemma 4.3]) that every coalgebra
has the maximum congruence.
A (binary) relation on a set is a subset of $A\cross A$ . Hence boolean operations such as union andintersections can be applied to relations. An equivalence relation on a set is a relation on suchthat $(x,x)\in\theta$ (reflexive), $(x, y)\in\theta\Rightarrow(y, x)\in\theta$ (symmetric) and $(x, y)\in\theta$ A $(y, z)\in\theta\Rightarrow(x, z)\in\theta$(the diagonal set of(transitive) for all $x,$ $y,$ $z\in A$ . Note that the identity relation$A)$ is an equivalence relation on any set
is a surjection
on
there
equivalenceanrelation. Given$(x,y)\in\theta$$e(x)=e(y)$
.
call
such
a surjection
only
if andif
Weof onto a (quotient) set such that$e:Aarrow Q$ a quotient function with respect to . Since a quotient function is unique up to isomorphisms,
is uniquely defined as follows:onan equivalence relation
$A$

$A$

$A$

$\theta$$\mathrm{i}\mathrm{d}_{A}=\{(x, x)|X\in A\}$

$A$

$A$

$\theta$$A$$Q$$\theta$$\Phi A$$\Phi(\theta)$$(u, v)\in\Phi(\theta)\Leftrightarrow\Phi(e)(u)=\Phi(e)(v)$Moreover let $f$ : $A_{0}arrow A$ be a function. An equivalence relation$(u,v)\in\theta_{f}\Leftrightarrow(f(u), f(v))\in\theta$

Proposition 4.1 Let(a) If(b)$\theta\subseteq\theta’$$I\overline{f}\theta\subseteq\theta’$, then, then$f$: $A_{0}arrow A$ be a function and$\theta_{f}\subseteq\theta_{f}’$$\theta_{f}$.

$\theta,$$\theta’$on.
$A_{0}$

is a relation onequivalence relations on$A$$A_{0}$

such that.

.

$\Phi(\theta)\subseteq\Phi(\theta’)$.

Proof. (a) It is trivial from definition. (b) Let $e:Aarrow Q$ and : $Aarrow Q’$ be quotient functions withrespect to and , respectively. Then there is a function $k:Qarrow Q’$ such that $ke=e’$ . Hence$e’$$\theta$$\theta’$$(u, v)\in\Phi(\theta)$$\Rightarrow$$\Phi(e)(u)=\Phi(e)(v)$$\Rightarrow$$\Phi(e’)(u)=\Phi(k)\Phi(e)(u)=\Phi(k)\Phi(e)(v)=\Phi(e’)(v)$$\Rightarrow$$(u, v)\in\Phi(\theta’)$.

$\square$5

Definition 4.2 Let $(A, a)$ be a -coalgebra.
$\Phi$(a) An equivalence relation

on a set$\theta$$A$

is a congruence on $(A,a)$ if$\theta\subseteq\Phi(\theta)_{a}$.

(b) A relation 9 on $A$ is a pre-congruence on $(A, a)$ if the equivalence relation
generated by, reflexive, symmetric and transitive closure) is a congruence on $(A,a)$ , that is,$\theta^{*}$$is$$of\theta$

The condition
implies $(a(x), a(y))\in\Phi(\theta)$ .

$\theta\subseteq\Phi(\theta)_{a}$

(that

.

in the above definition (a) is equivalent to a condition that $(x,y)\in\theta$

Proposition A3 If : $(A, a)arrow(B, b)$ is a homomorphism ofrelation id
is a congruence on $(A, a)$ .
$f$$\Phi$-coalgebras, then an equivalence$B)_{f}$

$($

. Let

$\mathrm{P}\mathrm{r}\infty \mathrm{f}$$\theta$$\theta\subseteq\Phi(\theta^{*})_{a}$$e$: $Aarrow Q$ be a quotient function with respect to. Then there is a unique injection. Note that $\Phi(m)$ is injective by 3.1. Hence$(\mathrm{i}\mathrm{d}_{B})_{f}$$m:Qarrow B$ such that $f=me$$(x, y)\in(\mathrm{i}\mathrm{d}_{B})_{f}$$\Rightarrow$$f(x)=f(y)$$\Rightarrow$$\Phi(m)\Phi(e)a(x)=\Phi(f)a(x)=bf(x)=bf(y)=\Phi(f)a(y)=\Phi(m)\Phi(e)a(y)$$\Rightarrow$$\Phi(e)a(X)=\Phi(e)a(y)$$\Rightarrow$$(x, y)\in\Phi(\mathrm{i}\mathrm{d}B)J)_{a}$.

$\square$Proposition 4.4 Given a congruence on $(A,a)$ and a quotient function $e:Aarrow Q$ with respect tothere is a unique function $q:Qarrow\Phi Q$ such that $e:(A, a)arrow(Q,q)$ is a homomorphism-coalgebrus.
$\theta$$\theta$$of\Phi$

Proof. A function$q$: $Qarrow\Phi Q$ can be defined as follows:
For $w\in Q$ : $q(w)=\Phi(e)a(x)$ if $w=e(x)$ .

This definition is-defined, since if $e(x)=e(y)$ then $(x, y)\in\theta$ and so $(a(x), a(y))\in\Phi(\theta)$ by. It is trivial that $qe=\Phi(e)a$ . The uniqueness offrom the surjectivity of . This
completes the proof.
$\mathrm{w}\mathrm{e}\mathrm{U}$$\theta\subseteq\Phi(\theta)_{a}$$q\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{w}\mathrm{s}$$e$$\square$

The -coalgebra $(Q, q)$ constructed in the above proposition is called a quotient$(A, a)$ with respect to a congruenceand denoted by.
$\Phi$(a) IfLemma 4.5(b) If.

$\mathrm{P}\mathrm{r}\infty \mathrm{f}$$\theta$$(\mathrm{a})$and$\theta$

is a pre-congruence on $(A, a)$ , thenare pre-congruences on $(A, a)$ , then$\mu$Assume that.
By 4.1 we have$\theta^{*}\subseteq\Phi(\theta^{*})_{a}$$\theta\subseteq\Phi(\theta^{*})_{a}$$\Phi$-coalgebra of$(A/\theta, a/\theta)$$\theta$. As$\Phi(\theta^{*})_{a}$$\theta\cup\mu$$\theta^{*}$

is a congmence on $(A, a)$ .

is a pre-congruence on $(A, a)$ .

is an equivalence relation on$A$

it simply follows that$(\mathrm{b})$$\theta\cup\mu\subseteq\Phi(\theta^{*})_{a}\cup\Phi(\mu^{*})a\subseteq\Phi((\theta\cup\mu)*)_{a}$Theorem 4.6 Every
Proof. Define a$\Phi$.

$\square$-coalgebra $(A, a)$ has the maximum $cong_{\Gamma u}ence---A$ .

$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}-_{A}--$

on

$A$

to be a union (supremum) of all pre-congruences on $(A, a)$ , that is,$—A=\cup\theta\theta\in S$ ’

where

$S$

is the set of all pre-congruences on $(A, a)$ . Then$–_{A}-= \bigcup_{\theta\epsilon s}\theta\subseteq\cup\Phi(\theta^{*})_{a}\subseteq\Phi(_{-_{A}}--*)_{a}\theta\in s$since by 4.1
Finally it suffices to prove$\Phi(\theta^{*})\subseteq\Phi(_{-_{A}}^{-*}-)$

for each. This shows thatis an equivalence relation on$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}_{-}^{-_{A}}-$$\theta\in S$

is the maximum pre-congruence.
. As the identity relation
on

$—A$
$A$

$\mathrm{i}\mathrm{d}_{A}$

$A$

6

(reflexive). Assume that $(x, y)\in---A$ . Then there is a preis a congruence it is clear that$(y,x)\in\theta^{*}$$(x,y)\in\theta$. But by the last lemma is a (pre-)congruencesoandcongruence such that$(x, y)\in---A$ and $(y, z)\in---A$ . Thenthat
Finally
assume$(y,x)\in---$(symmetric).
and hence
.
Hence
some
for
and
$\mathrm{i}\mathrm{d}_{A}\subseteq---A$$\theta^{*}$$\theta$$(x, y)\in\theta_{0}$$(y, z)\in\theta_{1}$$\theta_{0},$$\theta_{1}\in S$

and$(x, y)\in\theta 0\subseteq(\theta 0\cup\theta 1)^{*}$$(y, z)\in\theta 1\subseteq(\theta_{0}\cup\theta_{1})*$

an equivalence relation. As
and soby the last lemma we have $(x, z)\in---A$ (transitive).
$(x, z)\in(\theta_{0}\mathrm{U}\theta_{1})*\mathrm{b}\mathrm{e}\mathrm{C}\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{e}(\theta 0\mathrm{U}\theta 1)*\mathrm{i}\mathrm{s}$$(\theta_{01}\mathrm{U}\theta)*\mathrm{i}\mathrm{s}$a (pre-)congruence$\square$

Theorem 4.7 For every
into $(A/—A)q/—A)$ .

$\Phi$-coalgebra $(A, a)$ there is at most one homomorphism from any$\Phi$-coalgebra: $Aarrow A/—A$ be a quotient function with respect to $—A$ . Assume that $f,g$ : $(B, b)arrow$( $A/_{-}^{-_{A},/)}-a---A$ are homomorphisms. Construct a coequalizer : $(A/_{-}^{-}-_{A}, a/---A)arrow(R, r)$ of and(which does exist by 2.1). Then for any $u\in B$ there is $x,$ $y\in A$ such that $f(u)=e(x)$ and $g(u)=e(y)$ .
by 4.3 it. As
Moreover de $(x)=df(u)=dg(u)=de(y)$ , which means that
follows that $(x, y)\in---A$ and $e(x)=e(y)$ . Hence $f(u)=e(x)=e(y)=g(u)$ , which proves that $f=g$ .

Proof. Let

$e$

$f$

$d$

$(x, y)\in(\mathrm{i}\mathrm{d}_{R})_{de}$$g$$(\mathrm{i}\mathrm{d}_{R})_{de}\subseteq---A$$\square$

The following corollary is an immediate consequence from the last theorem.
Corollary 4.8 If the category Set
coalgebra.

$(\Phi)$of$\Phi$-coalgebras has a weak final coalgebra, then it has a final$\square$5

Main Theorem

This section proves the main theorem of the paper. To treat freely with trees of coalgebras we assume
preserves intersections throughout this section.
that an endofunctor :First we introduce tree congruences on coalgebras using the notion of trees. Then we show that,whenever all trees of coalgebras are bounded to a set, there is a weak final coalgebra. Thus by thesimilar fashion to Aczel and Mendler [2] an existence theorem of final coalgebras is proved.
on as follows: $(x, y)\in\xi_{A}$ for $x,$ $y\in A$ if and only
Let $(A, a)$ be a -coalgebra. Define a relation$[x]_{A}arrow[y]_{A}$$f$: $Aarrow A$
such that $f(x)=y$ . Obviously-coalgebrasof
if there is an isomorphism :$(A,a)$
followingbyofthevirtuecongruence
on
tree
the
we
call
is an equivalence relation on , which$\Phi$$\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$$\xi_{A}$$\Phi$$A$$\xi_{A}$$\Phi$$A$

Theorem 5.1 For each$\Phi$-coalgebra $(A, a)$ the equivalence relation$\xi_{A}$on$A$

is a congruence on $(A, a)$ .

Proof. Let : $Aarrow Q$ be a quotient function with respect to . It suffices to show that $(x, y)\in\xi_{A}$implies $\Phi(e)a(x)=\Phi(e)a(y)$ . Assume that $(x, y)\in\xi_{A}$ . Let $i:[x]_{A}arrow A$ and $j:[y]_{A}arrow A$ be inclusions,
respectively. There is an isomorphism $k:[x]_{A}arrow[y]_{A}$ with $k(x)=y$ .
$\xi_{A}$$e$$arrow jk$$\underline{\dot{i}}$$A$$[x]_{A}$$\downarrow a$$\downarrow h_{x}$$a\downarrow$$\Phi A$$A$–

$arrow$$\Phi[x]_{A}$$\Phi A$.

$\Phi(jk)$$\Phi(\dot{*})$First note that $ei=ejk$ . For each $z\in[x]_{A}(=H)$ we have$[i(z)]_{A}$$=$$[z]_{H}$$(3.4(\mathrm{a}))$$\cong$$jk[_{Z]_{H}}$$(3.2(\mathrm{b}))$$=$$\mathrm{b}k(Z)]_{A’}$$(3.4(\mathrm{b}))$,which indicates that $(i(Z))jk(z))\in\xi_{A}$ and so $ei(z)=ejk(z)$ . Therefore it follows that$\Phi(e)a(x)$The proof is completed.

$\square$$=$$\Phi(e)ai(x)$$=$$\Phi(e)\Phi(i)hx(X)$( is a homomorphism.)$=$$\Phi(e)\Phi(jk)(x)$$(ei=ejk)$$=$$\Phi(e)ajk(x)$$=$$\Phi(e)a(y)$$i$($jk$ is a homomorphism.)$(y=jk(x))$ .

7

Theorem 5.2 If every tree of a -coalgebra $(A, a)$ is isomorphic to a subcoalgebra of a$(T, t)$ , then there is at least one homomorphism $f$ : $(A, a)arrow(T/\xi_{T}, t/\xi_{T})$ .
$\Phi$$\Phi$-coalgebra

Proof. Let : $(T, t)arrow(T/\xi_{T}, t/\xi\tau)$ be a quotient homomorphism by . For every $x\in A$ there isbyan injective homomorphism : $[x]_{A}arrow(T,t)$ by the assumption. Define a function :$f(x)=ek(x)$ .
$\xi_{\mathcal{T}}$

$e$

$k$

$f$

$arrow e$$\underline{k}$$.\underline{i}$$[x_{1^{]_{A}}h_{x}}$$a\downarrow A$$\Phi(A)$$T/\xi_{T}\downarrow t/\xi_{T}$$T\downarrow t$$\Phi T$$\Phi[x]_{A}$$\Phi(T/\xi\tau)$$\overline{\Phi(e)}$$\overline{\Phi(k)}$$\overline{\Phi(i)}$$Aarrow T/\xi_{\mathrm{T}}$.

Note that this definition of $f(x)$ is independent on the choice of an injective homomorphism . (Letand
it is trivial that
: $[x]_{A}arrow T$ be another injective homomorphism. Then by$[k(X)]_{R}\cong[x]_{A}\cong[k’(x)]_{R}$ . Hence $ek(x)=ek’(x).)$ Next we show that $fi=ek$ . For each $z\in[x]_{A}$ thecomposite $mk$ of the inclusion $m$ : $[z]_{A}arrow[x]_{A}$ followed by is an injective homomorphism into andso $f(z)=ekm(z)$ . Hence $fi(z)=f(z)=ekm(z)=ek(z)$ , which shows that $fi=ek$ . Finally we showthat $f$ : $Aarrow T/\xi_{T}$ is a homomorphism, that is, $a\Phi(f)=f(t/\xi_{T})$ . But we have
$k$

$k’$

$3.4(\mathrm{b})$$3.2(\mathrm{b})$

$T$

$k$

$\Phi(f)a(x)$$=$$\Phi(f)a\dot{i}(X)$$=$$\Phi(i)\Phi(f)h_{x}(X)$( is a homomorphism.)$=$$\Phi(ek)h_{x}(x)$$(fi=ek)$$=$$(t/\xi_{T})ek(x)$$=$$(t/\xi\tau)f(X)$For a set $M$ the coproduct of all coalgebras in$i$( $ek$ is a homomorphism.)$(f(x)=ek(x))$ .
$\square$$\mathrm{S}\mathrm{e}\mathrm{t}_{M}(\Phi)$

will be denoted by $(T_{M}, t_{M})$ , that is,$(T_{M}, t_{M})=(A,a) \in \mathrm{S}\prod_{\Phi \mathrm{e}\mathrm{t}M()}(A, a)$.
: $(A, a)arrow(T_{M}, t_{M})$ denotes the inclusion of the coproduct for a -coalgebraandA -coalgebra $(A, a)$ is called $M$ -bounded if there is an injection of into $M$ . It is obvious that for
an $M$ -bounded -coalgebra $(A, a)$ there is an injective homomorphism : $(A, a)arrow(T_{M}, t_{M})$ , that is,card $(A)\leq card(M)$ . Hence we have the following$\Phi$$i_{A}$$(A, a)\in \mathrm{S}\mathrm{e}\mathrm{t}_{M()}\Phi$$A$$\Phi$$k$$\Phi$-coalgebras are $M$ -bounded for a set $M$ , then for each -coalgebra $(A, a)$there is at least one homomorphism : $(A, a)arrow(\tau_{M}/\xi_{T_{M}},tM/\epsilon\tau M),that\square$ is, the quotient coalgebraof $(T_{M}, t_{M})$ is a weak final coalgebm in Set .
$\mathrm{C}_{\mathrm{o}\mathrm{r}}\mathrm{o}\mathrm{u}\mathrm{a}\mathrm{r}\mathrm{y}5.3$

If all trees of$\Phi$$\Phi$$f$$(\Phi)$$(T_{M}/\xi_{T_{M}}, t_{M}/\xi_{T_{M}})$

In a category of coalgebras a final coalgebra is a coalgebra such that there is a unique homomorphismfrom each coalgebra into it. Combining with 4.8 and the last corollary we have the following

Theorem 5.4 If there is a set $M$ such that all
Setof -coalgebras has a final coalgebm.
$(\Phi)$6$tree\square s$of$\Phi$-coalgebras are $M$ -bounded, then the category$\Phi$

ExamplesThis section illustrates a few examples of coalgebras which satisfy the main theorem 5.4 and so havea final coalgebra.
Let $M$ be a set. The $M$-bounded power set functor$\wp_{M}(A)=${$S|S\subseteq A$$\wp_{M}$:$\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$is a functor such that

A card$(S)\leq card(M)$ }for all sets , where card $(M)$ denotes the cardinality of $M$ . For a set $M$ n-th productis defined by$M^{0}=1$ (a singleton set) and $M^{n+1}=M^{n}\cross M$ for $n\geq 0$ . The setof all finite strings of elements
in $M$ is formally defined by $M^{*}= \bigcup_{n\geq}0M^{n}$ .
$A$$M^{n}$$M^{*}$

8

Theorem 6.1 $Ail$ trees of$\wp_{M}$-coalgebras are$M^{*}$-bounded.

by $[x]_{0}=\{x\}$ andof-coalgebra and $x\in A$ . Define a subset
Proof. Let $(A, a)$ be a$([x]_{n+1})\leq
card([x]n\crossM)$ it$[x]_{n+1}= \bigcup_{y\in[x]_{*}}a(y)$ for $n\geq 0$ . Set. From card
that
card$([X] \infty)\leq card(\bigcup_{n\geq}0M^{n})=ca\gamma d(M*)$.
$[x]_{n}$$\wp_{M}$$A$$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{W}\mathrm{s}$$[x]_{\infty}= \bigcup_{n\geq 0}[X]n$for all $n\geq 0$ and so
Finally it suffices to see that $[x]_{A}=[x]_{\infty}$ . By induction we have
. Finally notethenand if. Because(i.e. $a(y)\in\wp u([X]\infty)$ ) for $y\in[x]_{n}$ .
is a subcoalgebra of $(A, a)$ since
that
.
Hence
$[x]_{n}\subseteq[x]_{A}$$[x]_{n}\subseteq[x]_{A}$$[x]_{0}\subseteq[x]_{A}$$[x]_{\infty}\subseteq[x]_{A}$$[x]_{n+1}= \bigcup_{y\in}[x]_{\mathrm{r}}a(y)\subseteq[x]_{A}$$a(y)\subseteq[x]_{n+1}\subseteq[x]_{\infty}$$[x]_{\infty}$$[x]_{A}\subseteq[x]_{\infty}$$\square$Combining with 5.4 and the last theorem we have theCorollary 6.2 The category Set$(\wp_{X})$$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{w}\mathrm{i}\mathrm{n}\mathrm{g}$has a final coalgebm.

Note that $\wp_{1}(X)=1+X$ for a singleton set$1(=\{\mathit{0}\})$.

and be endofunctors on Set. A natural tranLet
injection $f$ : $Xarrow Y$ a naturality square$\Psi$$\Phi$$\square$$\mathrm{S}\mathrm{f}_{0}\mathrm{r}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\sim \mathrm{n}\nu$:$\Psiarrow\Phi$is strict if for every$.$$\Psi(f)$$\Psi X$

$arrow$$\nu_{X}\downarrow\Phi X$$\Psi \mathrm{Y}$$\Phi \mathrm{Y}\downarrow\nu_{Y}$$\overline{\Phi(f)}$is a pullback.
Proposition 6.3 Let :If preserves intersections and$\nu$$\Psiarrow\Phi$$\Phi$

Proof. It$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{w}\mathrm{s}$

$\nu$

and
be a natuml transfomation between endofunctors
also preserves intersections.
:is strict, then$\Psi$$\Psiarrow\Phi$from easy diagram chasing.

$\Phi$

on Set.

$\Psi$$\square$be a strict natuml transformation and $(B, b)$ a -coalgebra. Then a subset
Lemma 6.4 Let :$B$ is a subcoalgebm$H$$(B,of b)$ if and only if $H$ is a subcoalgebm of a -coalgebm $(B, \nu_{B}b)$ .
of$\Psiarrow\Phi$$\nu$$\Psi$$\Phi$

Proof. Let$\dot{i}$: $Harrow B$ be the inclusion and consider a diagram$\dot{H}$:$arrow$$B$$\downarrow b$$\Psi(:)$$\Psi H$$rightarrow$$\Psi B$$\downarrow\nu_{B}$$\nu_{H}\downarrow$$\Phi B$$\Phi H$$\overline{\Phi(\dot{*})}$,

in which the square is a puUback by the strictness of . Then it is trivial that a function : $Harrow\Psi H$
with $bi=\Psi(i)h$ bijectively corresponds to a function : $Harrow\Phi H$ with $\nu_{B}bi=\Phi(i)h’$ . This completes
the proof.
$h$

$\nu$

$h’$

$\square$

As a direct result from the above lemma we have the following
Corollary 6.5 Let:
natural transfomation.
$\Phi,$(a) If $(B, b)$ is a$\Psi$$\Psi$$\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$be endofunctors preserving intersections and

$\nu$

:

$\Psiarrow\Phi$a strict-coalgebm, then $[x]_{(B,b})=[x]_{(b}B,\nu_{B})$ for all $x\in B$ .

(b) If all trees of -coalgebras are $M$ -bounded for a set $M$ , then so are those of -coalgebms.
$\Phi$

By 6.1 and 5.4 we have the following$\Psi$$\square$9

Example 6.6 All categories of coalgebras for the following endofiunctors have final coalgebm.

(a) The finite powerset functor(b) The Kleene fisnctor $X^{*}:$(c) A polynomial functor
are fixed sets).

(d) A functor
(e)

$A$

fimctor$\wp \mathrm{f}\mathrm{i}\mathrm{n}$:$\mathrm{s}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$$\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$.

.
(where$\Phi X=A_{0}+A_{1}\cross X+\cdots+A_{n}\cross X^{n}+\cdots.‘ \mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$$A_{0},$ $A_{1},$$\cdots$.

$\wp_{M}(A\cross X):\mathrm{S}\mathrm{e}\mathrm{t}arrow \mathrm{S}\mathrm{e}\mathrm{t}$$(A\cross X)^{*}$: Set–Set

Proof. (a) Let denote the set of all natural numbers. A natural inclusion
is a strict
natural transformation. (b) A natural transformation
assigningtois strict. (c) A natural transformation
assigningtois strict. (d) A natural transformation $\wp u(A\cross X)arrow$$\wp M(X)$ induced by the projection $A\cross Xarrow X$ is strict. (e) A natural transformation $(A\cross X)^{*}arrow X^{*}$
assigningtois strict.
$\omega$$\wp \mathrm{f}\mathrm{l}\mathrm{n}(X)arrow\wp_{w}(X)$$X^{*}arrow\wp_{\omega}(X)$$\sigma_{1}\sigma_{2}\cdots\sigma_{k}\in X^{*}$$\wp_{\omega}(X)$$\Phi Xarrow\wp_{\omega}(X)$$\{\sigma_{1},$$\sigma_{2},$$\cdots,$$\sigma_{k}1\in\wp_{v}‘(X)$$\{\sigma_{1}, \sigma_{2}, \cdots, \sigma_{k}\}\in$$(a, \sigma_{1}\sigma_{2}\cdots\sigma_{k})\in A_{k}\cross X^{k}(k\geq 0)$$\{\sigma_{1}, \sigma_{2}, \cdots, \sigma_{k}\}\in\wp_{\omega}(X)$$(a_{1}, \sigma_{1})(a2, \sigma_{2})\cdots(a_{k}, \sigma_{k})\in(A\cross X)^{*}$

References[1] Peter Aczel,$\mathrm{N}_{\mathrm{o}\mathrm{n}-}\mathrm{w}\mathrm{e}\mathrm{l}1_{-}\mathrm{f}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{d}$sets, CSLI Lecture Notes, No. 14, Stanford University, 1988.

[2] Peter Aczel and Nax Mendler, A final coalgebra theorem, Lecture Notes in Computer Science, Vol.
389 (1989), 357-365.
[3] Michael Barr, Terminal coa.lgebras in well-founded set theory, Theoretical Computer Science
114(3) (1993), 299-315.

[4] Yasuo Kawahara and Yoshihiro Mizoguchi, Relational structures and their partial morphisms inthe view of single pushout rewriting, To appear in Lecture Notes in Computer Science, 776 (1994),

218–233.

[5] Yasuo Kawahara and Masao Mori. A small final coalgebra theorem. Technical Report RIFIS-TRCS-90, Research Institute of Fundamental Information Science, Kyushu University, 1994.
[6] Saunders Mac Lane, Categories for the working mathematicians, Springer-Verlag, 1971.
[7] Yoshihiro Mizoguchi, A graph structure over the category of sets and partial functions, Cahiers detopologie et g\’eom\’etrie diff\’erentielle cat\’egoriques, 34 (1993), 2–12.

[8] J.C. Raoult, On graph rewritings, Theoret. Comput. Sci. 32(1984), 1-24.
[9] Jan J.M.M. Rutten and Daniel Turi, On the foundations of Final Semantics: Non-Standard Sets,
Metric Spaces, Panial Orders, Lecture Notes in Computer Science, 666 (1992), 477–530.