線形論理超入門！！ - 曇りなき眼で見定めブログ

　デカく構えたタイトル！！

　後期に専門が違う人向けに研究の説明をする演習があるようなので、ロジックが専門でない人向けの線形論理の解説を考えたい。

自然演繹からシーケント計算へ

　論理学の入門講義をとったことがある人は多そうなので、自然演繹から入ってみる。自然演繹は論理結合子（「かつ∧」とか「ならば→」とか）の導入則と除去則で成り立っている。例えば∧の規則はこんな感じ。

A B　　　　  A∧B
---(∧導入)  ---(∧除去)
A∧B　　　　  A(またはB)

というのを知っていることを前提にしたいけれど知らない人もいるかもしれない。でもそれはまあそれとしてここでは前提知識とする。
　自然演繹は論理学の入門講義でよく扱われるが、もうちょっと証明を勉強するとシーケント計算というのが出てくる。これも論理結合子の規則を持っていて、

A⇒A (公理)

Γ⇒A  Γ⇒B　　　　  Γ,A⇒C　　　　　Γ,B⇒C
--------(∧右) 　--------(∧左) -------(∧左)
  Γ⇒A∧B　 　　　 Γ,A∧B⇒C　　　　Γ,A∧B⇒C

となる（これは直観主義論理の例）。ここで、 $\Gamma$ というのは論理式の集まりと思ってよい。ただし集合ではない。同じ論理式が1個か複数かで違うからである（要素の数もカウントする集合は多重集合という。なのでこれらは論理式の多重集合である）。自然演繹では全体でやっていた「前提から帰結を出す」(推論)ということを、シーケント計算では一段ごとにやっているというイメージである。例えば $\land$ 左規則のひとつめは「 $\Gamma$ と $A$ という前提から $C$ が出せたならば、 $\Gamma$ と $A \land B$ という前提から $C$ を出してもよい」と読める。
　こういう解釈ができるのもシーケント計算のメリットだが、メリットはそれだけではない。自然演繹では暗黙のうちに仮定されていた構造規則というのを、シーケント計算では暗黙にでなく明示的に扱える。構造規則というのは以下のような規則である。

Γ,A,A⇒C　　 　　 Γ⇒C
-------(縮約) 　-----(弱化)
 Γ,A⇒C　　　　　 Γ,A⇒C

　縮約というのは、「 $\Gamma, A, A$ という前提から $C$ が出たならば、前提の $A$ をひとつ減らしてもよい」と読める。これは自然演繹でひとつの仮定を何度使ってもよいことと対応している。この性質を使うことで自然演繹では $((A \to A) \to B) \to (A \to B)$ のような定理が証明できる。この式と縮約規則はよく見ると似ている。弱化は前提をどのように増やしてもよいという規則である。自然演繹では使わない仮定が増えたところで困ることはない。
　シーケント計算を使った証明の例をひとつ。

 A⇒A　　      B⇒B
-----(弱化)  -----(弱化)
A,B⇒A　　    A,B⇒B
-----------------(∧右)
　　  A,B⇒A∧B

二つしか規則を使っていないけど構造規則と $\land$ 規則を使えてるからまあよしとしましょう（ここに $\land$ 左規則を二回と縮約を適用すると $A \land B \Rightarrow A \land B$ というただの公理になってしまう）。

もうひとつの連言

　ここで重要なのが、 $\land$ 規則は次のようにしてもよいということである。

Γ⇒A  Γ'⇒B　　　　 Γ,A,B⇒C
---------(∧右') --------(∧左')
 Γ,Γ'⇒A∧B　 　　　Γ,A∧B⇒C

これらの「'」を付けた規則は最初の規則と同じだということが示せる。同じということはどういうことかというと、まず $\land$ 右規則の上段から $\land$ 右'規則（と構造規則）を使って $\land$ 右規則の下段を出すことができる。

