構造計算

数理論理学において、構造計算（CoS）は、非可換論理の構造的証明理論を研究するための、深層推論を備えた証明計算体系である。この計算体系はその後、線形論理、古典論理、様相論理、およびプロセス計算の研究に応用され、深層推論が計算体系で利用可能になることで、これらの研究において多くの利点が得られると主張されている。

これは、バース大学のアレッシオ・グリエルモによる論文「相互作用と構造のシステム」で2001年に初めて紹介されました。^{[ 1 ] [ 2 ]}

式とは、（整形式の）論理記号の文字列です。例えば、${\displaystyle ((a\land b)\land \neg c)\lor d}$これは公式です。

等式理論とは、すべての論理式の集合における同値関係を記述する方程式のリストである。一般的な等式としては、結合法則、交換法則、および論理定数に関する等式が挙げられる。

構造とは、論理式の同値類のことである。「構造」という名称は、CoSがシーケントと論理式を区別せず、シーケント計算において単一のオブジェクトを用いて両方の役割を果たすことを強調している。具体的には、構造は論理式の同値類とみなすことができる。

コンテキストとは、サブ構造が削除された構造のことです。例えば、${\displaystyle A\land -}$は、${\displaystyle -}$は削除されたサブ構造を表します。コンテキストは次のように記述されます。${\displaystyle S\{-\}}$例えば、${\displaystyle S\{-\}:=A\land -}$、 それから${\displaystyle S\{B\}}$は次のように定義される。${\displaystyle A\land B}$。

推論規則は次の形式である${\displaystyle {\frac {S\{A\}}{S\{B\}}}}$、 どこ${\displaystyle A,B}$は下部構造であり、${\displaystyle S\{\}}$これは特定の公式ではなく、「どんな文脈でもここに当てはまる」という指示です。これを簡略化して表現すると次のようになります。${\displaystyle {\frac {A}{B}}}$去る${\displaystyle S\{\}}$暗黙的。デフォルトでは、推論ルールに現れるコンテキストは正の極性を持つ必要があります。

文脈には極性があります。文脈の極性は、正または負のいずれかです。たとえば、${\displaystyle A\lor -}$肯定的な文脈ではあるが、${\displaystyle A\lor \neg -}$否定的な文脈ではあるが、${\displaystyle (A\lor \neg -)\to C}$は再び肯定的な文脈です。文脈の肯定性または否定性は極性と呼ばれます。たとえば、私たちは「${\displaystyle A\lor -}$「正の極性を持つ」、そして「${\displaystyle A\lor \neg -}$負の極性を持つ。

2つの構造は互いに双対である可能性がある。同様に、2つの推論規則は${\displaystyle {\frac {S\{A\}}{S\{B\}}},\;{\frac {S\{B'\}}{S\{A'\}}}}$互いに双対になることもできる。${\displaystyle A'}$デュアルとして${\displaystyle A}$、 そして${\displaystyle B'}$デュアルとして${\displaystyle B}$古典的な対位法は、この二重性の例である。

慣例として、${\displaystyle ()}$接続詞として、${\displaystyle []}$選言の場合。例えば、線形論理では次のように書きます。${\displaystyle (A_{1},\dots ,A_{n})}$のために${\displaystyle A_{1}\otimes \dots \otimes A_{n}}$、 そして${\displaystyle [A_{1},\dots ,A_{n}]}$のために${\displaystyle A_{1}\mathbin {\mbox{⅋}} \dots \mathbin {\mbox{⅋}} A_{n}}$。

MLL⁻ を単位のない乗法線形論理の証明システムと定義する。

式は以下から構成される${\displaystyle F::=a|{\bar {a}}|F\mathbin {\mbox{⅋}} F|F\times F}$。 ここ、${\displaystyle a}$そして${\displaystyle {\bar {a}}}$は双対原子である。双対性の式は$${\displaystyle (A\otimes B)^{\bot }=A^{\bot }\mathbin {\mbox{⅋}} B^{\bot },\quad (A\mathbin {\mbox{⅋}} B)^{\bot }=A^{\bot }\otimes B^{\bot }}$$特に、否定はもはや存在しない。なぜなら、否定を論理結合子から、論理原子のペア間の単なる双対性へと格下げしたからである。定義によれば、${\displaystyle {\bar {\bar {a}}}=a}$。

