オートマトンの大事な概念と公式

• s-(x, y)→t は遷移（のインスタンス）と言う。s∈S, t∈T でSとTが一致しなくてもよい。
• 遷移（のインスタンス）の集まりを遷移セット、遷移ルール、遷移関係などと言う。
• s-(_, _)→t を無音遷移という。_は無音記号。
• すべての遷移が無音である遷移セットを無音遷移セットという。
• X={_}、Y={_} なら、X >> Y 型の全ての遷移セットは無音になる。
• 遷移セットを射とする圏があり、直和をモノイド積としてトレース付き圏になる。
• 写像 f:A→B は無音遷移セットとして実現できる。
• 関係 R:A→B も無音遷移セットとして実現できる。
• i:A→S, j:B→S, F:S→*S が決めるオートマトンをAut(F, i, j)とすると、F(F, i, j) = i;[Tr_S(Δ;F;∇)];j^t となる。j^tは関係としてのjの転置である。
• 遷移セット（遷移ルール）の圏は、その圏から作ったオートマトンの圏に埋め込める。その意味で、オートマトンの圏はもとの遷移セットの圏の拡張になる。
• 遷移に入出力があれば（無音でなければ）、遷移セットは2セルであり、オートマトンも2セルとなる。

オートマトンよりも前に1ステップの遷移からなる圏があって、そこでトレースを使ってオートマトンを作れるところがミソ。C|→Aut(C) という構成がある。そういえば、昔Circ構成にハマっていたことがある。