Try   HackMD

Bisimulation for Ordered Coalgebras

(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

X, the largest bisimulation on
X
is the kernel of the unique morphism
XZ
into the final coalgebra
Z
.

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

R:XY can be represented as a preorder/poset
R
such that

  • the underling set of
    R
    is the disjoint union of
    X
    and
    Y
    and
  • the order on
    R
    is the one inherited from
    X
    and
    Y
    plus
    xRy  xRy
    .

In other words, we encode the relation

R via the order of the preorder/poset
R
, also known as the collage of
X
and
Y
.

Definition: Let

T be a (locally monotone) functor on preorders or posets. The weakening relation
R:XY
is an order-bisimulation between coalgebras
X
and
Y
if there is
RTR
such that
XRYTXTRTY

Remark: Equivalently,

R:XY is an order-bisimulation if the unqiuely determined function
RTR
in
Set
is order-preserving.

Remark: It follows from the definition that

R is a weakening relation. In other words, the pullback and the comma of the cospan
XRY
coincide. (Notation: I am tempted to drop the overline over the
R
in the following, because of the ugly extra space it introduces between lines.)

Example: The identity cospan

XXX is not isomorphic to the collage of a relation unless
X
is discrete. The collage of the order on
X
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

T-bisimulation is simulation.

  • Let

    D be the downset functor. A bisimulation between
    D
    -coalgebras
    (X,ξ)
    and
    (Y,ν)
    is a relation
    RX×Y
    such that
    xRy  ξxνy,

    or, more explicitely, [2]

    xRy  xx.yy.xRy

  • Let

    U be the upset functor. Recall that
    UX=[X,2]o
    is ordered by reverse inclusion. A bisimulation between
    U
    -coalgebras
    (X,ξ)
    and
    (Y,ν)
    is a relation
    RX×Y
    such that
    xRy  ξxνy,

    or, more explicitely,

    xRy  yy.xx.xRy

Intuitively, a

D-bisimulation is forward simulation: Every move in the domain can be simulated by a "larger" move in the codomain. Conversely,
U
-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
R
is a weakening relation closed under the order in
X
and
Y
.)

Remark: Notice that even if

X and
Y
are discrete, we do not obtain ordinary bisimulation, but rather ordinary forward and backward simulation. On the other hand, if we take
T
to be the convex powerset functor, then
T
-bisimulation is ordinary bisimulation.

Remark: The framework of functorial modal logic guarantees that for every functor

T 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.

Ordered neighbourhood coalgebras

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

D(X,) we have
ab  xa.yb. xy.

In

U(X,) we have
ab  yb.xa. xy.

DU
-coalgebras

Recall

DUX=[[X,2],2] for ordered sets
X
. In particular
DUX
is
UpPX
for discrete
X
(when
UpPX
is ordered by inclusion).

Lemma: Let

R:XY be a weakening relation and
R
its collage. Then the order of
DUR
is given by
AB  aA.bB.yb.xa. xRy

Corollary: A weakening relation

R:XY is a cospan-(bi)simulation between
DU
-coalgebras
(X,ξ)
and
(Y,ν)
iff
xRy    aξx.bνy.yb.xa. xRy

UD
-coalgebras

Recall

UDX=[[Xo,2],2]o for ordered sets
X
.

Lemma: Let

R:XY be a weakening relation and
R
its collage. Then the order of
UDR
is given by
AB  bB.aA.xa.yb. xRy

Corollary: A weakening relation

R:XY is a cospan-(bi)simulation between
DU
-coalgebras
(X,ξ)
and
(Y,ν)
iff or, more explicitely,
xRy    bνy.aξx.xa.yb. xRy

Order dual of R-coherent pairs

Can these characterisations be rephrased using the ordered version of

R-coherent pairs? [3]

No, because

xa.yb.xRy is equivlant to
aRo[b]
. [4] On the other hand, the dual [JKM20]
R
of a relation
R
is defined as
(a,b)RR[a]b
, that is,
xa.xRyyb
.

Remark: The weakening relation

R:(X,ξ)(Y,ν) is a
UD
-bisimulation iff
xRy    yb.xa.R[a]b

and

R is a
DU
-bisimulation iff
xRy    xa.yb.aRo[b]

Other Functors

Ordification of the Neighbourhood Functors

For the Ordification of the neighbourhood functor and the monotone neighbourhood functor see the note on Cospan Bisimulation.

Downsets

xRy  xξ(x).yb.xRy(ξ(x)Ro[ν(y)])

Upsets

xRy  yν(y).xξ(x).xRy(R[ξ(x)]ν(y))

Convex subsets

Is obtained from the conjunction of the two conditions above.

References

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)

Further Reading

Aczel:

Aczel, Mendler:

Lawvere:

Rutten:


  1. 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. ↩︎

  2. We write

    xx for
    xξx
    and similarly for
    yy
    etc. ↩︎

  3. R-coherent pairs were introduced in [HKR09]. ↩︎

  4. If

    R:XY is a weakening relation then
    R:YoXo
    is the opposite relation. In the discrete case it coincides with
    R1
    . ↩︎