(draft … references to be added) … (up)
We collect some results on cospan bisimulations. These results invariable relate ordinary bisimulations on sets with ordered bisimulation on ordered sets. Since bisimulations on ordered sets include simulations as well as bisimulations we will call them (bi)simulations.
We first review notation and define the notion of an order-extension of a set-functor.
The subsection span and cospan bisimulations investigates the relationship between cospan bisimulations and span bisimulations.
The subsection cospan (bi)simulations and change of base looks at cospan (bi)simulations enriched over different quantales.
Together this shows that cospan (bi)simulation works uniformly over sets, orders, metric spaces and -categories. For example, Rutten's final coalgebra theorem for sets can now be seen as a special case of Worrell's final coalgebra theorem for -categories.
If and are cospan-bisimulations, is then a coalgebra morphism?
Connections with logic induced bisimulations?
In this section,
Following on from part one, we are interested in preordification of . Preordifictions are universal solutions to the problem of finding a together with a transformation . In fact, the preordification of can be defined as the -enriched left Kan extension of along . But some results hold more generally for any ordered extension .
Definition: We call an order-extension of if there is a natural transformation
Remark: Equivalently, is an order-extension of if there is a natural tranformation . This also captures the intuition that adds ordering to . If one insists on being an iso, this notion is equivalent to the one of Jacobs and Jacobs-Hughes (ADD REFERENCES).
Question: iso is equivalent to being bijective. Is there an interesting example of an order-extension for which is not bijective?
Remark: The mate of is . If is the preordification then is an iso, but for posetifications this does not need to be the case as the example of convex powerset (=the posetification of powerset) shows. We summarise some of the relationships between properties of these natural transformations in the table below.
1 | ' is an order-extension of | ||
2 | iso | a strict order-extension of | |
3 | left Kan extension, | is the ordification of | |
4 | iso | ' is an order-lifting of | |
5 | iso | is an order on |
and and . If , then also .
The following result makes precise that every span bisimulation is a cospan (bi)simulation.
Proposition: Let be an order-extension of . If two states in two -coalgebras are -span-bisimilar then they are -cospan-(bi)similar.
Proof: Let and be two -caolgebras. Let be a -span bisimulation. Let be the cocomma of . Applying to the square
and using the arrow from the span-bisimulation the universal property of the cocomma gives the required arroe . QED
Examples: A number of familiar examples arise as instances of this proposition.
Questions: Is there something more one can say about structural relationships between bisimulation and simulation? For example, one could try to isolate those functors for which forward simulation plus backward simulation is bisimulation, but I do not know how interesting this would be (is there a good abstract notion of "deterministic" functor?). Anything else?
For weak pullback preserving functors, we also have the converse of the previous proposition.
Proposition: Let preserve weak pullbacks. If two states in two -coalgebras are cospan-bisimilar then they are span-bisimilar.
Proof: Let be a cospan bisimulation and be the collage, hence cocomma, of . Let be the ordification of . With the help of the iso we can consider the -square as a cocomma in ordered sets. Cocommas are exact. Since ordifications preserve exact squares if preserves weak pullbacks [Theorem 4.11,BKV15] , the -square is exact. But exact squares in posets are weak comma squares, hence there is an making into a span bisimulation. QED
In sets every function is a relation and every coalgebra morphism a bisimulation. In ordered sets every function gives rise to two relation and with
Proposition: Let . If is a -coalgebra morphism, then and are cospan-(bi)simulations.
Proof: and are the weakening closures of the spans and , respectively. Recall the definition of cospan-(bi)simulation and the fact that the collage of the weakening closure of a relation represented by a span is the cocomma of . Now the proposition follows from the universal property of cocommas. QED
Example: Recall that is a -cospan-(bi)simulation iff
We also know that is a morphism of -coalegbras iff
It is now easy to check that the first clause says precisely that is a (bi)simulation and the second clause that is a (bi)simulation. (I find this very pretty.)
Question: Can we prove the converse of the proposition? - - - This is interesting, I wrote out the obvious diagrams, but I didn't see how to proceed. - - - Maybe the converse is only true in special cases?
Cospan (bi)simulations allow us to see ordinary coalgebraic bisimulations as well as quantale enriched ones in the same framwork. The basic picture, taken from Section 4 of [BKV19] is as follows. take, respectively, connected components, discrete preorders and underlying sets. They lift via doctrinal adjunction to coalgebras since the right adjoints satisfy and .
On the right-hand side, is the top and bottom preserving embedding with a right adjoint and, if is non-trivial and integral[1], a left adjoint . The left ajoint maps all elements other than bottom to and the right adjoint maps all elements other than top to . The adjunction lifts to a -enriched adjunction between the categories of coalgebras. If the quantale has no zero-divisors, then is a quantale-morphism and lifts to -cat enriched adjunction between categories of coalgebras. See Propositions 4.9 and 4.10 of [BKV19] for details.
Propositions ?? … I think, mutatis mutandis, we can move the two propositions above from the left Set/Pre column to the right Pre/-cat column …
Examples ?? Can we make an example of ordinary transition systems and bisimulation and then a metric example? Are there scenarios where one would want an orderd coalgebra as an abstraction of a metric coalgebra? I never really looked so much at Kripke frames over metric spaces … any ideas?
Balan, Kurz, Velebil: Positive fragments of coalgebraic logics. 2015.
Balan, Kurz, Velebil: Extending set functors to generalised metric spaces. 2019.
Jacobs
Hughes-Jacobs
Scratch notes on exact squares
A quantale is integral if the neutral element of the multiplication is the top element. ↩︎