# «A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Electrical Engineering and Computer ...»

The converse is not true: the equivalence kernel of a homomorphism is not, in general, a bisimulation (see Example 2.3.3). But the graph of a homomorphism, or more accurately, considering our working deﬁnition of a binary class relation, the homomorphism itself, is.

Assume F -coalgebras C1, γ1 to C2, γ2.

** Theorem 2.3.**

2. h is a homomorphism from C1, γ1 to C2, γ2 if and only if h is a class function from C1 to C2, and a bisimulation between C1, γ1 and C2, γ2.

Proof. See [56, thm. 2.5].

In other words, homomorphisms are functional bisimulations. This should not be surprising: homomorphisms are supposed to preserve structure, and bisimulations to capture equivalence of it. But do they really?

There is not much to be said about homomorphisms; they are too basic to doubt.

Bisimulations, on the other hand, deserve investigation.

We begin with a formal statement of coalgebraic bisimilarity.

We say that c1 and c2 are bisimilar among C1, γ1 and C2, γ2 if and only if there is a bisimulation B between C1, γ1 and C2, γ2 such that c1 B c2.

We say that c1 and c2 are bisimilar in C, γ if and only if c1 and c2 are bisimilar among C, γ and C, γ.

A disturbing fact about coalgebraic bisimilarity is that, unlike ordinary bisimilarity, it is not, in general, an equivalence concept.

** Example 2.3.**

3. Let F be an endofunctor on Class that assigns to every class C the class

Let S2 = {0}, and γ2 be the unique function from S2 to F (S2 ), namely a function from S2

**to F (S2 ) deﬁned by the following mapping:**

0 → 0, 0, 0.

Let h be the unique function from S1 to S2, namely a function from S1 to S2 deﬁned by the

**following mapping:**

0 → 0;

1 → 0.

h is trivially a homomorphism from S1, γ1 to S2, γ2. But whereas h(0) and h(1) are equal, and thus, trivially bisimilar in S2, γ2, 0 and 1 are not bisimilar in S1, γ1, lest there be a binary relation B on S1, and an F -coalgebra graph B, β such that 0, 1 ∈ graph B and β( 0, 1 ) = 0, 0, 0, 1, 1, 1.

** Note 2.3.**

1. We cannot replace ordered triples with multisets of size 3 having at most two members of multiplicity greater than 0 to the same eﬀect in Example 2.3.3.

** Example 2.3.**

1.1. Let F be an endofunctor on Class that assigns to every class C the class

For every class C, F (C) is simply the class of all multisets of size 3 having just at most two members of multiplicity greater than 0 (see [62, chap. A]).

**Let S = {0, 1}, and γ be a function from S to F (S) deﬁned by the following mapping:**

0 → [0, 0, 1];

1 → [0, 1, 1].

We want to show that the full binary relation on S is a bisimulation on S, γ. In order to do so, we must ﬁnd a function β : S × S → F (S × S) such that both proj1 (S × S) and proj2 (S × S) are homomorphisms from the F -coalgebra S × S, β to S, γ.

**One such function is deﬁned by the following mapping:**

→[ 0, 0 0, 0, 0, 0, 0, 0 ];

→[ 0, 1 0, 1, 0, 1, 1, 0 ];

→[ 1, 0 0, 1, 1, 0, 1, 0 ];

→[ 1, 1 1, 1, 1, 1, 1, 1 ].

Thus, 0 and 1 are bisimilar in S, γ.

This should cast serious doubt on the coalgebraic notion of bisimulation: how can one hope to capture all of equivalence of structure using a notion, the induced similarity concept of which is not, in general, transitive?

This discrepancy was not lost on Aczel and Mendler, who, also in [5], generalized the coalgebraic concept of bisimulation further into that of what they called a precongruence, or in the case of an equivalence class relation, a congruence. This is a technically more complicated concept: to determine whether a binary class relation R on the carrier of an F -coalgebra C, γ is a precongruence on C, γ, one has to invoke a quotient of C with respect to the equivalence class relation generated by R, compose its image under F with γ, and test whether R is contained in the equivalence kernel of the composite. It is also an intuitively more warranted concept, exactly formalizing the idea of a class relation that is compatible with the cooperation of a coalgebra. Every bisimulation on an F -coalgebra is a precongruence, but not every precongruence on an F -coalgebra is a bisimulation. In fact, the endofunctor that we used in Example 2.3.3 is one that was devised in [5] for the express purpose of demonstrating this separation between the two concepts.

CHAPTER 2. TRANSITION SYSTEMS 22 ** Note 2.3.**

