janusのシーケント計算

参考：

• 対称モノイド圏のシーケント計算 - 檜山正幸のキマイラ飼育記 メモ編
• 順序ベース多圏と名前ベース多圏、シーケント計算 - 檜山正幸のキマイラ飼育記 メモ編
• レコード形式指標に対するセオリーとシーケント - 檜山正幸のキマイラ飼育記 メモ編

janusコンポネントのプロファイルは、「ポート名:ポート型」を使って、

• {a1:A1, ..., an:An ; b1:B1, ..., bm:Bm}⇒{x1:X1, ..., xs:Xs ; y1:Y1, ..., yt:Yt}

と書ける。これはまた、次のようにも書ける。

• +a1:A1, ..., +an:An, -b1:B1, ..., -bm:Bm ⇒ +x1:X1, ..., +xs:Xs, -y1:Y1, ..., -yt:Yt

次のような推論で、プロファイル＝シーケントの計算が出来るだろう。なお、前件、後件はそれぞれ、フロントフェイス、バックフェイスと呼ぶ。

 Γ, ±a:A Δ ⇒ Φ

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

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

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

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

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

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

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

 Γ ⇒ Φ
 Γ ⇒ Δ, Σ   Σ, Φ ⇒ Ψ

 ----------------------------[traditional cut]

 Γ, Φ ⇒ Δ, Ψ
 Γ⇒A,Δ

 ----------[*導入 左]

 A*,Γ⇒Δ
 Γ,A⇒Δ

 ----------[*導入 右]

 Γ⇒Δ,A*