ラベル付き遷移系のIO結合

IO(入出力）の形式化はけっこう難しい問題です。ここでは、ラベル付き遷移系によるIO（あるいは通信）のモデル化を述べます。XとYがラベル付き遷移系のとき、あるインターフェースを通じてXとYはIO（通信）をします。「Xが出力命令を実行すること」と「Yが入力命令を実行すること」は必ず同時に起こります。2つのラベル付き遷移系において、出力命令と入力命令が同時に実行されることがIO（または通信）ということになります。

内容：

1. ラベル付き遷移系
2. IOインターフェースを持ったラベル付き遷移系
3. IOインターフェースによるIO結合
4. 圏論の観点からの課題

ラベル付き遷移系

SとLは集合、δ:S×L→S は写像とします。3つ組 X = (S, L, δ) をラベル付き遷移系といいます。Sは状態空間、Lはラベルの集合、δが遷移写像です。Lの要素は、アクション記号と呼ばれることもあります。遷移写像δは、部分写像や非決定性写像を許すこともあります。必要があれば、X = (S_X, L_X, δ_X), Y = (S_Y, L_Y, δ_Y) のように、S, L, δ に下付き添字を付けて区別します。

ラベルLが単元集合のときは、δ:S→S と見なせるので、ラベルなしの遷移系です。つまり、ラベルなしの遷移系はラベル付き遷移系の特殊ケースです。状態空間Sが単元集合のときは、δ:L→1 となるので、ラベル集合Lがなんであっても自明な遷移しか起きません。LまたはSのどちらか、あるいは両方が空集合であることも許します。このとき、δは空集合上に存在する唯一の写像です。

IOインターフェースを持ったラベル付き遷移系

X = (S, L, δ) がラベル付き遷移系として、それとは別に集合A, Bがあるとします。i:A→L, j:B→L を単射（埋め込み写像）とします。ラベル付き遷移系Xと、i, jを一緒にした構造を考えましょう。これを改めてXとして、X = (S, L, δ, i, j) と書きます。i:A→L を入力インターフェース、j:B→L を出力インターフェースと呼びましょう。そして、X = (S, L, δ, i, j) は、IOインターフェースを持ったラベル付き遷移系だといいます。

iとjは単射なので、事実上 A⊆L、B⊆L と考えることができます。つまり、AとBはラベル集合Lの一部だと思ってもいいわけです。Lの要素は状態遷移を引き起こす命令（の記号）と考えることができます。特に、Aに属する命令は入力命令、Bに属する命令は出力命令と解釈します。A∩B（正確には、i_X(A)∩j_X(B)）に属する命令は、入力と出力を同時に（一挙に）行うものです。

IOインターフェースによるIO結合

X = (S, L, δ, i, j) がIOインターフェースを持ったラベル付き遷移系で、i:A→L, j:B→L がそのIOインターフェースだとします。このとき、X:A→B と書くことにします。Xを、「集合Aから集合Bへの射」と考えるわけです。A→B であるようなラベル付き遷移系の全体を Hom(A, B) とします。こう書くと、IOインターフェースを持ったラベル付き遷移系の全体が圏を構成するように思えます。実際は、事情はそう単純ではなくて、ストレートに圏を作ることはできません（後述します）。しかし、あたかも圏であるかのように扱うことは有効なので、以下では、X:A→B とか Hom(A, B) のような記法を使うことにします。

2つのIOインターフェースを持ったラベル付き遷移系 X:A→B、Y:B→C があるとき、これらをこの順で結合したラベル付き遷移系を X*Y とします。普通の結合記号「;」でもいいのですが、いつもと違う結合記号にします（深い意味はない）。X*Y をXとYのIO結合と呼びます。*はIO結合演算です。Z := X*Y と置いて、S_Z, L_Z, δ_Z, i_Z, j_Z を具体的に構成します。

まずは状態空間：

• S_Z := S_X×S_Y

単に直積です、簡単ですね。次にL_Z、少し面倒です。

• L_Z := (L_X + L_Y)/〜

+は集合の直和で、〜は同値関係です。この同値関係〜は、だいたい次のように定義されます。以下で、記号＼は集合の差（引き算）です。

1. L_X＼j_X(B) 上では通常の等号
2. L_Y＼i_Y(B) 上では通常の等号
3. j_X(B) と i_Y(B) を同一視する。

L1 := L_X＼j_X(B)、L2 := L_Y＼i_Y(B)、B1 := j_X(B)、B2 := i_Y(B) と置いて表にまとめると：

＼	L1	L2	B1	B2
L1	等号	無関係	無関係	無関係
L2	無関係	等号	無関係	無関係
B1	無関係	無関係	等号	j(b) = i(b)
B2	無関係	無関係		j(b) = i(b)	等号

要するにL_Zは、j_X と i_Y を使って、L_X と L_Y を貼りあわせたものです。

δ_Z は次のようになります。s∈S_X、t∈S_Y、z∈L_Z に対して、δ_Z((x, y), z) を δ_Z(x, y, z) と3変数の形で書くことにして：

1. x∈L1 のとき、δ_Z(s, t, x) := (δ_X(s, x), t)
2. y∈L2 のとき、δ_Z(s, t, y) := (s, δ_Y(t, y))
3. j(b)∈B1 のとき、δ_Z(s, t, j(b)) := (δ_X(s, j(b)) , δ_Y(t, i(b)))
4. i(b)∈B2 のとき、δ_Z(s, t, i(b)) := (δ_X(s, j(b)) , δ_Y(t, i(b)))

L_Zの貼り合わせ構成に対応した定義ですね。

最後に、i_Z と j_Z ですが、これは簡単です。

• i_Z := i_X
• j_Z := i_Y

ただし、i_Z と j_Z の余域はL_Zになるように調整します。

圏論の観点からの課題

X:A→B とか Hom(A, B) のような記法を使ってきましたが、IOインターフェースを持ったラベル付き遷移系の全体が圏になるかと言うと、色々と難しい点があります。それについて述べます。

まず、Hom(A, B) が大きすぎるという問題があります。X:A→B の形をしたラベル付き遷移系の全体は小さな集合にはなりません。通常の圏の定義では、圏全体は大きくても、ホムセットは小さい集合です。ホムセットが大きいままでも議論できるかもしれませんが、扱いやすくはないでしょう。

X∈Hom(A, B) と Y∈Hom(B, C) に対して、それらのIO結合 X*Y を定義したのですが、演算*は、結合法則や（恒等射を適切に定義しての）単位法則が成立しません。結合法則もどき、単位法則もどきは定式化できそうですが、等式的法則としてバッチリ成立しているわけではありません。このことも議論を困難にします。

上記2つの問題はおそらくは関連していて、同時に解決できるかも知れません。Hom(A, B) は単に（大きな）集合ではなくて、それ自体を圏とみなすことができます（ラベル付き遷移系が対象、射を別途定義する）。Hom(A, B) が圏ならば、始対象／終対象を取るとか、up-to-isoを使った同値関係で割り算するなどの方法で、Hom(A, B) を小さくすることが可能です。ただし、単なるラベル付き遷移系ではうまくいかないでしょう。よりリッチな構造であるメイヤー代数が必要そうです。

今まで Hom(A, B) という書き方をしてきましたが、もっと構造化したほうがいいでしょう。i:A→L と j:B→L の組は、集合圏の余スパン (A→L←B) を定義します。集合を対象、余スパンを射とする圏 Cospan(Set) が定義できます。余スパン圏の射を（イイカゲンな記法ですが） L:A→B のように書きましょう。Homは、余スパンの圏をパラメータ域とすると考えられます。

IOインターフェースを持ったラベル付き遷移系とIO結合の定義を振り返ってみれば、X∈Hom(A, B) と書くよりは、X∈Hom(L:A→B) と書くほうがふさわしいと分かります。なぜなら、IO結合演算*は、次のように書けるからです。

• * : Hom(L:A→B)×Hom(M:B→C) → Hom(L;M:A→C)

この状況は、豊饒圏と高次圏を組み合わせれば、うまく表現できそうです。

と、いろいろと課題は多いのですが、IO（通信）を圏論の枠内で考えることは意義があると思っています。