2. We can also use Example 2.3.3 to separate the two concepts. For by [31, prop. 4.2], the equivalence kernel of a homomorphism from an F -coalgebra C1, γ1 to an F -coalgebra C2, γ2 is a precongruence on C1, γ1.

** Note 2.3.**

3. In [5], the concept of precongruence was deﬁned only for binary class relations on single F -coalgebras. However, one can use directed sums (see Deﬁnition 2.4.10), to extend this deﬁnition to binary class relations between pairs of diﬀerent F -coalgebras.

Deﬁnition 2.3.3.1. A precongruence on C, γ is a binary class relation P on C such that for every quotient q with respect to the equivalence class relation generated by P,

** graph P ⊆ graph ker(F (q) ◦ γ).**

We say that P is a congruence on C, γ if and only if P is a precongruence on C, γ, and an equivalence class relation on C.

**The following is easy:**

Proposition 2.3.3.2. P is a precongruence on C, γ if and only if P is a class relation on C, and the equivalence class relation generated by P is a congruence on C, γ.

We say that c1 and c2 are congruent in C, γ if and only if there is a congruence P on C, γ such that c1 P c2.

Deﬁnition 2.3.4. A precongruence between C1, γ1 and C2, γ2 is a binary class relation P : C1 ↔ C2 such that

Proof. Suppose that B is a bisimulation between C1, γ1 and C2, γ2.

Let graph B, β be an F -coalgebra such that dpr B is a homomorphism from graph B, β to C1, γ1, and cpr B one from graph B, β to C2, γ2.

Let E be the equivalence class relation generated by (inj1 (C1 + C2 ))−1 ; B ; inj2 (C1 + C2 ).

** Theorem 2.3.**

3.4. h is a homomorphism from C1, γ1 to C2, γ2 if and only if h is a class function from C1 to C2, and a precongruence between C1, γ1 and C2, γ2.

Proof. Suppose that h is a homomorphism from C1, γ1 to C2, γ2.

Then by Theorem 2.3.2, h is a bisimulation between C1, γ1 and C2, γ2, and thus, by Proposition 2.3.3.3, a precongruence between C1, γ1 and C2, γ2.

Conversely, suppose that h is a precongruence between C1, γ1 and C2, γ2.

Let E be the equivalence class relation generated by (inj1 (C1 + C2 ))−1 ; h ; inj2 (C1 + C2 ).

Let q be a quotient of C1 + C2 with respect to E.

**Then the following diagram commutes:**

E is the smallest equivalence class relation that contains (inj1 (C1 + C2 ))−1 ; h ; inj2 (C1 + C2 ), or equivalently, the smallest transitive relation that contains the reﬂexive-symmetric closure of it.

**We use induction to prove that for any c1 and c2 such that c1 E c2, the following are true:**

CHAPTER 2. TRANSITION SYSTEMS 25

If c1 = c2, then (i) and (ii) are vacuously true. Also, since inj1 (C1 + C2 ) is injective, (iii) is trivially true, and since inj2 (C1 + C2 ) is injective, (iv) is trivially true.

(inj2 (C1 + C2 ))(c2 ) = c2, and h(c ) = c2. Thus, (ii) and (iii) are vacuously true. Also, by the induction hypothesis, if there is c1 such that

(inj1 (C1 + C2 ))(c2 ) = c2, and c = h(c2 ). Thus, (i) and (iv) are vacuously true. Also, by the induction hypothesis, if there is c1 such that (inj2 (C1 + C2 ))(c1 ) = c1, then c1 = c, and hence, h(c2 ) = c1. Thus, (ii) is true. Finally, by the induction hypothesis, if there is c1 such that (inj1 (C1 + C2 ))(c1 ) = c1, then h(c1 ) = c, and hence, h(c1 ) = h(c2 ). Thus, (iii) is true.

Therefore, q ◦ inj2 (C1 + C2 ) is injective, and thus, has a left inverse.

Another implication, which we are not using for this proof, is that { c1, c2 | q((inj1 (C1 + C2 ))(c1 )) = q((inj2 (C1 + C2 ))(c2 ))} = graph h, is a pullback of q ◦ inj1 (C1 + C2 ) and q ◦ inj2 (C1 + C2 ) in and thus, graph h, dpr h, cpr h F -Coalg.

Let g be a left inverse of q ◦ inj2 (C1 + C2 ).

Since h is a class function, dpr h is bijective, and h = (cpr h) ◦ (dpr h)−1.

Thus, by generalization, h is a homomorphism from C1, γ1 to C2, γ2.

