ユースケースをなんとかする -- 手始め

ユースケース＝サブシステムなんだと思うが、これといってサブシステムの厳密な定義もないしね。

とりあえず、システムはなんらかの状態遷移系だとする。状態遷移系はその遷移グラフで決まるから、ラベル付き有向グラフでシステムを表現することにする。ラベルは頂点ラベル、辺ラベルの両方を認める。ラベリングが要らないなら、単元集合をラベル値の集合にしておけばいい。

システムを表すグラフGは次のものから構成される。

1. 頂点集合 N
2. 辺集合 E
3. 辺の始点と終点 src, trg: E→N
4. 頂点ラベル値の集合 L_N
5. 辺ラベル値の集合 L_E
6. 頂点ラベリング ν : N→L_N
7. 辺ラベリング ε: E→L_E

多重辺もループも認める。有限性の条件は課さない。もう何でもあり。

圏論風に、Gの頂点の集合を |G|、頂点A, Bに対する辺の集合を G(A, B) とする。a∈E が、src(a) = A, trg(a) = B のとき、a:A→B in G と書く。

G = (N, E, ν, ε)、G' = (N', E', ν', ε') のとき、写像 f_N:N→N', f_E:E→E' が次の条件を満たすとき、ラベル厳密保存のグラフ準同型写像と呼ぶ。

• src(f_E(a)) = f_N(src(a))
• trg(f_E(a)) = f_N(trg(a))
• ν'(f_N(A)) = ν(A) forall A∈N
• ε'(f_E(a)) = ε(a) forall a∈E

ラベル値の集合が順序集合のとき、ラベル保存の条件をゆるめて、laxグラフ準同型写像とoplaxグラフ準同型写像を定義する。

lax条件：

• ν(A) ≦ ν'(f_N(A)) forall A∈N
• ε(a) ≦ ε'(f_E(a)) forall a∈E

oplax条件：

• ν'(f_N(A)) ≦ ν(A) forall A∈N
• ε'(f_E(a)) ≦ ε(a) forall a∈E

辺に型をラベリングして、型の包含関係（階層関係）を順序構造にすることは多い。サブシステムの記述と少し違うが、Catyのリソースをノードにするとマッチング階層で順序構造を入れたりもできる。

---

自然数の区間[0, n]をラベリングなし有向グラフ（竹グラフ）とみて、ラベリングを考えないグラフ準同型を長さnの軌道（trajectory）と呼ぶ。グラフGに対して、軌道の全体を Traj(G) とする。始点と終点を決めて、Traj(G)(A, B) のような記法も使う。長さがちょうどn、n以下の軌道は、Trajⁿ(G), Traj^≦n(G) と書く。

ラベリングを忘れて、圏と同様に、広い準同型、充満準同型、忠実準同型、埋め込みなどを定義する。直和と直積も圏と同じに定義する。

中途半端だが、今日はこのへんで。