Circ-Kleisli構成のもっといい定式化

子供が起き出す前にメモ。

直接計算で、対称モノイド圏CのTによるCirc-Kleisli圏CK_T(C)を構成できたが、CK_T(C)=Circ(Kleisli_T(C))だともっと都合がいい。実は、最初はそのような構成を目指したが、Kleisli_T(C)にモノイド構造を入れることができなくてあきらめたのだった。

CK構成にはモナドの強度（tensorial strength）を使ったのだが、強度付きならモノイド積が構成できるような気もしてきた。調べてみると、John Power & Edmund Robinson "Premonoidal categories and notions of computation" で既にやっていた。

まずは定義から；τがTの強度だとして、τ' = σ|τ|σ;;T として定義する（通常記法なら Tσ・t・σ）。

τ':: T(A)+B -[σ]→ B+T(A) -[τ]→ T(B+A) -[T(σ)]→ T(A+B)

次の条件を満たすとき、モナド強度は可換だという。

 T(A)+T(B) -[τ]→T(TA+B) -[T(τ')]→TT(A+B) -[μ]→ T(A+B)

 =========================================================

 T(A)+T(B) -[τ']→T(A+TB) -[T(τ)]→TT(A+B) -[μ]→ T(A+B)

John Power & Edmund Robinsonによれば：

• TのKleisli圏C_Tがプレモノイド圏となる ⇔ Tは強度を持つ
• TのKleisli圏C_Tがモノイド圏となる ⇔ Tは可換強度を持つ

つまり、Kleisli圏のプレモノイド構造と強度が1対1に対応している。Circ構成は（おそらく）プレモノイド圏でも通用するだろうから、Circ(Kleisli_T(C))はトレース付きプレモノイド圏になる。これに関しては、Nick Benton & Martin Hylandの"Traced Premonodal Categories"がある。

D=CK_T(C)は、hom-catを持つので二圏となる。A, Bを固定してhom-cat D(A, B)を考えると、CでA×X→T(B×X)なので、Cが閉圏なら、X→[A, T(B×X)]とできる。これは、関手F(X)=[A, T(B×X)]を定義するので、home-cat D(A, B)はFの余代数の圏と考えられる。つまりD(A, B) = Coalg_F(C)。

Cが閉でなくても、Int(CK(C))を構成してコンパクト閉圏が構成できる。CをインスティチューションのSignとしてInt(CK(C))の射こそ、コンポネントを定義するとふんでいる。

一番簡単な例は、ミーリー機械と線形文法（元祖BNF）だから、これを調べよう。