一様性原理と模倣／双模倣

クリーネ圏（Kleene圏）では、スター帰納法が基本になる。

 f:X→X, ψ;X→Y,  f;ψ ≦ ψ

 -----------------------------

 Rep(f);ψ ≦ ψ : X→Y
 g:Y→Y, ψ;X→Y,  ψ;g ≦ ψ

 -----------------------------

 ψ;Rep(g) ≦ ψ : X→Y

これから次の一様性原理が出る。

 f:X→X, g:Y→Y, ψ;X→Y,  f;ψ = ψ;g

 --------------------------------------

 Rep(f);ψ  = ψ;Rep(g) : X→Y

よって、半加法的クリーネ圏は、全一様性を持つコゥゼン圏（Kozen圏）となる。問題はその逆だが、等式的な一様性原理から不等式である帰納法を出すのは困難な気がしてきた。それなら、トレースに関して、不等号で定式化される帰納原理を考えたほうがいいのではないか。 Tr(f) ≦ Tr(g) となるようなヤツ。

山勘では、模倣／双模倣が事例になるような気がする。バーグストラ、ステファネスクとかに書いてあるか？

• "Bisimulation is Two-Way Simulation" (1994) by Bergstra, Stefanescu （http://citeseer.ist.psu.edu/58109.html）
• "Studying Equivalences of Transition Systems with Algebraic Tools" (1995) by Pasquale Malacaria（http://citeseer.ist.psu.edu/489182.html）

を読んでみよう。