|
(n) linear logic =========================== ・ 線形 ： [せんけい] 【名詞】 1. (1) line 2. straight alignment 3. (2) (gen) (math) linear ・ 線形論理 ： [せんけいろんり] (n) linear logic ・ 形 ： [けい, かたち, ぎょう] 1. (suf) shape 2. form 3. type ・ 論 ： [ろん] 【名詞】 1. (1) argument 2. discussion 3. dispute 4. controversy 5. discourse 6. debate 7. (2) theory 8. doctrine 9. (3) essay 10. treatise 1 1. comment ・ 論理 ： [ろんり] 【名詞】 1. logic ・ 理 ： [り] 【名詞】 1. reason
線形論理（せんけいろんり、）は、「弱化(weakning)規則」と「縮約(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年、フランスの論理学者ジャン＝イヴ・ジラールが提唱した。 == 線形結合記号 == 線形論理では、論理結合子が再検討される。各結合子は、乗法的 (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)」を表す。 実際の自動販売機は、これらの結合子の複雑な組み合わせで表され、それによって機械の全ての振る舞いを記述できる。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「線形論理」の詳細全文を読む スポンサード リンク
|