遷移翻訳系モデルに細かい工夫をする

遷移翻訳系（トランスデューサ;transducer, XDCR）を圏を考える際に、細かい工夫をすると議論がスムーズになることに気が付いた。それらの工夫とは：

1. アルファベット（基本記号集合）を点付き集合（pointed set）と考え、クリーネスター・モナドを点付き集合の圏Set_●上で考える。
2. ラベル付き遷移系の拡張として定義した入出力遷移系 X:A→B （X⊆S×(A×B)×S）の圏の上にクリーネスター・モナドを構成する。そのKleisli圏を考える。
3. マルチポート、マルチアルファベットに対してマクロ記号（マクロ信号）という概念を使う。
4. エルゴット（Elgot）遷移パスによるトレース

点付き集合上のクリーネスター

Set_●を点付き集合の圏とする。基点は常にτと書く。τは、インフォーマルには無音記号と解釈する。A∈|Set_●|に対して、A＼{τ} = A' と書くことにする。A^(*) = {τ}∪(A')⁺と定義して、モノイド演算・を次のように定義する。α、β∈(A')⁺：

1. τ・τ = τ
2. τ・α = α
3. α・τ = α
4. α・β = αβ （連接）

定義から、モノイドとして A^(*) ≒ (A')^*である。

この定義のメリットは、1 = {τ} が始対象兼終対象（つまり零対象）となり、1が×と＋の単位にもなる点である。(f:A→B)∈Set_● にもf^(*)を定義できる。普通のクリーネスターと同様に、(-)^(*)もモナドになる。

入出力付き遷移系のクリーネスター

A, Bが点付き集合として、特別なラベル付き遷移系 X⊆S×(A×B)×S が入出力付き遷移系である。X:A→B と書く。状態空間を明示したいときは X:A→B (S) とする。Xを頂点集合がSであるグラフと考え、グラフXから生成されたパス圏（自由圏）をX^(*)とする。ただし、次の点は注意を要する。

1. すべての頂点sに対して、τ/τ（入力τ、出力τ） でラベルされたループ辺s→sを付け加える。（あるいは最初から付いていると仮定する。）
2. このループ辺をid_sとして扱う。

(-)^(*)で定義されたモナドでKleisli圏を考えることができる。その射は、A→B^(*)という入出力遷移系である。

マルチアルファベットとマクロ記号

A_i∈|Set_●|として、列[A₁, ..., A_n]をマルチアルファベットと呼び、マルチアルファベットで型付けされたポートセットを（型付き）マルチポートと呼ぶ。

列[A₁, ..., A_n]に対して、[A₁, ..., A_n]^# := (A₁)^(*)×...×(A_n)^(*) と定義する。空列に対しては、[]^# := {τ} とする。空列の場合も含めて、マルチアルファベットに対する(-)^#の値は|Set_●|に入ることが重要。（実際には、マルチアルファベットのモノイド圏が定義できて、(-)^#は関手となるはず。）

Σ = [A₁, ..., A_n]がマルチアルファベットのとき、Σ^# = [A₁, ..., A_n]^# := (A₁)^(*)×...×(A_n)^(*)を、マルチアルファベットΣのマクロアルファベットと呼び、その元はマクロ記号と呼ぶ。マクロアルファベットは定義より点付き集合となるので、マクロアルファベットに対する入出力付き遷移系が考えられる。

エルゴット（Elgot）遷移パス

T:A×X→B×X が入出力付き遷移系だとする。Tの状態空間を|T|として、T⊆|T|×[(A×X)×(B×X)]×|T| である。Tの元を遷移規則または遷移ステップと呼ぶ。遷移ステップの連続した列を遷移パスと呼ぶ。入出力を in/out で書くとして、次の形の遷移パスをエルゴット遷移パスと呼ぶ。

1. (a, τ) / (b₁, x₁) a∈A, b₁∈B, x₁∈X
2. (τ、x₁) / (b₂, x₂)
3. (τ、x₂) / (b₃, x₃)
4. 以下同様

エルゴットパスは無限パスだが、終局的に (τ, τ) / (τ, τ) の連続となるパスは安定エルゴットパスと呼ぶ。

(a, τ)の入力の前に、(τ, τ)という入力がn回続いた形をしたエルゴットパスは、遅れnのエルゴットパスと呼ぶ。一般には、すべての遅れを持ったエルゴットパスを考える必要がある。入力がa∈Aであるエルゴットパスとは、ある遅れを持った(a, τ)を入力とするエルゴットパスのことである。エルゴットパスの各遷移で出力されるBの記号をすべて連接したものは、このエルゴットパスの出力と呼ばれる。

エルゴットパスによる入出力は、Tのコピーの長い列を使ってエミュレートできる。