線形論理の変種

ウィキペディア小見出し辞書

線形論理の変種

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/11/16 14:33 UTC 版)

「線形論理」の記事における「線形論理の変種」の解説

線形論理には、様々な限定バージョンや変種が存在する。その1つは、古典/直観論理の軸に沿った変種である。古典線形論理 (CLL) は Girard が最初に提唱した線形論理である。CLL では、全ての結合子には双対が存在する。以下は、CLL をシークエント計算で表したものである。 証明は全てカット規則を使わない形に変換できる。 線形含意はこの表には出ていないが、線形否定と乗法的論理積を使えばCLLでも A ⊸ B ≡ A⊥ ⅋ B と定義できる。これは古典論理ではお馴染みの形である。例えば、普通の含意 ⇒ は、A ⇒ B ≡ ?A⊥ ⅋ B と定義できる。 このような定義はもちろん「線形否定」の記法を必要とするが、古典論理では双対を使うこともできる。A の双対は A⊥ と記述され、以下のように定義される。 (A ⊗ B)⊥ = A⊥ ⅋ B⊥ (A & B)⊥ = A⊥ ⊕ B⊥ (A ⊕ B)⊥ = A⊥ & B⊥ (A ⅋ B)⊥ = A⊥ ⊗ B⊥ 論理単位元も同様の双対を持つ。例えば、⊤⊥ = 0 であり、! と ? は双対である。双対の規則とは、ある項を一方の辺からもう一方に移す場合、その双対に変換される、というものである。 直観線形論理 (ILL) は、1つの帰結しか許容しない。CLL とは異なり、ILL の結合子には完全な双対性はない。実際、par (⅋) と why not (?) と命題定数「ボトム (⊥)」は、導入規則の帰結が複数必要となるため、ILL には存在しない。結果として、ILL では線形含意が基本的結合子となっている。 線形論理の他の変種には、特定の結合子を持つものと持たないものなどがあり、扱う論理の複雑さも様々である。以下は、最も一般的な変種である。 乗法的線形論理 (MLL) - 乗法的結合子（tensor と par）およびそれらの単位元のみが許容される。決定可能だが、決定問題はNP完全である。 乗法的加法的線形論理 (MALL) - MLL に加法的結合子を追加したもの。決定問題はPSPACE完全である。 乗法的指数線形論理 (MELL) - 指数的結合子を MLL に追加したもの。MELLの決定問題は未解決である。 乗法的加法的指数線形論理 (MAELL) - 全ての結合子を持っている。決定不能である。 完全直観線形論理 (FILL) - 乗法的結合子 tensor、par と線形含意を許容する。（論理積、論理和、含意がある）直観論理に近い。 線形論理には一階のものと高階の拡張があるが、その考え方は標準的である（一階述語論理と高階述語論理を参照）。 線形論理に近い部分構造論理として、以下のものがある。 アフィン論理 - 弱化の構造規則を持つ線形論理の拡張。1 と ⊤ はアフィン論理では区別されない。 適切さの論理 - 縮約の構造規則を持つ線形論理の拡張。 非可換論理 - 線形論理から転置の構造規則を除いたもの。乗法的論理積がさらに2つに分割される（left fuse と right fuse）。