同期通信による結合

以前からなんか釈然としないことがあった。

僕は双ラベル付き関係／遷移系（bilabelled relation/transition system）で、入出力を持つシステムをモデル化しようとしていた。2つのラベル集合A, Bに対して、f:A→B というプロファイルの射を考える。が、なーーんかこれがうまくない。

Lをラベルの集合として、単射の余スパン A→L←B を考えて、普通のLラベル付き遷移系を考える。これを f:A→B と考える。こう考えると、Lの不定性、状態空間の不定性から、Hom(A, B)が巨大な圏になってしまう問題があるのだが、より自然なモデル化ができると思う。

f:A→B, g:B→C の結合は、L←B→M というスパンにより貼り合わせたラベルがf;gのラベル集合となる。何度も出会っている構成法だから違和感はない。セリンガーが使っていたin/outの方法とも整合しそうだし。

あと、同期／非同期を空間化する「時間の空間」概念をもっとはっきりさせる必要がある。