モノイド圏からシーケント計算の作り方

一気にドカッと書こうと思っていたけど、無理そうだからチマチマ書こう、っと。

モノイド圏からハロ多圏を作って、そのハロ多圏上でシーケント計算を作る処方箋が分かってしまったよ、ムフムフ。

もとになるモノイド圏だが、これにはいろいろなオペレータが付いていてもいい。主に考えるオペレータは：

1. ラムダオペレータ（抽象、カリー化、指数、閉性）
2. コンウェイ（Conway）流不動点オペレータ
3. トレース

の3つだ。カザネスク／ステファネスク／ハイランド／長谷川の定理によれば、デカルト圏では不動点オペレータとトレースが同値だが、一般的文脈では違うオペレータになる。

他にアクセサリー的なオペレータとして：

1. 対角Δ
2. 余対角（和）∇
3. ブレイディングβ
4. クロス（対称ブレイディング）σ
5. 放電器!
6. ボトム⊥

など。放電器!とボトム⊥は、記号も概念の由来も違うが双対的。対角と余対角ももちろん双対。

オペレータの挙動が基本推論規則となるので、これらのさまざまなオペレータ、その組み合わせによりシーケント計算も変わる。また、オペレータ（恒等や結合もオペレータとみなす）の推論系としての定式化も、公理、構造規則、論理規則のどれにするかはすごくバリエーションがある。好みが相当入っててしまう。まー、それはいいとしよう。

プレーンな（アクセサリ的オペレータを持たない）モノイド圏では、次の定式化が必要。

1. Aごとの恒等
2. 結合
3. モノイド積
4. モノイド単位

「普通な感じ」で定式化すれば：

1. 恒等は公理（公理シェマ）
2. 結合は左cutと右cutの構造規則
3. モノイド積は論理規則
4. モノイド単位は、定数Iに関する増と減

「定数Iに関する増と減」は構造規則なのか、論理定数の導入消去規則なのかビミョー、まーどうでもいいけど。

推論規則を記述するとき、射（多射）というよりは対象（多対象）を変形することがある。このタイプの規則は略記ができると便利。それで、右側半規則、左側半規則、両側半規則という概念と記法を入れたい。例えば：

   A, B

  -------[両:∧導入]

   A∧B

これは両側半規則で、次のような規則に書き換えて（展開して）よい。

  Γ, A, B, Δ ⇒ Φ

  -------------------

  Γ, A∧B, Δ ⇒ Φ

  Δ ⇒ Φ, A, B, Ψ

  -------------------

  Δ ⇒ Φ, A∧B, Ψ

半規則の意味は多射である。その多射を前結合（多圏の部分結合だが）または後結合することにより、射に関する規則が得られる。左半規則は下から上に読み、前結合により規則を得る。右半規則は上から下に読み、後結合により規則を得る。両側半規則は同型でなくてはならない。

仮定なしでシーケントが証明できれば、そのシーケントが意味する多射がハロ多圏に存在することを保証する。あるいは、そのシーケントが真空から生まれることを保証する。仮定があるなしに関わらず、証明は、多射を1セルとする高次多圏において2セルになる。よって、証明を対象とした計算は2セルの計算になる。恒等証明、証明の部分結合、証明の並置（形式的モノイド積）などは2セル＝証明に対するオペレータ。そして、cut消去など、証明の変形は3セルになる。