Theory of supercategories

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.

-
Could you briefly explain what bisimulation means in a mathematical context for those of us without a CS background? – Qiaochu Yuan May 30 '11 at 9:21
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. – Qiaochu Yuan May 30 '11 at 9:57
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?) – Qiaochu Yuan May 30 '11 at 10:39
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. – Vag May 31 '11 at 8:38
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. – Qiaochu Yuan May 31 '11 at 17:16

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.

-
Why have you set up relation by characteristic function, not as just relation? Do you mean it must be computable? – Vag Jun 1 '11 at 8:46
No. It's just a relation. How I implement relations is irrelevant. – Qiaochu Yuan Jun 1 '11 at 9:38