模倣と一様性
このエントリーの言葉使いは、セリンガーに従う（Categorical Structure of Asynchrony）。
まず、双模倣と単なる模倣、それと2方向模倣は別な概念なんだけど、僕はよくわかってない。セリンガーは双模倣（bisimulation, bisimilar）を扱っているが、ここでは片方向の模倣（simulation, simulable）を考える。
とりあえず、強模倣と弱模倣の定義。ラベル付き遷移系があって、アルファベットに無音記号（silent, unobservable なsymbol, label）があるとする。
遷移系Sが、関係Rにより遷移系Tを強模倣できる（strongly simulable, can simulate strongly）とは、無音記号も含む任意のα, t, t' に対して、上の図のような遷移 s -(α)-> s' in S が存在すること。
弱模倣を定義するには、s -*-> s' と s =(α)=> s' の概念が必要。
- s = s' であるか、sからs'への無音記号だけの遷移列が存在するなら s -*-> s'
- αが無音記号なら、s =(α)=> s' は s -*-> s' のこと、
- そうでないなら、s -*-> s0 -(α)-> s1 -*-> s' となるs0, s1 があるとき s =(α)=> s'
遷移系Sが、関係Rにより遷移系Tを弱模倣できる（weakly simulable, can simulate weakly）とは、無音記号も含む任意のα, t, t' に対して、上の図のような遷移 s =(α)=> s' in S が存在すること。
弱模倣を単に模倣と呼び、関係Rを模倣関係（simulation relation）と呼ぶ。
初期状態（initial state）が1点として指定されている遷移系 (s0, S) , (t0, T)で、(s0, t0)∈R である模倣関係Rがあれば、初期状態付き遷移系における模倣概念になる。
セリンガーの用語で"Hasegawa's uniformity property of traces" とは、トレース付きモノイド圏Cにモノイド部分類（monoidal subclass）Uが付いている状況で、「とあるh∈Uに対して f;(h + X) = (h + Y);g ならば Tr(f) = Tr(g)」が成り立つことである。
- セリンガーはUをモノイド部分圏としているが、長谷川さん自身は圏でない例を出している。
- Uに属する射は一様射（uniform morphism）と呼ぶ。
- この性質を持つトレース、またはトレース付き圏に、一様（uniform）という形容詞を付ける。uniformly traced も使う。
- 一様性（uniformity）は、類Uに対して相対的（with respect to U）に定義される。
- トレースの等しさを主張する命題は、一様性原理（uniformity principle）とも呼ばれる。
- 一様性原理は証明原理で、帰納法（induction）に近い。つまり、一様性原理≒帰納法の原理
- 一様トレース付き圏では、一様性原理を使った証明ができる。
圏Cがトレース付き圏で、さらに順序で豊穣化されているとする。そのとき、
- とあるh∈Uに対して f;(h + X) ⊆ (h + Y);g ならば Tr(f) ⊆ Tr(g)
も一様性原理と呼ぶ。一様射が二重圏の垂直射で与えられる状況が面白いだろう。不等号を2セルで与えれば、もっと一般化できるが、いまんところ事例がない。
