Algebras and Coalgebras, Section 11. Bisimulation & behavioral equivalence (前半)

勉強 メモ

代数の congruence に相当する bisimulation と behavioral equivalence について。圏論っぽい雰囲気が漂っていて楽しい節です。ほとんど set functor ですけど。*1

以下、特に断らないかぎり Ω は set functor で \sigma: S \rightarrow \Omega S は Ω-coalgebra とする。添え字や prime がついても同じ。

behavioral equivalence

s ∈ S, s' ∈ S' が behaviorally equivalent であるとは、適当な余代数 X と準同型の組 S \rightarrow X \leftarrow S' があって、これらで s と s' が同じ点にうつること。

と、本には書いてあります。後に出てくる bisimulation の定義を見るに、この図式のことを behavioral equivalence と呼ぶ、みたいな定義があってもいいと思うのですが、それは出てきませんでした。

bisimulation

bisimulation とは B \subset S \times S' であって Ω-coalgebra の構造をもち、両成分への射影 S \leftarrow B \rightarrow S' が準同型となるもののことをいう。ある bisimulation に (s, s') が属するとき、s と s' は bisimilar であるという。

と、本に書いてある定義ではそうなってますが、別に直積集合の部分集合とする必然性はないような。圏論的な観点からいえば、単に同じところからの準同型があればいいということになりそうです。

ちなみに、代数の congruence を似たような方法で定義することもできるという話が出ています。

関係 R \subset A_0 \times A_1 が substitutive であるとは、適当に R に代数の構造を入れて射影が準同型となるようにできることとする。このとき R が substitutive equivalence であることと congruence であることは同値。

面白い。

examples of bisimulation

Kripke frame (for basic modality; P-coalgebra) の余代数としての bisimulation は、普通の意味での bisimulation と同じ。Kripke model でも同様。これはどちらも単純な計算でわかる。

deterministic finite automata の bisimulation B は、次の二つの条件を満たす関係。

  • (s, s') ∈ B ならば s と s' は両方とも受理状態であるか、またはどちらも受理状態でない
  • (s, s') ∈ B ならば、どんなアルファベットが入力されても、s と s' の遷移先はまた B で関連付けられる

coalgebra homomorphism も、写像を二項関係とみなすことで bisimulation になる。これを証明するには、まずグラフから定義域への射影(第一射影)が全単射になっていることに注意する。その逆写像を第二射影と合成するともとの写像になることを使う。

*1:ところで set functor って、集合の圏の endofunctor のことだと思っていいんでしょうか。定義書いてないんですけど。