順序ベース多圏と名前ベース多圏、シーケント計算

最近、少しだけ多圏の使い方に慣れてきた。多圏はけっこうバリエーションがある。まず、カットの自由度から、シングルカット多圏とマルチカット多圏がある。シングルカットはワイヤー1本に関してカットする。マルチカットは束（たば；リボン）でカットできる。

シーケント計算にならって、多圏の多対象（polyobject）をΓ、Δなどで表す。多対象の長さを|Γ|と書くが、ここでは|Γ|は{1, 2, ..., n}を表すとして、Γの台と呼ぶ。|Γ|⊆Nだが、台は必ず区間の形をしている。

多対象を列ではなくて、レコードにしてみる。名前（キー）の集合Kを固定して、レコード{a1:A1, ..., an:An}を考える。Γ={a1:A1, ..., an:An}のとき、Γの台|Γ|は、名前の集合{a1, ..., an}だとする。

単対象の集合Oと名前の集合Kを固定すると、そこでシーケント計算が定義できる。定数記号×、Iを導入して、A∈Oに対する「A⇒A」と「⇒I」を公理として、次の推論を許す。

 Γ, a:A, b:B, Δ ⇒ Φ

 ----------------------[× 左導入]

 Γ, x:A×B, Δ ⇒ Φ（x!∈|Γ|∪|Δ|）
 Γ ⇒ Φ, a:A, b:B, Ψ

 ----------------------[× 右導入]

 Γ ⇒ Φ, x:A×B, Ψ （x!∈|Φ|∪|Ψ|）
 Γ ⇒ Φ

 -------------[I導入]

 x:I, Γ ⇒ Φ （x!∈|Γ|）
 Γ, a:A Δ ⇒ Φ

 ----------------------[左改名]

 Γ, x:A, Δ ⇒ Φ（x!∈|Γ|∪|Δ|）
 Γ ⇒ Φ, a:A, Ψ

 ----------------------[右改名]

 Γ ⇒ Φ, x:A, Ψ （x!∈|Φ|∪|Ψ|）
 Γ ⇒ Φ   Δ ⇒ Ψ

 --------------------[mix]

 Γ, Δ ⇒ Φ, Ψ （|Γ|∩|Δ| = |Φ|∩|Ψ| = 空）
 Γ, Δ ⇒ Φ, Δ

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

 Γ ⇒ Φ

この計算を多圏の定義に直せば：

1. トレース付きモノイド圏で解釈可能である。
2. 改名の亜群が作用している。
3. モノイド積は条件付きでしか定義できない（部分的になる）。
4. マルチカットを許す

つまり、可置換部分モノイド多圏（permutable partially-monoidal polycategory）とでも呼ぶべき構造になる。カット（結合）はトレースカットから定義できる。