(draft … reference to be added) … (up)
The basic observation about ordinary, set-based coalgebras, due to Aczel's monograph "Non-Well Founded Sets", is the following:
Given a coalgebra , the largest bisimulation on is the kernel of the unique morphism into the final coalgebra .
Aczel observed this as a fact for special coalgebras such as Kripke models and then took it as a starting point for a general definition, known today as Aczel-Mendler bisimulation.
Moving to the ordered setting, that is, enriching over preorders or posets, one can generalise by either formalising kernels as pullbacks (as before) or as order-pullbacks, which we call comma objects or comma squares or just commas, following terminology introduced by Lawvere in the category-enriched situation.
Choosing pullbacks, one only recovers the equality on the final coalgebra. On the other hand, choosing comma squares leads to a richer theory of bisimulations that includes simulations as special cases of bisimulations.
In fact, in preorders and posets, comma and cocomma squares are exact, that is, weakening relations can be both tabulated and cotabulated. This leads us to Definition 5.2 of (Worrell 2000), which, btw, does work for more general enrichments. Also note that because of the use of co-spans there is no need to restrict to weak-pullback preserving functors.
We first need to recall that every weakening relation can be represented as a preorder/poset such that
In other words, we encode the relation via the order of the preorder/poset , also known as the collage of and .
Definition: Let be a (locally monotone) functor on preorders or posets. The weakening relation is an order-bisimulation between coalgebras and if there is such that
Remark: Equivalently, is an order-bisimulation if the unqiuely determined function in is order-preserving.
Remark: It follows from the definition that is a weakening relation. In other words, the pullback and the comma of the cospan coincide. (Notation: I am tempted to drop the overline over the in the following, because of the ugly extra space it introduces between lines.)
Example: The identity cospan is not isomorphic to the collage of a relation unless is discrete. The collage of the order on can be obtained as the cocomma of the comma of the identity cospan. [1] In fact, in posets, every collage is the cocomma of its comma.
Example: If we instantiate the definition above with the downset functor and the upset functor, we obtain that -bisimulation is simulation.
Let be the downset functor. A bisimulation between -coalgebras and is a relation such that
or, more explicitely, [2]
Let be the upset functor. Recall that is ordered by reverse inclusion. A bisimulation between -coalgebras and is a relation such that
or, more explicitely,
Intuitively, a -bisimulation is forward simulation: Every move in the domain can be simulated by a "larger" move in the codomain. Conversely, -bisimulation is backward simulation: Every move in the codomain can be simulated by "smaller" move in the domain. (The words "smaller" and "larger" are intended to remind us of the fact that is a weakening relation closed under the order in and .)
Remark: Notice that even if and are discrete, we do not obtain ordinary bisimulation, but rather ordinary forward and backward simulation. On the other hand, if we take to be the convex powerset functor, then -bisimulation is ordinary bisimulation.
Remark: The framework of functorial modal logic guarantees that for every functor there is a sound, complete and bisimilarity preserving logic. In this case, these are the familiar -logic for the downset functor and the -logic for the upset functor. In case of the convex powerset functor we obtain Dunn's positive modal logic.
Recall from Monotone Neighbourhood Coalgebras and Neighbourhood Coalgebras the various ways in which neighbourhood coalgebras can be extended to the ordered setting. For the proofs below, we will need the following.
In we have
In we have
Recall for ordered sets . In particular is for discrete (when is ordered by inclusion).
Lemma: Let be a weakening relation and its collage. Then the order of is given by
Corollary: A weakening relation is a cospan-(bi)simulation between -coalgebras and iff
Recall for ordered sets .
Lemma: Let be a weakening relation and its collage. Then the order of is given by
Corollary: A weakening relation is a cospan-(bi)simulation between -coalgebras and iff or, more explicitely,
Can these characterisations be rephrased using the ordered version of -coherent pairs? [3]
No, because is equivlant to . [4] On the other hand, the dual [JKM20] of a relation is defined as , that is, .
Remark: The weakening relation is a -bisimulation iff
and is a -bisimulation iff
For the Ordification of the neighbourhood functor and the monotone neighbourhood functor see the note on Cospan Bisimulation.
Is obtained from the conjunction of the two conditions above.
Hansen, Kupke and Pacuit: Neighbourhood Structures: Bisimilarity and Basic Model Theory. LMCS 2009. (Def 3.5, Thm 3.12)
Worrell: Coinduction for recursive data types: partial orders, metric spaces and -categories, CMCS 2000. (Def 5.2)
Aczel:
Aczel, Mendler:
Lawvere:
Rutten:
This observation is useful for working with abstract order-enriched categories. If they admit commas of identity cospans, then for each object there is a span representing the order on that object. ↩︎
We write for and similarly for etc. ↩︎
R-coherent pairs were introduced in [HKR09]. ↩︎
If is a weakening relation then is the opposite relation. In the discrete case it coincides with . ↩︎