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