日記 (2018 年 2 月 14 日)
線型論理とは、 Girard†2 によって提唱された論理体系で、 弱化規則や縮約規則の使用が制限されているのが特徴である。
これによって、 連言は × と ⊗ に分かれ、 選言は + と ⊕ に分かれている。
また、 指数的結合子と呼ばれる 2 種類の結合子 !,? によって、 弱化規則や縮約規則の使用を制御する。
完全な線型論理の体系は以下のように定義される。
定義には様々なバリエーションがあるが、 ここでは Girard の原論文に従って、 シークエント計算の形で定義する。
記号は少し変えてある。
定義 1.1.
論理言語を以下によって定義する。
原子論理式は a で表すとし、 論理式 A を、
A::=1∣0∣⊤∣⊥∣a∣a∗∣A×A∣A+A∣A⊗A∣A⊕A∣!A∣?A
によって定める。
また、 各論理式 A に対して、 別の論理式 A∗ を、
1∗ ≡ 0 0∗ ≡ 1 ⊤∗ ≡ ⊥ ⊥∗ ≡ ⊤ a∗ ≡ a∗ (a∗)∗ ≡ a (A×B)∗ ≡ A∗+B∗ (A+B)∗ ≡ A∗×B∗ (A⊗B)∗ ≡ A∗⊕B∗ (A⊕B)∗ ≡ A∗⊗B∗ (!A)∗ ≡ ?A∗ (?A)∗ ≡ !A∗
によって再帰的に定める。
さらに、 省略記法として、
A⊸B ≡ A∗⊕B A⧟B ≡ (A⊸B)×(B⊸A)
を用いる。
シークエントの導出規則は以下によって定める。
Γ,Δ は任意個の論理式の列を表す。
⊢A,A∗Axiom ⊢A,Γ ⊢A∗,Δ ⊢Γ,ΔCut ⊢Γ,A,B,Δ ⊢Γ,B,A,ΔExchange ⊢1,Γ1 ⊢⊤⊤ ⊢Γ ⊢⊥,Γ⊥ ⊢A,Γ ⊢B,Γ ⊢A×B,Γ× ⊢A,Γ ⊢A+B,Γ+L ⊢B,Γ ⊢A+B,Γ+R ⊢A,Γ ⊢B,Δ ⊢A⊗B,Γ,Δ⊗ ⊢A,B,Γ ⊢A⊕B,Γ⊕ ⊢A,?Γ ⊢!A,?Γ! ⊢A,Γ ⊢?A,Γ?D ⊢Γ ⊢?A,Γ?W ⊢?A,?A,Γ ⊢?A,Γ?C
以上によって定義される論理を 「線型論理 (linear logic)」 という。
それぞれの結合子がどのような意味合いをもつのかについては様々な解釈がある。
これについては、 私自身もまだイメージが掴めておらず何も書けないので、 Girard†3 などを参照してほしい。
見て分かる通り、 ここで定義した線型論理のシークエントには前件が存在しない。
ただし、 Γ⊢Δ を ⊢Γ∗,Δ の意味だとすることで、 A∗ という形を使わずに、 前件をもつシークエントの導出規則で上と等価なものを作ることもできる。
このバージョンの導出規則は、 Bierman†1 や Troelstra†4 などに記載がある。
さて、 線型論理のシークエント計算による定式化は上の通りできたが、 導入則と除去則から成る自然演繹としての定式化できるかも気になるところである。
しかし、 自然演繹は結論としてちょうど 1 つの論理式しか許さないので、 後件に少なくとも 2 つの論理式を要求する ⊕ や ? の導出規則を自然演繹の形で扱うことは難しい。
そこで、 ×,+,⊗,! の 4 つに結合子を制限し、 ⊸ をプリミティブな結合子として追加したものが考えられている。
これも定義に様々なバリエーションがあるが、 ここでは Bierman†1 によるものを記載する。
定義 1.2.
論理言語を以下によって定義する。
原子論理式は a で表すとし、 論理式 A を、
A::=1∣0∣⊤∣a∣A×A∣A+A∣A⊗A∣A⊸A∣!A
によって定める。
推論規則は以下によって定める。
Γ,Δ およびこれに添字が付いたものは任意個の論理式の多重集合を表す。
A⊢AAxiom Γ1⊢A1 ⋯ Γk⊢Ak Γ1,⋯,Γk⊢11I Γ1⊢A1 ⋯ Γk⊢Ak Δ⊢0 Γ1,⋯,Γk,Δ⊢B0E ⊢⊤⊤I Γ⊢⊤ Δ⊢A Γ,Δ⊢A⊤E Γ⊢A Γ⊢B Γ⊢A×B×I Γ⊢A×B Γ⊢A×EL Γ⊢A×B Γ⊢B×ER Γ⊢A Γ⊢A+B+IL Γ⊢B Γ⊢A+B+IR Γ⊢A+B Δ,A⊢C Δ,B⊢C Γ,Δ⊢C+E Γ⊢A Δ⊢B Γ,Δ⊢A⊗B⊗I Γ⊢A⊗B Δ,A,B⊢C Γ,Δ⊢C⊗E Γ,A⊢B Γ⊢A⊸B⊸I Γ⊢A⊸B Δ⊢A Γ,Δ⊢B⊸E Γ1⊢!A1 ⋯ Γk⊢!Ak !A1,⋯,!Ak⊢B Γ1,⋯,Γk⊢!B!P Γ⊢!A Δ⊢B Γ,Δ⊢B!W Γ⊢!A Δ,!A,!A⊢B Γ,Δ⊢B!C Γ⊢!A Γ⊢A!D
以上によって定義される論理を 「直観主義線型論理 (intuitionistic linear logic)」 という。
注意すべき点は、 上の定義中の Γ や Δ が多重集合だという点である。
すなわち、 要素の順番は区別しないが、 要素の個数の違いは区別する。
通常の直観主義論理には弱化規則と縮約規則があるので、 要素の個数が問題となることはなく、 Γ などはただの集合として良い。
しかし、 線型論理はこの 2 つの規則の使用を制限することで生まれたものなので、 前件の個数の違いに敏感になる必要がある。
今後のしばらくの目標は、 上で定義した線型論理の圏論的モデルを構成することである。
参考文献
- G. M. Bierman (1993) 「On intuitionistic linear logic」 Ph. D. thesis, The University of Cambridge
- J. Y. Girard (1987) 「Linear logic」 『Theoretical Computer Science』 50:1–101
- J. Y. Girard (1995) 「Linear logic: Its syntax and semantics」 『In Advances in Linear Logic』 1–42
- A. S. Troelstra (1992) 『Lectures on Linear Logic』 Center for the Study of Language and Information