Jtdylktuy

Category Theory has enormous utility as language for expressing mathematics, both continuous and discrete. It allows beautiful and succinct expression of that else be clumsy and clutterized. One important factor of that utility (I guess) is that CT uses function equality instead of Leibniz equality so (assuming working only with definitions and theorems that are "not evil") it does not distinguish between isomorphic structures.

So, the question: Are there some theories that allows theorems to be restated in more abstract and more succint way while using bisimulation (or something like) instead of Leibniz Equality? (It is OK if that theories will have a lot narrower application that CT (CS area is preferred, though).)

An explanation of what bisimulation means for these who out of CS context:

Consider some set of labels L and two structures A and B, each with set (a carrier) and with partial function from carrier and label to carrier (we call that function `step'). Step also may be relation if nondeterminism wanted.

Bisimulation is a relation between two these structures A and B such that there exists relation R with the following two properties: (1) for all x1 and x2 from carrier of A, and for all y1 from carrier of B, (x1,y1) in R AND (x1,a,x2) in step(A) there exists y2 such that (y1,a,y2) in step(B) and (x2,y2) in R; (2) for all y1 and y2 from carrier of B, and for all x1 from carrier of A, (x1,y1) in R AND (y1,a,y2) in step(B) there exists x2 such that (x1,a,x2) in step(A) and (x2,y2) in R.

Informally speaking, bisimulation between two systems means that externally visible behaviour of that systems is indistinguishable for external observer.

(* Coq poetry *)



Record Machine (State Label : Set) : Type := mkMachine

    { initial : State -> Prop

    ; accepting : State -> Prop

    ; step : State -> Label -> State -> Prop

    }.



(* simulates M1 M2 === M1 `embedded_in` M2 *)



Definition simulates

    {S1 S2 L : Set}

    (R : S1 -> S2 -> Prop) (M1 : Machine S1 L) (M2 : Machine S2 L) : Prop

    :=

    (forall q, M1.(initial) q -> exists s, R q s AND M2.(initial) s) AND

    (forall q, M1.(accepting) q -> exists s, R q s AND M2.(accepting) s) AND

    (forall q1 q2 s1 a,

    R q1 s1 ->

    M1.(step) q1 a q2 ->

    exists s2,

    M2.(step) s1 a s2 AND

    R q2 s2).



Definition bisimulation

    {S1 S2 L : Set}

    (R : S1 -> S2 -> Prop) (M1 : Machine S1 L) (M2 : Machine S2 L) : Set

    :=

    simulates R M1 M2 AND simulates (Flip R) M2 M1.



Definition no_junk_states

    {S1 S2 : Set}

    (R : S1 -> S2 -> Prop)

    :=

    (forall q, exists s, R q s) AND

    (forall s, exists q, R q s) .



Definition no_junk_steps

    {S1 S2 L : Set}

    (R : S1 -> S2 -> Prop) (M1 : Machine S1 L) (M2 : Machine S2 L) : Prop

    :=

    forall q1 q2 a,

    M1.(step) q1 a q2 ->

    exists s1, exists s2,

    M2.(step) s1 a s2 AND

    R q1 s1 AND

    R q2 s2.

For example, these two systems is bisimilar with $R = {(a,e),(a,g),(b,f),(c,h),(d,h)}$:

And those are NOT bisimilar (Q do not ever tries to simulate P):

Applications of bisimulation (stolen from MathOverflow):

• process equivalence in concurrency theory


• model logic: expressiveness characterisations, modal correspondence theory


• coinduction, for example in Game Theory


• non-well founded set theory


• algebraic set theory


• geometric topology

tunes.org said:

The category-theoretic definition of bisimulation is the following. A bisimulation between two coalgebras A1 and A2 is a coalgebra A3 such as there is a span of homomorphisms from A3 to both A1 and A2. Intuitively, this means that there is an automaton A3 that can be simulated contemporarily by A1 and by A2.

Note that it is easy to extend bisimulation defined on coalgebras to algebras too by adding property such that for each constructor C : L -> carrier(A), there must be constructor C' from B such that C' : L -> carrier(B) and for all l in L, (C(l),C'(l)) in R and vise versa.

First let's talk about the category of relations. The category of relations is the category whose objects are sets and whose morphisms $text{Hom}(A, B)$ between two sets are the relations $A times B to { 0, 1 }$. Composition of relations is defined as follows: if $R in text{Hom}(A, B), S in text{Hom}(B, C)$, then the composite relation $S circ R in text{Hom}(A, C)$ is defined by $a (S circ R) c$ if there exists $b in B$ such that $a S b, b R c$.

The category of relations has extra structure not possessed by the category of (sets and) functions: it is a dagger category, which means that associated to each morphism $f : A to B$ there is a morphism $f^{dagger} : B to A$, and this assignment satisfies natural properties. In this particular case $f^{dagger}$ is just given by taking the transpose relation. (I hesitate to call this the "inverse" relation because it is not in general the inverse morphism in the usual sense.)

Let $L$ be a set of labels. We can define a category $text{Trans}_L$ whose objects are sets $A$ equipped with partial functions $t_A : A times L to A$ (labeled state transition systems) and whose morphisms are simulations: that is, $R in text{Hom}(A, B)$ if, whenever $a xrightarrow{ell} a'$ is a transition in $A$, there is a transition $b xrightarrow{ell} b'$ in $B$ such that $aRb, a' R b'$.

From this category we can define a dagger category $text{BTrans}_L$ with the same objects whose morphisms are simulations such that their daggers are also simulations (that is, bisimulations). Unlike what I previously thought, bisimulations are not the same as simulations such that their inverses are simulations. Nevertheless, in this way bisimulation still defines an equivalence relation on labeled state transition systems.

A nice analogy for the corresponding equivalence relation is that of cobordism of manifolds, since the cobordism category is also a dagger category.