線形論理
線形論理︵せんけいろんり、英: Linear logic︶は、﹁弱化(weakening)規則﹂と﹁縮約(contraction)規則﹂という構造規則を否定した部分構造論理の一種である。﹁資源としての仮説 (hypotheses as resources)﹂という解釈をする。すなわち、全ての仮説は証明において﹁一回だけ﹂消費される。古典論理や直観論理のような論理体系では、仮説︵前提︶は必要に応じて何度でも使える。例えば、A と A⇒ Bという命題から A∧ Bという結論を導出するのは、次のようになる。
(一)A と A⇒ Bを前提とするモーダスポネンス︵あるいは自然演繹でいう含意の除去︶により、B が得られる。
(二)前提 Aと (1) の論理積から A∧ Bが得られる。
これをシークエントで表すと、A, A⇒ B⊢ A∧ Bとなる。上記の証明ではどちらの行でも、A が真であるという事実を﹁消費﹂している。この真理の﹁気軽さ﹂は形式手法では一般に必須である。
しかし、日常的な世界に関する文に適用するには、真理は抽象的すぎ、扱いにくい。例えば、約1リットルのクリームから約450グラムのバターができるとする。クリームをバターを作るのに使うとすると、クリームとバターの両方を持っているという結論は得られない。ところが上の論法でいけば cream, cream ⇒ butter ⊢ cream ∧ butter となる︵ここで、cream は﹁私は1リットルのクリームを持っている﹂という命題を表し、butter は﹁私は450グラムのバターを持っている﹂という命題を表す︶。
このような活動を通常の論理でうまく表せないのは、クリームやバターなどの﹁資源﹂全般の性質によるものである。ある量の資源は、真理のように好きなように使ったり始末したりできず、全ての﹁状態変化﹂について注意深く見ていかなければならない。バター作りを正確に表すと、次のようになる。
1リットルのクリームがあり、1リットルのクリームを450グラムのバターに変換するプロセスを経ると、450グラムのバターが得られる。
線形論理ではこれを cream, cream ⊸ butter ⊩ butter と表記する。論理結合子︵⇒ の代わりに ⊸︶と論理内含︵⊢ の代わりに ⊩︶の記号が異なる点に注意されたい。
線形論理は1987年、フランスの論理学者ジャン＝イヴ・ジラールが提唱した。
証明は全てカット規則を使わない形に変換できる。
線形含意はこの表には出ていないが、線形否定と乗法的論理積を使えば、CLLでも A⊸ B≡ A⊥ ⅋ Bと定義できる。これは古典論理ではお馴染みの形である。例えば、普通の含意 ⇒ は、A ⇒ B≡ ?A⊥ ⅋ Bと定義できる。
このような定義はもちろん﹁線形否定﹂の記法を必要とするが、古典論理では双対を使うこともできる。A の双対は A⊥ と記述され、以下のように定義される。
線形結合記号[編集]
線形論理では、論理結合子が再検討される。各結合子は、乗法的 (multiplicative) なものと加法的 (additive) なものに分けられ、それぞれ同時 (simultaneous) 存在と択一 (alternative) 存在に対応する。結合子を解説するため、ここでは自動販売機を例として説明する。 乗法的論理積︵tensor、⊗︶ 資源の同時並行的出現を表し、消費されるときに使われる。例えば、ガムを1個とソフトドリンクを1瓶買う場合、gum ⊗ drink を要求する。どういう順番に並べるかは自由である。論理積が不可分であるとき、順序は無関係である。例えば (gum ⊗ drink) ⊗ candy としたとき、まずガムを選んで次にキャンディを選び、最後にドリンクを選ぶこともできる。実際、⊗ では結合法則と交換法則が成り立つので、先の式は gum ⊗ (candy ⊗ drink) と等価である。定数1は資源がないことを表し、単位元として機能する。すなわち、A ⊗ 1 ≡ 1 ⊗ A≡ Aである。 加法的論理積︵with、&︶ 資源の択一的出現を表し、人間側の選択を表す。自動販売機でポテトチップスとキャンディとソフトドリンクが同じ値段で売られているとき、その値段ぶんの金を持っていればどれか一つだけ購入できる。購入後は、candy & chips & drink ︵つまり、この論理積のどれか1つ︶を入手している。このような場合に ⊗ を使うことはできない。⊗ を使うと全部を購入したことになってしまう。この演算でも結合法則と交換法則が成り立つ。 加法的論理積の単位元は﹁トップ﹂である︵⊤ と表記し、A & ⊤ ≡ ⊤ & A≡ Aとなる︶。これは、選択肢がないこと、あるいは選択できないことを表す。資源の正確な列挙が難しいか不可能なときに使われることが多い。例えば、自動販売機で購入するものを気にしない場合や、何も購入しない可能性もある場合、購入した資源は ⊤ で表される。この単位元を ⊗ で使う場合、資源の最小合成を表す。例えば、少なくともキャンディを購入し、可能なら他にも何かを購入する場合、購入したものは candy ⊗ ⊤ で表される。 乗法的論理和︵par、⅋︶ 資源の同時平行的出現を表し、供給するときに使われる。1つのボタンを押すと、ガムとソフトドリンクを1つずつ同時に購入できるとすると、これを gum ⅋ drink と表すことができる。乗法的論理積 gum ⊗ drink との違いは、機械側で順序を制御する点である。ガムとドリンクではどういう順序でも構わないが、コーヒーの自販機ではコーヒーと紙コップが販売され、cup ⅋ coffee と cup ⊗ coffee では意味が大きく異なる。論理積のときと同様、結合法則と交換法則が成り立つ。その単位元は﹁ボトム﹂︵⊥︶であり、空のゴールを意味する。例えば、コインを投入せずに返却レバーを押すことを表す。 加法的論理和︵plus、⊕︶ 資源の択一的出現を表し、機械の制御する選択を表す。例えば、自販機が博打的な動作をする場合を考える︵すなわち、100円を投入すると、キャンディかソフトドリンクか有給休暇一日ぶんが得られるとする︶。この購入の結果は candy ⊕ drink ⊕ vacation で表される。どれか1つを購入できることは分かっているが、購入者が選択を制御することはできない。実際、自販機で有給休暇を購入できるわけがない。加法的論理積 candy & drink & vacation の場合、購入者が休暇を選択可能である。この演算でも結合法則と交換法則が成り立つ。単位元は 0 であり、出力が何もない場合、致命的問題の発生、機械がプログラムに従えない状況などを表す。 線形含意︵lolli、⊸︶ 上掲の論理積と論理和は世界の状態を定義するが、その記述は静的である。状態変化については、線形論理では線形含意の結合子︵⊸︶を定義している。資源的観点では、A ⊸ Bは、資源 Aを消費して資源 Bを生成することを意味する。硬貨粉砕機があるとき、その作用は penny ⊸ smashed penny と表される。なお、含意自身も単一消費の原則に従わなければならない資源であることに注意されたい。 指数的結合子︵!、?︶ ここまで解説した結合子は状態やその遷移を表すことができるが、真理値を記述するには弱すぎる。実世界に関する議論が標準の数学的推論を妨げるべきではないので、これは明らかに好ましい。線形論理は、様相論理の考え方を導入し、通常の論理を対をなす指数的結合子を使って埋め込む。 ●命題の再利用やコピーは、"of course" 結合子︵!︶を使ってなされる。論理的に、!A が仮説として2カ所に出現するとき、それらは1つの出現に縮約される。消費者またはユーザーが Aの出現回数を決定することができるという意味で、これは論理積と関連している。 ●帰結の集まりは、"why not" 結合子︵?︶を使った命題で拡張することができる。論理的には、任意の事実に ?A という追加の帰結を含めることで弱めることができる。供給者または機械が Aの出現回数を決定することができるという意味で、これは論理和と関連している。 資源的解釈において、!は﹁任意生産 (arbitrary production)﹂を表し、?は﹁任意消費 (arbitrary consumption)﹂を表す。 実際の自動販売機は、これらの結合子の複雑な組み合わせで表され、それによって機械の全ての振る舞いを記述できる。線形論理の変種[編集]
線形論理には、様々な限定バージョンや変種が存在する。その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）。
関連項目[編集]
参考文献[編集]
- Girard, Jean-Yves. Linear logic, Theoretical Computer Science, London Mathematical 50:1, pp. 1-102, 1987.
- Girard, Jean-Yves, Lafont, Yves, and Taylor, Paul. Proofs and Types. Cambridge Press, 1989. (An electronic version is online at [1].)
- Troelstra, A.S. Lectures on Linear Logic. CSLI (Center for the Study of Language and Information) Lecture Notes No. 29. Stanford, 1992.
外部リンク[編集]
- Patrick Lincoln's excellent Introduction to Linear Logic (Postscript)
- Introduction to Linear Logic by Torben Brauner
- A taste of linear logic by Philip Wadler
- Linear Logic by Roberto Di Cosmo and Dale Miller. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).
- Overview of linear logic programming by Dale Miller. In Linear Logic in Computer Science, edited by Ehrhard, Girard, Ruet, and Scott. Cambridge University Press. London Mathematical Society Lecture Note, Volume 316, 2004.