線形論理って何?

線形論理は、みなさんに馴染みの深い(?)直観主義論理や古典論理と並ぶ論理体系の 一種で、ちょっと変わった「含意(ならば)」や「連言(かつ)」が登場します。 なぜそんなものがいるのかを理解するために次の命題を考えましょう。

命題A:「私は110円持っている」

命題B:「私はコーラを買える」

命題C:「私はチョコレートを買える」

今、コーラもチョコレートも110円だとしましょう。すると、 110円持ってればコーラもチョコレートも買えますから 「AならばB」かつ「AならばC」であると言えます。 ということは、普通の論理だと、「Aならば”BかつC”」がいえますから、 「110円持っていれば、コーラも買え、かつ、チョコレートも買える」ということになります。 これは正しいでしょうか?X君とY君は次のように言い争いになりました。

X:「110円持ってれば、コーラもチョコレートもどちらでも好きな方を買える。だから どっちも買えるというのは正しい。」

Y:「110円持ってても、コーラを買えばお金はなくなっちゃくからチョコレートは買えなくなる。だからどっちも買えるというのは間違いだ。」

この言い争いの原因は何でしょうか? それはX君とY君は「かつ」を別の意味で解釈しているからです。 つまり、「AかつB」を、X君は「AもBも(同時になりたつとはかぎらないけど) どちらも好きな方を成立させることができる」と解釈し、Y君は「AもBも同時に成り立つ」 と解釈しているわけです。ところが通常の論理では「かつ」に相当する論理記号は 一つだけですから、上のような混乱が生じたわけです。 そこで、線形論理では、X君にような解釈とY君のような解釈を別々の連言で表します (ここでは前者を&で表し、後者をΛで表すことにします)。 さらに、「110円持っていれば○○が買える」では、○○を買ってしまったら 「110円持っている」という事実はなくなってしまうわけですから、 「ならば」の意味も通常の論理の含意とは異なることがわかります。そこで、含意についても 違う記号を用意して、-o で表すことにします。

さて、以上のように新しい論理記号を用いると、何が成立するかを次のように 正確に表現できます。

A-o B:「110円持ってれば、コーラを買える。ただしコーラを買ってしまったら 110円はもうなくなってしまう。」

A-o C:「110円持ってれば、チョコレートを買える。ただしチョコレートを買ってしまったら110円はもうなくなってしまう。」

ではもう一度、X君とY君の主張を確認してみましょう。X君は、 「Aならば"BかつC"」を「A-o(B&C)」のことだと解釈していたわけです。 だからその意味では、X君の主張は正しかったわけです。 一方、Y君は、「Aならば"BかつC"」を「A-o(BΛC)」、すなわち 「Aが成り立っていればBもCも同時に成立する」と解釈していたわけです。 だからそれが誤りだというY君の主張も正しかったわけです。

以上が線形論理の簡単な動機づけです。線形論理には上で導入した以外にも いろいろな論理記号が登場します。勘のいい人にはすでに察子がついたと 思いますが、「選言(または)」も2つの論理記号にわかれます。 また、通常は、A-oBとAからBを導くと、Aは成立しなくなってしまいますから、 「いつでも成立する」命題を表現するために、「!A」というような論理式も導入します (!がついていれば、何回でも使えるわけです)。

この十年、上のような線形論理のコンピュータサイエンスへの応用が注目を集め、 さまざまな角度から研究がされてきました。我々の研究室でも、その一つとして、 並行・分散プログラミング言語と線形論理との関係について研究をすすめてきました。 いったいどんな関係があるんだ?と興味のある人は課題7 を選んでみましょう。


課題7のページに戻る

課題のホームページ

koba@is.s.u-tokyo.ac.jp