乗法的「または」について

線型論理のおはなし。線型論理は少しかじった程度でまったく詳しいわけじゃないのでこれから書く内容が的外れである可能性もあると思いますが,以前からなんとなく思っていることを書いてみます。

線型論理には「かつ」と「または」がそれぞれ二種類あり,加法的・乗法的という接頭辞つきで呼び分けられます。よく引き合いに出されると思われる「コーヒーまたは紅茶」を例にとって違いを見てみましょう。

加法的「かつ」は,「どちらか好きな方を選ぶことができるが,両方とも選ぶことはできない」です。「コーヒーまたは紅茶がつきます」と言われたらこの意味ですね。どちらを選ぶこともできますが,両方くれと言うことはできません。日常の言葉では「または」と言いますが,線型論理の演算子としては「かつ」に相当するものなのです。

乗法的「かつ」は,「両方とも与えられる」です。もし「コーヒーと紅茶がつきます」と言われて「と」が乗法的なら,コーヒーと紅茶が両方とも出てくるということです。でも普通のお店ではあんまりそういうことはなさそうですね。

加法的「または」は,「どちらか一方が与えられ,どちらであるかはわからない」です。コーヒーか紅茶が出てきますが,どちらが出てくるかは店の都合によって決まるので出てくるまでわからないのです。

普通の飲食店でこういうことはあんまりないと思いますが,ここは視点を変えるともっとうまく解釈できます。これまでは客の視点で考えていましたが,そうではなく店の視点で考えてみましょう。そうすると「コーヒーまたは紅茶がつきます」は「コーヒーまたは紅茶を出さなければならない」となりますが,どちらであるかは注文を受けるまでわからないので,加法的「または」の解釈とうまく一致します。「コーヒーまたは紅茶」の「または」は,客にとっては加法的「かつ」ですが,店にとっては加法的「または」だったのです。

最後に乗法的「または」ですが,これについては非常に説明が難しいようで,定説を知りません。ここでは無理矢理解釈を試みるために,ド・モルガンの法則を使ってみます。「コーヒーまたは紅茶」は「コーヒーではないし紅茶でもない,のではない」なので,否定されているところを継続の型と思うと,「コーヒーを受け取る継続と紅茶を受け取る継続を受け取る継続」が「コーヒー乗法的または紅茶」であるということになります。

これだけだとよくわからないのでもうちょっとかみくだこうとしてみましょう。継続というのはそれを消費する人(あるいは双対的に,それに消費されるもの)のことですから,「コーヒー乗法的または紅茶」とは,コーヒー(だけ)を飲む人と紅茶(だけ)を飲む人の二人がいるとうまく消費できる何か,というところでしょうか。それって何なの,というと,なんなんでしょう。コーヒーと紅茶両方なんだけど量は通常のコーヒーの半分と通常の紅茶の半分とか……というイメージをたいした根拠もなく持っていたんですが,今の説明だけ見るとコーヒーと紅茶が一杯ずつ出てきてもいいような気がします。でもそれだと「または」ではなく「かつ」なのでおかしい気がします。なぜなんでしょう。

よく考えてみると,コーヒーを飲む人と紅茶を飲む人とコーヒーと紅茶があると,コーヒーと紅茶それぞれについてそれを消費するという行為が発生し,飲んだ後にはカップが二つ残ります。つまり継続を使った結果が二つ出てきてしまいそうです。二つあるとそれは単一の継続の呼び出し結果とは考えられないので,これでは整合性のある解釈とはいえません。求められているのは,コーヒーを飲む人と紅茶を飲む人の二人がいるときに,その二人が消費した結果カップが一つだけ残るようなもの,なのです。それって何なんでしょうか。

よくわからなくなってきましたね。やっぱり乗法的な「または」は難しい。

もしかしたら,加法的なときと同様に客と店の双対性を使って解釈したほうがよかったのかもしれません。何か思いついたらまた書きます。