An immediate corollary of Theorem 2.3.2 and 2.3.3.4 is that in the case of single-valued binary class relations, the concepts of bisimulation and precongruence coincide.

Here, mostly for the purpose of accessibility, we have decided to follow the approach of Rutten in [56], who advocates the coalgebraic concepts of bisimulation and bisimulation equivalence as formal duals to the algebraic ones of substitutive relation and congruence.

His tacit preference over the more appropriate concepts of precongruence and congruence of [5] is partly justiﬁed by the the fact that more can be proved about bisimulations and bisimulation equivalences than precongruences and congruences. No matter: most of the theory in [56] is developed under the assumption that the endofunctor F preserves weak pullbacks, a technical condition under which the concepts of bisimulation and precongruence coincide. And although we will never need to make explicit mention of it, every particular endofunctor considered here will actually satisfy this condition, unless speciﬁcally intended not to.

2.4 Behaviour modelling and ﬁnal coalgebras Suppose that we wanted to use L-labelled transition systems to model the behaviour of processes of some kind. What we would wish for then is that there be a system diverse enough to model the behaviour of every process, but coarse enough not to distinguish between processes of equivalent behaviour. Is there such a system?

The way to use an L-labelled transition system to model the behaviour of a process is to map the process to a state of the system, and let the branching structure emanating from that state represent the behaviour of the process. Equivalence of behaviour then amounts to similarity of branching structure of some kind, and indeed determines the actual association between ‘behaviour’ and branching structure. If we let bisimilarity be that concept of similarity, and assume for simplicity that any state of every L-labelled transition system models the behaviour of some process, then our question becomes an enquiry over the existence of an L-labelled transition system S, T such that for every L-labelled transition system S, T and any s ∈ S, there is s ∈ S such that s and s are bisimilar among S, T and S, T, and for any s1, s2 ∈ S, s1 and s2 are bisimilar in S, T if and only if s1 = s2.

We want to use Theorem 2.3.2 to turn this enquiry into an instance of a common universal construction problem, namely that of a terminal object of a category.

** CHAPTER 2. TRANSITION SYSTEMS 29 An object of a category is a terminal object of that category just as long as for every object of that category, there is exactly one arrow of that category from the latter to the former.**

The category pertaining to our enquiry is that of all L-labelled transition coalgebras and all homomorphisms between them. But once again, we work generally.

First, notice that for every F -coalgebra C, γ, id C is an endomorphism on C, γ, and for every homomorphism h1 from an F -coalgebra C1, γ1 to an F -coalgebra C2, γ2, and every homomorphism h2 from C2, γ2 to an F -coalgebra C2, γ2, h2 ◦ h1 is a homomorphism from C1, γ1 to C2, γ2. Thus, F -coalgebras and their homomorphisms form a category.

We write F -Coalg for the category whose objects are all the F -coalgebras, and arrows all the homomorphisms from one F -coalgebra to another.

Note that for any homomorphism h from an F -coalgebra C1, γ1 to an F -coalgebra C2, γ2, the domain and codomain of h as an arrow of F -Coalg are C1, γ1 and C2, γ2 respectively, and not to be confused with the domain and codomain of h as an arrow of Class, which are C1 and C2 respectively.

We say that C, γ is ﬁnal in F -Coalg if and only if for every F -coalgebra C, γ, there is exactly one homomorphism from C, γ to C, γ.

We use “ﬁnal” here rather than “terminal” only to conform with common practice in the germane literature: an F -coalgebra is ﬁnal in F -Coalg if and only if it is a terminal object of F -Coalg.

Notice that if C1, γ1 and C2, γ2 are both ﬁnal in F -Coalg, then C1, γ1 ∼ C2, γ2, = lest there be another endomorphism, apart from the identity map, on either of them. In plain words, all ﬁnal F -coalgebras are isomorphic to one another.

** Theorem 2.3.**

2 suggests that there might be a connection between our enquiry and the notion of ﬁnality. We set out to make this connection, if any, precise.

We say that C, γ is weakly complete in F -Coalg if and only if for every F -coalgebra C, γ and any c ∈ C, there is c ∈ C such that c and c are bisimilar among C, γ and C, γ.

Note that our use of the term “weakly complete” is diﬀerent from, and in general, strictly more inclusive than that in [2], [5], and [3].

Proposition 2.4.1.1. If for every small F -coalgebra C, γ, there is a homomorphism from C, γ to C, γ, then C, γ is weakly complete in F -Coalg.

Proof. Suppose that for every small F -coalgebra C, γ, there is a homomorphism from C, γ to C, γ.

Assume an F -coalgebra C, γ.

Assume c ∈ C.

** By Lemma 2.4.**