2
$\begingroup$

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.

  • 0
    Could you briefly explain what bisimulation means in a mathematical context for those of us without a CS background?2011-05-30
  • 1
    Okay, so as far as I can tell, bisimulation is just a type of isomorphism in a particular category. You don't need to go outside of category theory to describe it.2011-05-30
  • 1
    Take the category whose objects are those systems and whose morphisms are relations respecting the transitions. (I have to admit I don't fully understand the definition of your systems, though. You say they're equipped with a function from carriers and labels to carriers, but what's the output of this function on $a$ and $y$ in the first system?)2011-05-30
  • 0
    Idea of my question is not "to go outside of category theory to describe bisimulation" but to weaken category theory by replacing isomorphism by bisimularity to allow definitions be more abstract.2011-05-31
  • 0
    I withdraw my previous comments; having reread the definition on Wikipedia, it is not quite what I thought it was. But it can still be understood in the context of category theory.2011-05-31

1 Answers 1