System(Γ, Σ)の具体例：翻訳系
とにかくメモ、しゃべるようにメモじゃ。
インスティチューションのMod関手を一般化したい。指標Σ、Γと指標射φがあるとき、Mod(φ): Mod(Γ)→Mod(Σ) となるが通常のMod関手だが、Modを2引数Mod(Γ, Σ)にしたいのだが、混乱をさけるため2引数のバージョンはSystem(Γ, Σ)と書くことにする。直観的には、System(Γ, Σ)のメンバー（射, 1セル）は、Γの実装を渡されてΣを実現するような実行系である。
System(Γ, Σ)はそれ自身が圏になっている。Systemの全体は2-圏。2-圏／双圏の定義はいつまでも憶えられないけど、とりあえず、hom-setスタイルの圏の定義をcat-enrichしてみよう -- つまり、hom-catスタイルで定義する。
セルと結合の記法
| Sign | = S と略記する。Sが0セルの集合になる。通常の習慣とは違い、0セルをΣ, Γなどで表し、1セルをA, Bなど、2セルをα、βなどとする。0セル -- 指標または仕様、1セル -- 実行系、2セル -- 実行形のあいだの変換＝準同型、と意味づけられる。2セルに関しては、 α: A→B :: Γ→ Σ のような記法を使おう。これは、A:Γ→ Σ, B:Γ→ Σ, α:A→B をまとめて書いただけのこと。対応するペースティング図式を思い出せば自然な記法だと思う。 |
2セルの縦結合と横結合をどう書き表すか？で非常に悩む。僕は、このての記法が異常に気にかかる性分だからなぁー。α:A→B :: Γ→Σ と β:B→C :: Γ→Σ の縦結合は、α;βが自然だろう。んんんん、横結合はパイプ記号|にしようかな。んんんん、とりあずそれでいこう。α:A→B :: Σ→Γ、ξ:X→Y :: Γ→Δ として、α|ξ: A;X → B;Y :: Σ→Δ となる。2セルの縦結合と1セルの通常結合が同じ「;」だけど、、、、んんんん、いいとしよう。
Systemのhom-cat
んで、肝心の具体例。
Signは集合の圏とする。Sは集合の類。直観的には、集合をアルファベットとみなす。1セルA:Γ→Σは、決定性の翻訳系（トランスデューサ）とする。Aの状態空間を同じAで表すとして、翻訳写像は、A×Γ → A×Σ* となる。
翻訳写像の状態遷移部分はtA:A×Γ→A 、出力部分はoA:A×Γ→Σ*で表す。翻訳写像の全体はタプル(tA, oA)で書ける。Aがシングルトンのときは、t:Γ→Σ*となるから、単なる関数になる。
入力アルファベットがΓ, 出力アルファベットがΣである翻訳系の圏をSystem(Γ, Σ)とする。翻訳系の射は状態空間の写像α:A→Bで翻訳写像の効果を保つものである。この圏の定義は、ΓとΣを固定すると（そのΓ、Σごとに）局所的に与えられる。
0, 1セルが作る圏の定義
次に、通常の結合「;」をSystem(Γ, Σ)とSystem(Σ, Δ)に対して与えなくてはならない。Kleisli圏の構成と似た方法を使う。補助定理からはじめる。
Zが状態空間だとして、翻訳写像 Z×Σ→Z×Δ*があるとき、この定義域をZ×Σ*に自然に拡張できる。それには、まずZ×Σ*→Z×(Δ*)*に拡張する。拡張に~を付けて示すと：
- tZ~(z, σ1σ2...σn) = tZ(...(tZ(tZ(z, σ1), σ2)...), σn)
- oZ~(z, σ1σ2...σn) = oZ(z, σ1)oZ(tZ~(z, σ1), σ2) ... oZ(tZ~(z, σ1...σn-1), σn)
記号法を工夫すれば、もう少しわかりやすく表記できる。状態zにσが入力されたときの遷移先をz*σとして、出力をz^σとする。
- z*(σ1σ2...σn) = (...((z*σ1)*σ2)...)*σn
- z^(σ1σ2...σn) = z^σ1 (z*σ1)^σ2 ... (z*(σ1...σn-1))^σn
演算子*を左結合的に使い、z=z0, z*σ1 = z1, z*(σ1σ2) = z2などの略記を使うと：
- z*(σ1σ2...σn) = z*σ1*σ2*. ..*σn
- z^(σ1σ2...σn) = z0^σ1 z1^σ2 ... zn-1^σn
要するに、けっこう自然な概念だ。
Z×Σ*→Z×(Δ*)*からZ×Σ*→Z×Δ*に落とすには、(Δ*)*→Δ*という自然な写像を使う。拡張してから落とすのは、モナドに対するKleisli構成と同じである。
やっと準備ができた。A∈System(Γ, Σ)、X∈System(Σ, Δ)だとする。翻訳写像は、A×Γ→A×Σ*、X×Σ→X×Δ*である。新しい状態空間を Z=A×X とする。X×A×Γ→X×A×Σ*の拡張は自明にできる。直積の順序を交換すればZ×Γ→Z×Σ*となる。A×X×Σ→A×X×Δ*が自明な拡張とすれば、これは何もしなくてもZ×Σ→Z×Δ*である。
Z×Γ→Z×Σ*、Z×Σ→Z×Δ*が用意できた。先の拡張可能性定理を使って、Z×Σ*→Z×Δ*と拡張する。Z×Γ→Z×Σ*とZ×Σ*→Z×Δ*は普通に結合できるから、結合して、Z×Γ→Z×Δ* が得られる、これは System(Γ, Δ)に入る。
Γの恒等写像は状態空間をシングルトンにとって、Γ→Γ*を自然な埋め込みにとればよい。あとは圏の公理を確認する（省略）。
2セルの横結合
残るは2セルの横結合|の定義だ。
α:A→B :: Γ→Σ、 ξ:X→Y :: Σ→Δ として、A;Xの状態空間はA×X、B;Yの状態空間はB×Yとなる。αとξは状態空間の変換 A→BとX→Yなのだから、A×X→B×Yは、写像の直積として定義できる。この直積写像をα|βと定義する。
横結合の結合律、単位律、縦結合との交替律は、まー、たぶん成立するだろう。
課題
とりあえず、はしょったところをきちっと埋める。
この例は決定性だが、非決定のときも考える。非決定の定式化で、Pow(A×Σ*)を使うのと、Pow(A)×Pow(Σ*)を使うのでは事情が変わる。Pow(A)×Σ*もあり得る。A×Pow(Σ*)もあるな。そういうバリエーションをどう説明するのか？
インスティチューションの立場から言えば、SignとSystemの関係が問題。|Sign| = |System|という関係では寂しすぎる。ModとSystemの関係をハッキリさせる。SystemからModが定義できるような気がする、そのはずだ。
翻訳系の例で、Sen(Σ)とかProg(Σ, Γ)とは何だ？ TermモナドにあたるのがKleeneスターモナドとか言語モナドなのか？
翻訳系では観測がないので、観測理論が使えないし、終対象も作れない（いや、作れるのか？）。観測付きの翻訳系の場合まで拡張しよう。
翻訳系はオートマトンとの関係があるはずだが、ハッキリしない。
状態空間を集合圏で考えているが、一般の対称モノイド圏ではどうなるの？
Circ構成やKleisli構成に似た構成が出てくるんだけど、これはどうして？やっぱり強モナドが背後にあるのかな？
1セルの圏はコンパクト閉圏にできると思う。向きが付いたコボルディズムと同じような絵が描けるはず。