このシステムのCoSは以下のとおりです。^{[ 4 ]}$${\displaystyle {\begin{aligned}&\mathrm {i} \downarrow \;{\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}&&\mathrm {i} \uparrow \;{\frac {A\otimes A^{\perp }}{}}\\&\mathrm {i} \downarrow \;{\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}&&\mathrm {i} \uparrow \;{\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}\\&\sigma \downarrow \;{\frac {S\{A\mathbin {\mbox{⅋}} B\}}{S\{B\mathbin {\mbox{⅋}} A\}}}&&\sigma \uparrow \;{\frac {S\{A\otimes B\}}{S\{B\otimes A\}}}\\&\alpha \downarrow \;{\frac {S\{A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C\}}}&&\alpha \uparrow \;{\frac {S\{A\otimes (B\otimes C)\}}{S\{(A\otimes B)\otimes C\}}}\\&\mathrm {s} \;{\frac {S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}}\end{aligned}}}$$各行は双対ルールのペアです。スイッチルールはそれ自身と双対関係にあります。

開始ルールは4つあり、i↑用が2つ、i↓用が2つです。ルールが1つではなく2つある理由は、このシステムには単位がないためです。${\displaystyle 1,\bot }$ユニットと共に${\displaystyle 1}$のために${\displaystyle \otimes }$単純に包含することができる${\displaystyle {\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}}$特殊なケースとして${\displaystyle {\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}}$、 どこ${\displaystyle S\{-\}}$は空のコンテキストであり、${\displaystyle B=1}$同様に、ユニットでは${\displaystyle \bot }$のために${\displaystyle \mathbin {\mbox{⅋}} }$包含することができる${\displaystyle {\frac {A\otimes A^{\bot }}{}}}$下${\displaystyle {\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}}$。

協会の規則${\displaystyle \alpha }$および整流${\displaystyle \sigma }$これは、両方の結合子が結合法則と交換法則を満たすことを意味します。これらの規則は、次の式に置き換えることができます。${\displaystyle (A\otimes B)\otimes C=A\otimes (B\otimes C)}$など

i↑はシーケント計算における恒等公理に対応する。${\displaystyle A\vdash A}$または同等に、${\displaystyle \vdash A^{\bot },A}$。

i↓ はカットルールに対応します。${\displaystyle {\frac {\Gamma \vdash \Delta ,A\quad A,\Gamma '\vdash \Delta '}{\Gamma ,\Gamma '\vdash \Delta ,\Delta '}}}$。

スイッチルール${\displaystyle {\frac {S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}}}$はより微妙です。それは${\displaystyle S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}\vdash S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}$一般に、CoSの推論規則は、「90度回転させる」ことによって、シーケント計算における証明可能なシーケントとして読み取ることができる。

SLLSシステムは、完全な線形論理のCoSバージョンです。MLL⁻のCoSよりもはるかに大きいです。^{[ 5 ]}$${\displaystyle {\begin{aligned}&\mathrm {ai} \downarrow \;{\frac {1}{a\mathbin {\mbox{⅋}} {\bar {a}}}}&&\mathrm {ai} \uparrow \;{\frac {a\otimes {\bar {a}}}{\bot }}\\&\mathrm {d} \downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\mathbin {\&} (C\mathbin {\mbox{⅋}} D)}{(A\mathbin {\&} C)\mathbin {\mbox{⅋}} (B\oplus D)}}&&\mathrm {d} \uparrow \;{\frac {(A\oplus B)\otimes (C\mathbin {\&} D)}{(A\otimes C)\oplus (B\otimes D)}}\\&\mathrm {p} \downarrow \;{\frac {!(R\mathbin {\mbox{⅋}} T)}{!R\mathbin {\mbox{⅋}} ?T}}&&\mathrm {p} \uparrow \;{\frac {!R\otimes ?T}{?(R\otimes T)}}\\&\mathrm {aw} \downarrow \;{\frac {0}{a}}&&\mathrm {ac} \downarrow \;{\frac {a\oplus a}{a}}&&\mathrm {ac} \uparrow \;{\frac {a}{a\mathbin {\&} a}}&&\mathrm {aw} \uparrow \;{\frac {a}{\top }}\\&\mathrm {nm} \downarrow \;{\frac {0}{0\mathbin {\&} 0}}&&\mathrm {s} \;{\frac {(A\mathbin {\mbox{⅋}} B)\otimes C}{(A\otimes C)\mathbin {\mbox{⅋}} B}}&&\mathrm {m} \;{\frac {(A\mathbin {\&} B)\oplus (C\mathbin {\&} D)}{(A\oplus C)\mathbin {\&} (B\oplus D)}}&&\mathrm {nm} \uparrow \;{\frac {\top \oplus \top }{\top }}\\&\mathrm {nm} _{1}\downarrow \;{\frac {0}{0\mathbin {\mbox{⅋}} 0}}&&\mathrm {m} _{1}\downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\oplus (C\mathbin {\mbox{⅋}} D)}{(A\oplus C)\mathbin {\mbox{⅋}} (B\oplus D)}}&&\mathrm {m} _{1}\uparrow \;{\frac {(A\mathbin {\&} B)\otimes (C\mathbin {\&} D)}{(A\otimes C)\mathbin {\&} (B\otimes D)}}&&\mathrm {nm} _{1}\uparrow \;{\frac {\top \otimes \top }{\top }}\\&\mathrm {nm} _{2}\downarrow \;{\frac {0}{0\otimes 0}}&&\mathrm {m} _{2}\downarrow \;{\frac {(A\otimes B)\oplus (C\otimes D)}{(A\oplus C)\otimes (B\oplus D)}}&&\mathrm {m} _{2}\uparrow \;{\frac {(A\mathbin {\&} B)\mathbin {\mbox{⅋}} (C\mathbin {\&} D)}{(A\mathbin {\mbox{⅋}} C)\mathbin {\&} (B\mathbin {\mbox{⅋}} D)}}&&\mathrm {nm} _{2}\uparrow \;{\frac {\top \mathbin {\mbox{⅋}} \top }{\top }}\\&\mathrm {nl} _{1}\downarrow \;{\frac {0}{?0}}&&\mathrm {l} _{1}\downarrow \;{\frac {?R\oplus ?T}{?(R\oplus T)}}&&\mathrm {l} _{1}\uparrow \;{\frac {!(R\mathbin {\&} T)}{!R\mathbin {\&} !T}}&&\mathrm {nl} _{1}\uparrow \;{\frac {!\top }{\top }}\\&\mathrm {nl} _{2}\downarrow \;{\frac {0}{!0}}&&\mathrm {l} _{2}\downarrow \;{\frac {!R\oplus !T}{!(R\oplus T)}}&&\mathrm {l} _{2}\uparrow \;{\frac {?(R\mathbin {\&} T)}{?R\mathbin {\&} ?T}}&&\mathrm {nl} _{2}\uparrow \;{\frac {?\top }{\top }}\\&\mathrm {nz} \downarrow \;{\frac {\bot }{?0}}&&\mathrm {z} \downarrow \;{\frac {?R\mathbin {\mbox{⅋}} T}{?(R\oplus T)}}&&\mathrm {z} \uparrow \;{\frac {!(R\mathbin {\&} T)}{!R\otimes T}}&&\mathrm {nz} \uparrow \;{\frac {!\top }{1}}\end{aligned}}}$$

