多圏上のシーケント計算

シーケント計算は、別に論理と考える必要はなくて、単なる計算法と割り切ったほうがいいようだ。

トレース付き対称多圏（traced symmetric polycategory）を考えることはできる。そこでの計算はシーケント計算が便利。まずは、トレースによるカット（trace-cut）を基本推論として導入する。

  Γ, x ⇒ Δ, x

 ----------------[trace]

    Γ ⇒ Δ

トレース・カットを使って伝統的なカットを導いてみる。

 Γ ⇒ Δ, x   x, Φ ⇒ Ψ

 -------------------------[monoidal product]

 Γ, x, Φ ⇒ Δ, x, Ψ 

 -------------------------[symmetry]

 Γ, Φ, x ⇒ Δ, Ψ, x

 -------------------------[trace]

   Γ, Φ ⇒ Δ, Ψ
 i.e.
 Γ ⇒ Δ, x   x, Φ ⇒ Ψ

 ==========================[cut]

   Γ, Φ ⇒ Δ, Ψ

これって、f;g = Tr[(f×g);σ] のことだ！

命題変数に順序が入れば、それから公理系を作れる。図形的には有向グラフから多圏を作って、その上でシーケント計算することになる。極性（polarity）は否定（negation）として解釈することもできるだろうし、ベキがあればそれはimplicatioになる。

そういや、白旗さんも線形論理の文脈でコンパクト閉圏を持ち出していたし、線形分配圏（多圏）も線形論理から来ていた。線形論理には近付きたくなかったのだが、なんか引き寄せられているような、、、