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

昨日の続き。Ω は set functor で $\sigma: S \rightarrow \Omega S$ (や、その添え字のついたやつら) は Ω-coalgebra とします。

relation lifting

ここからさらに圏論の香りが強くなります。嬉しい。

関係 $R \subset S_0 \times S_1$ の relation lifting とは、図式 $S_0 \leftarrow R \rightarrow S_1$ を Ω で写した $\Omega S_0 \leftarrow \Omega R \rightarrow \Omega S_1$ から定まる $\rho_R : \Omega R \rightarrow \Omega S_0 \times \Omega S_1$ の像のこと。これを $\overline \Omega (R)$ と書く。

そうすると、二つの点 $s_0 \in S_0, s_1 \in S_1$ が bisimilar であるのは $(\sigma_0(s_0), \sigma_1(s_1)) \in \overline \Omega (R)$ となるときかつそのときに限る。このことと $\overline \Omega$ が (集合の包含関係について) 単調であることを使うと、bisimulation 全体が (set-theoretic union を join とする) 完備束になっていることがわかる。特に bisimulation の中で包含関係について最大のものがあり、これが bisimilarity relation (何らかの bisimulation で関係付けられる対全体) である。

この次に、具体的な関手については relation lifting が書き下せるということで Kripke polynomial functor について書き下したものが載っていました。powerset functor の場合は普通の bisimulation の定義で見たような条件が出てきます。具体的にどうなるかは単に手を動かすだけでわかるので、わざわざここに写すこともないでしょう。省略。

bisimilarity implies behavioral equivalence

二つの状態が bisimilar であれば、behaviorally equivalent である。

証明。二つの状態 $s_0 \in S_0,\; s_1 \in S_1$ ]が bisimilar ならば、適当な Ω-coalgebra B があって $S_0 \leftarrow B \rightarrow S_1$ で両者が同じところから来るようなものが存在する。その pushout $S_0 \rightarrow X \leftarrow S_1$ *1 をとれば、これらの状態は (同じ B の点の像になっているから) X で一致する。したがって behaviourally equivalent である。

ちなみに X は普通に直和を割れば作れます。余代数の構造がきちんと入ることの確認を忘れずに。

functors preserving weak pullbacks

weak pullback を保存するような Ω については、その余代数の bisimulation がいくつかのよい性質を持っているというお話。

一つ目は、Ω-coalgebra の bisimulation は合成で閉じているという性質。これは $S_0 \leftarrow B \rightarrow S_1$ と $S_1 \leftarrow B' \rightarrow S_2$ が bisimulation のとき、合成は $B \rightarrow S_1 \leftarrow B'$ の集合の圏での pullback になっていることに注意すればわかる。

もう一つは、そのような Ω については bisimilarity と behavioral equivalence が一致するということ。もし behavioral equivalence を与える図式 $S_0 \rightarrow X \leftarrow S_1$ が与えられれば、その (集合の圏での) pullback が Ω の性質から余代数の構造をもち、必要な可換性を満たす。

ちなみに weak pullback を保存する関手の例としては Kripke polynomial functors が挙げられています。さらに polynomial functor であれば (weak でない) pullback も保存します。教科書に実際に例として出てきた関手はこれくらいのクラスに入っているものが多いようです。

*1:のようなもの。集合の圏の pushout に Ω-coalgebra の構造が入って図式が可換になることは確認しましたが、Ω-coalgebra の圏で pushout になるかどうかは確認してません。