Γ⇒A  Γ⇒B
--------(∧右')
 Γ,Γ⇒A∧B
 -------(縮約*)
  Γ⇒A∧B

ただし(縮約*)では $\Gamma$ の式すべてに縮約を適用しているのを省略して一段で書いている。逆に $\land$ 右規則（と構造規則）を使って $\land$ 右'規則を出すこともできる。

  Γ⇒A　　      Γ'⇒B
------(弱化*) ------(弱化*)
Γ,Γ'⇒A　　    Γ,Γ'⇒B
-------------------(∧右)
 　　 Γ,Γ'⇒A∧B

ただし(弱化*)では $\Gamma$ あるいは $\Gamma '$ ができるまで弱化を何度も使っているのを一段に省略して書いている。実は左規則についても同様にして同じことが示せるのだが、ここでは右規則のみに注目する。

資源消費と線形論理

　 $\land$ 右規則について考えてみる。これは「 $\Gamma$ という前提から $A$ が出て同じ $\Gamma$ という前提から $B$ が出るならば、 $\Gamma$ という前提から $A \land B$ を出してもよい」ということと読める。このような推論は自然演繹でもありえるが、その場合は仮定を二度使うこととなる。これが $\land$ 右'規則を使って $\land$ 右規則を出すときに縮約を使うことと対応している。逆に $\land$ 右規則を使って $\land$ 右'規則を出すときの弱化に対応するのは、仮定を増やすということである。 $\land$ 右規則では二つの上段式で同じ前提を持っていなければならないので、同じになるように仮定を増やす必要がある。さて、ここで注目していただきたいのが、図を見るとわかるとおり $\land$ 右規則と $\land$ 右'規則の行き来には構造規則を使うことが避けられないということである。仮定を何度も使ったり仮定を増やしたりということと対応する構造規則なるものをなしにしたらどうなるか。
　ここに「資源の消費」という考え方を導入したい。仮定は資源、 $\Rightarrow$ は資源を消費して何かを作ることと考える。こうすると構造規則の制限というアイデアを正当化できる。仮定は資源なので何度も使えないし勝手に増やしたりもできない。
　構造規則をなしにしたらどうなるかというと、もはや $\land$ 右規則と $\land$ 右’規則は同一視できなくなる（実は左規則についても）。なのでこれらを記号を分けて以下のように書く。

Γ⇒A  Γ⇒B　　　　  Γ,A⇒C　　　　　Γ,B⇒C
--------(&右) 　--------(&左) -------(&左)
  Γ⇒A&B　 　　　 Γ,A&B⇒C　　　　Γ,A&B⇒C

Γ⇒A  Γ'⇒B　　　　 Γ,A,B⇒C
---------(⊗右)  --------(⊗左)
 Γ,Γ'⇒A⊗B　 　　　Γ,A⊗B⇒C

&と $\otimes$ はそれぞれ加法的連言と乗法的連言という。これらが線形論理の論理結合子である（選言も同じように分裂する）。

まとめ

　まとめる。
　シーケント計算の $\land$ の右規則には二種類あり、それらは構造規則を前提とすれば同一視できる。しかし構造規則は資源消費という観点からは望ましくない規則ともいえる。構造規則をなしにすると二つの規則は同一視できなくなり、 $\land$ が二種類に分裂することとなる。これが線形論理の連言である。
　注意しなければならないのは、歴史的には線形論理は別の理由で導入され、資源消費と結び付けられたのはできたあとということである。しかし今では線形論理といったら資源という感じになっているし、創始者のジラール先生もそうなのでよしとする。
　参考にしたのはこの本（記法が違うが）。

Lectures on Linear Logic (Lecture Notes Book 29) (English Edition)

作者:Troelstra, A. S.
Center for the Study of Language and Inf

Amazon

　線形論理誕生の経緯は照井一成「線形論理の誕生」という論文に詳しい。この論文についてはそのうち書く。