論理に出てくる述語(predicate)をコンピュータの文脈で考えると、適当なデータ領域Dの上で定義され、真偽値(trueまたはfalse)を戻り値とする関数になります。述語を数学的な関数と捉えるなら、その論理計算は古典論理と同じようにできます。しかし、コンピュータによる計算だと、なかなか古典論理と同じにはいきません。
部分的にしか定義されない述語の計算
コンピュータのなかの関数はプログラムにより定義されます。プログラムにより定義された関数の宿命として、無限走行したり例外が発生したりで結果が得られないことがあります。つまり、述語の関数 D→{true, false} は部分関数となります。
部分(かもしれない)関数 f:D→{true, false} があるとき、未定義な部分では f(x) = ⊥ と考えます。⊥ は架空の値でボトムと呼ばれます。「f(x) = ⊥」という言明は、xのところで関数fが未定義だということに他なりません。この細工をすると、部分関数fを f:D→{true, false, ⊥} の全域関数だと考えることができます。
{true, false, ⊥} に値をとる関数は3値の述語だと言ってもいいでしょう。論理演算である∧(AND)や∨(OR)はどうなるでしょうか。⊥を加えた3値の真偽表を書いてみます。横軸が f(x) の値で、縦軸が g(x) の値として、欄に f(x)∧g(x) の値が書き込んであります。
∧ | true | false | ⊥ |
---|---|---|---|
true | true | false | ⊥ |
false | false | false | ⊥ |
⊥ | ⊥ | ⊥ | ⊥ |
f(x)∧g(x) を計算するときに、f(x) と g(x) の両方の値を使うのではなくて、片方の値が得られたら結果を出してしまうことがあります。短絡(ショートカット)計算です。直列(逐次、順次)処理と並列処理で結果が変わりますが、f(x)∧g(x) を「fの計算が終わった後でgの計算をする」と解釈する場合(つまり直列処理)の短絡的真偽表は次のようになります。
∧ | true | false | ⊥ |
---|---|---|---|
true | true | false | ⊥ |
false | false | false | ⊥ |
⊥ | ⊥ | false | ⊥ |
並列処理では、短絡というよりは、「f(x)とg(x)を計算する2つの計算プロセスのどちらか一方がfalseで終わったら結果をfalseにする」というルールで計算することになるでしょう。そのときの真偽表は次のようです。
∧ | true | false | ⊥ |
---|---|---|---|
true | true | false | ⊥ |
false | false | false | false |
⊥ | ⊥ | false | ⊥ |
真偽の判断が難しくて出来ないとき
述語fに対してf(x)を求めることは、x∈D に関するある性質が成り立つかどうかを判断することです。神様なら確実に真偽を決定できるでしょうが、現実には真偽の決定が難しいことがあります。⊥の場合とは異なり、プログラムが無限走行したり例外を起こすわけではなくて、プログラムの判断能力が乏しいので結果が出ない状況ですね。
この状況を表現するために「わかりません」を表すindef(indefinite)を真偽値に加えます。すると真偽値の集合は {true, false, indef, ⊥} となります。indefが返るときは、プログラムはきちんと正常終了しています。その結果(プログラムによる判断の報告)が「わかりません」なのです。indefを考慮した直列短絡計算の真偽表が次。
∧ | true | false | indef | ⊥ |
---|---|---|---|---|
true | true | false | indef | ⊥ |
false | false | false | false | ⊥ |
indef | indef | false | indef | ⊥ |
⊥ | ⊥ | false | ⊥ | ⊥ |
indef∧⊥ が⊥になってしまうのは、できるだけ確実な結果を得るため(falseと断定できることがあるので)次の結果を待つせいです。
⊥やindefが役に立つとき
プログラムの無限走行や例外は避けがたいことがあるので、値に⊥を入れて考えたほうがいいときは多いでしょう。人間は、そして人間が作るプログラムは全能ではないので、答を出せないこともあります。自覚的にギブアップするときはindefのような値を導入する必要があります。
実行時にはちゃんと計算ができてても、実行前に計算結果をある程度は予測(静的解析)しようとすると、「わかりません」という答になることはままあります。
不確定さや曖昧さを無視するのではなくて、不確定さ/曖昧さの影響や法則性を明確にしたいときに⊥やindefは役に立ちます。