$${\displaystyle {\begin{aligned}A\otimes B&=B\otimes A&\qquad (A\otimes B)\otimes C&=A\otimes (B\otimes C)&\qquad A\otimes 1&=A\\A\mathbin {\&} B&=B\mathbin {\&} A&(A\mathbin {\&} B)\mathbin {\&} C&=A\mathbin {\&} (B\mathbin {\&} C)&A\mathbin {\&} \top &=A\\A\oplus B&=B\oplus A&(A\oplus B)\oplus C&=A\oplus (B\oplus C)&A\oplus 0&=A\\A\mathbin {\mbox{⅋}} B&=B\mathbin {\mbox{⅋}} A&(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C&=A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)&A\mathbin {\mbox{⅋}} 1&=\bot \\??R&=?R&!!R&=!R\\\bot \oplus \bot &=\bot =?\bot &1\mathbin {\&} 1&=1=!1\end{aligned}}}$$

このCoSによりBVシステム（基本システムV）を生成できます：^{[ 1 ]}$${\displaystyle {\begin{aligned}&\mathrm {ai} \downarrow \;{\frac {\circ }{a\mathbin {\mbox{⅋}} {\bar {a}}}}&&\mathrm {ai} \uparrow \;{\frac {a\otimes {\bar {a}}}{\circ }}\\&\mathrm {s} \;{\frac {(A\mathbin {\mbox{⅋}} B)\otimes C}{(A\otimes C)\mathbin {\mbox{⅋}} B}}\\&\mathrm {q} \downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\triangleleft (C\mathbin {\mbox{⅋}} D)}{(A\triangleleft C)\mathbin {\mbox{⅋}} (B\triangleleft D)}}&&\mathrm {q} \uparrow \;{\frac {(A\triangleleft B)\otimes (C\triangleleft D)}{(A\otimes C)\triangleleft (B\otimes D)}}\end{aligned}}}$$

$${\displaystyle {\begin{aligned}A\otimes B&=B\otimes A&\qquad (A\otimes B)\otimes C&=A\otimes (B\otimes C)&\qquad A\otimes \circ &=A\\A\mathbin {\mbox{⅋}} B&=B\mathbin {\mbox{⅋}} A&(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C&=A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)&A\mathbin {\mbox{⅋}} \circ &=A\\&&(A\triangleleft B)\triangleleft C&=A\triangleleft (B\triangleleft C)&A\triangleleft \circ &=A=\circ \triangleleft A\end{aligned}}}$$

• カイ・ブリュンラー（2004）。古典的証明における深層推論と対称性。ロゴス出版。

• 構造計算ホームページ
• Maude の CoS : Maude システムを使用して、構造の計算における論理システムの実装を文書化したページ。