Coalgebraic (Bi)Similarity

(draft … references to be added)

One of the main contributions of coalgebra to computer science is to provide the minimal abstract setting allowing us to account for various different notions of simulation and bisimulation in a uniform way with the help of a single simple parameter, that of a functor \(T\) on a category \(\mathcal C\).

The objects of the category \(\mathcal C\) represent the possible state spaces and the functor \(T\) represents the possible one-step transitions states can take.

Since (bi)simulation is a relationship betweeen states, the category \(\mathcal C\) should be the category of sets, or of sets with additional structure. The theory of (bi)similarity is not part of the theory of coalgebras that can be developed over arbitrary categories \(\mathcal C\). [1]

In the following we will define bisimilarity for set-coalgebras and then look at (bi)similarity for coalgebras over other base categories.

Bisimilarity for Set-Coalgebras

Every functor \(T:\sf Set\to Set\) induces a notion of \(T\)-bisimilarity on elements of \(T\)-coalgebras \(X\to TX\).

Definition: Bisimilarity (behavioural equivalence) \(\simeq\) is the smallest equivalence relation between elements \((x,X\to TX)\) of coalgebras induced by pairs

\[(x,X\to TX)\ \simeq\ (f(x),Y\to TY)\]

where \(f:X\to TX\) is a coalgebra morphism.

Intuitively, bisimilarity captures that what is preserved by homomorphisms. [2]

Remark (2nd Definition): Equivalently, this definition can be formulated using cospans. Two elements of two coalgebras are bisimilar (behaviourally equivalent)

\[(x,X\to TX)\ \simeq\ (y,Y\to TY)\]

if there are coalgebra morphism \(f,g\) with \(f(x)=g(y)\).

The second definition has the advantage that one does not need to close under transitivity. The first definition has the advantage that it is more conceptual and makes the connection of bisimilarity with the final coalgebra more direct, as we are going to see now.

Observation: The equivalence classes of bisimilarity are the connected components of the category of elements of the forgetful functor \({\sf Coalg}( T)\to \sf Set\).

Recall that colimits in the category of sets can be computed by taking a disjoint sum and then quotienting by connected components. [3]

This implies, together with the Definition and the Observation, that the colimit of the forgetful functor quotients the disjoint sum of all coalgebras by bisimilarity, yielding the final coalgebra. [4]

Prop: The final coalgebra (if it exists [5]) is the colimit of the forgetful functor \(U:{\sf Coalg}( T)\to \sf Set\).

Proof: Let \(Z={\sf colim}\,U\). The coalgebra structure \(Z\to TZ\) is given by the universal property of the colimit. Moreover, by \(Z\) having a cocone \(c\) over \(U\), for every \(X\to TX\) there is a morphism \(c_X:X\to Z\). In particular, there is \(c_Z:Z\to Z\). It follows from \(Z\) being a colimit that \(c_Z\) is the identity. But this implies that all coalgebra morphisms \(f:X\to Z\) are equal to \(c_X\). Hence there is precisely one coalgebra morphism \(X\to Z\) and \(Z\to TZ\) is the final coalgebra.

Remark: This proof is a variation of Lemma 1 in Chapter X of Mac Lane, which shows that the limit of the identity functor is the initial object (and the colimit of the identity functor is the terminal object).

(Bi)similarity for Ordered Coalgebras

We briefly indicate that essentially the same approach to bisimilarity works for coalgebras over ordered sets (preorders or posets). [6]

Let \(T:\sf Ord\to Ord\) be a functor.

Definition: Two elements of two coalgebras are (bi)similar

\[(x,X\to TX)\ \lesssim\ (y,Y\to TY)\]

if there are coalgebra morphism \(f,g\) such that \(f(x)\le g(y)\).

Colimits in preorders are computed as in \(\sf Set\) with the preorder on the colimit being the smallest preorder compatible with the preorders on the components. Colimits in posets additionally quotient by antisymmetry.

We can adapt the category of elements to the ordered setting. Then (bi)similarity is the smallest preorder on the category of elements generated by “connections between components” and the “preorders inside components”.

As before we obtain

Prop: The final coalgebra (if it exists) is the colimit of the forgetful functor \({\sf Coalg}( T)\to \sf Ord\).

Other Base Categories

One could continue here with looking at other base categories such as metric spaces, topological spaces, nominal sets, various categories of algebras, …

I don’t do this (for now) because the literature is big and growing and the new interesting phenomena that arise are particular to the base category one chooses.

References

Modal Logic: van Benthem, Segerberg, Goldblatt, …

Concurrency: Park, Milner, van Glabbeek, Panangaden, …

Coalgebra: Aczel, Aczel-Mendler, Barr, Rutten, Worrell, Kurz, Staton, Hughes-Jacobs, Balan-Kurz-Velebil, …

Mac Lane: Categories for the Working Mathematician. 1971.

---

[1]

This can be seen from the fact that the theory of coalgebras over \(\mathcal C\) is the theory of algebras over \(\mathcal C^{\rm op}\). But the theory that can be developed simultaneously for algebra and coalgebra is quite small in the sense that it excludes most features that are of particular interest to the algebraist or the coalgebraist. Intuitively, the intersection of algebra and coalgebra only consists of those “systems” that can be defined by unary operations such as deterministic automata or, more generally, presheaves.

[2]

This notion makes sense in any category which has a forgetful functor to \(\sf Set\). Why is it trivial for categories of algebras?

[3]

Exercise: Let \(D:\mathcal I\to \sf Set\) be a functor. Form the disjoint sum \(S\) of all \(D(i)\), \(i\in\mathcal I\). Connect \((x,Di)\) with \((y,Dj)\) if there is \(f:i\to j\) in \(\mathcal I\) such that \(f(x)=y\). Then the connected components of \(S\) are the colimit of \(D\).

[4]

For a deeper understanding of final coalgebras, it is instructive to study the proof of the General Adjoint Functor Theroy as it appears in Mac Lane and then the proof of the final coalgebra theorem of Aczel-Mendler. Further contributions to this topic are in papers by Barr, by Adamek-Milius-Velebil and others. Much of this work resolves around the question of what are the most elegant side conditions that allow us to cope with situations where the final coalgebra does not exist in the category of coalgebras. (Footnote: Aczel-Mendler showed that for all set-functors there is a final coalgebra that classifies bisimilarity for all set-coalgebras and the carrier of which is a proper class. I find this still the most elegant formulation of the size problem in coalgebra as it shows exactly where the distinction between set and proper class comes in.)

[5]

As shown by Aczel-Mendler, the final coalgebra always exists if one allows coalgebras on proper classes (as opposed to only sets).

[6]

It is well known, in the classic case of the Kripke frames (coalgebras for the powerset functor), that to ask that \(x,y\) are bisimilar is a stronger requirement than to ask that \(x,y\) are forward and backward bisimilar. Accordingly, it does make a difference whether we take, for example, the final upset-coalgebra over preorders or posets. Over preorders equality in the final coalgebra is bisimilarity and the preorder captures forward-simulation. Over posets, equality means the existence of a forward-simulation in both directions.