うーん、よくわからん。
なにがよくわからんかを、よくわかるように書いておくと、後でわかるかもしれないから書いておこう。
tranceducer（「遷移翻訳系」と僕は意訳しているが）をインスティチューション（institutions）で扱いたいのだ。
Aを入力、Bを出力、Xを状態空間とするtransducerはf:A×X→B×X in Set で記述できる。transducerの圏は、SetからのCirc構成で、feedback付き圏になる。このままではtracedにならないが、タイミング（フィードバックの遅れ）をうまく処理すれば、たぶんtracedになる。さらにInt構成すれば、コンパクト閉圏になるはず。
transducerの圏は、二圏（traditional 2-category）でもあるけど、この二圏構造はコンパクト閉圏のほうにもうまく持って行けるのだろうか？たぶん持って行ける。コンパクト閉二圏ができるだろう。
と、そこまではなんとなくわかる。で、インスティチューションを使って考える。transducerを記述する指標Σは、入力指標ΣI + 出力指標ΣO + 状態指標ΣS のような形をしているのだろう。これを、(ΣI→Σ←ΣO)という余スパンだと思いたい。指標Σ上に適当なセオリーTがあれば、Tのモデル圏Mod(Σ, T)を考えることができる。特に、Mod(Σ) = Mod(Σ, 0)が考えられる。Mod(Σ)が実はtransducer二圏のhom圏ならうれしい。
モデル圏が二圏のhom圏に対応してるのは（それがほんとうなら）おいしい話だ。が、じゃ、入力指標ΣIや出力指標ΣOに対しても、モデル圏Mod(ΣI)、Mod(ΣO)が考えられるが、これは何だ？ 意味不明だ。
あー、うまく対応しない。そもそも、transducerは割と簡単でハッキリしたものだし、インスティチューションはやたらに一般的な枠組みだから、まだギャップがあるのだろう。インスティチューションの指標圏を非常に具体的に決めてかからないと何もわからないのかもしれない。
とりあえず、指標をプロパティ（アクセッサ）、アクション（ミューテータ）、イベントに分けてみるか。アクションとイベントは極性で区別される。文はとりあえず、PreCond, Actions, Events, PostCondの4つ組とする。ActionsかEventsのどちらかが省略されると、両端が論理式でガードされた列になる。これで、言語理論と繋がるような気がするが、、、。
4つ組p{α/β}qに対する命題ホーア論理のような推論規則が必要だ。次は必要だろう（ないと辛い）。
- |- p{/}p
- p{α/β}q, q{η/ξ}r |- p{α;η/β;ξ}r
- p'⇒p , p{α/β}q |- p'{α/β}q
- q⇒q' , p{α/β}q |- p{α/β}q'
α、βなどは列言語と考えて、それなりの規則も要るだろう。たとえば：
- p{α/β}q, p{η/ξ}q |- p{(α|η)/(β|ξ)}q
で、とりあえず、transducerやオートマトンの議論は、インスティチューションのなかで再現できなくてはならない。例えば、列文法は、インスティチューションのセオリーにエンコードできないといけない。それくらい出来ないと、ハナシにならないよな。
