懐中電灯とは何かを述語論理で
懐中電灯とはなにか?!
懐中電灯を通して、仕様と故障箇所検出について考えてみる。
1. 懐中電灯の目的
懐中電灯の目的は何か?
漠然と言えばそれは「闇を照らす」ことだと思う。
なにか ⇒ 闇を照らす … (1)
の「なにか」にあたるもののひとつが懐中電灯と言えるだろう。
(1)には室内灯や街灯や車のライトなども含まれるから、「懐中電灯」と減退したい場合には「持ち歩きができる」という条件をつけるべきだ。
なにか ⇒ 闇を照らす ∧ 持ち運びができる … (2)
考え出すと他にも条件がつくし、そもそも「闇を照らす」ことだけが目的ではないかもしれない。
「相手の目をくらます」とか、もっと具体的に「机の下に落とした鍵を探す」ことが目的ということもありうる。
「懐中電灯」の目的とは何なのだろうか?
2. 懐中電灯の機能と構造
目的がよくわからないままだが、懐中電灯の機能や構造についてすこし考えてみる。
最初に懐中電灯を考えた人は、懐中電灯が存在していないので、その機能も構造も知らない。だから、目的から機能や構造を発明したわけなので、発明について考えるにはここで考えようとしていることはちょっとチートになってしまうが、その仕組みを考えることは、懐中電灯を理解したり表現したりするのに役立つとおもう。
まず、機能としてはこうなるだろう。
懐中電灯は「スイッチ」を入れると「ランプ」が灯る。 … (3)
懐中電灯は「スイッチ」を切ると「ランプ」も灯らない。 … (4)
(4)がないと、スイッチを切っても「ランプ」が灯っぱなしになるので、必要だ。
これだけだと、室内灯や車のライトも合致してしまう。そこで「持ち運びができる」というのは、物理的な構造に関係すると思うから、これも書いておくべきだろう。
懐中電灯は、「スイッチ」と「電池」と「ランプ」があり、それらは「電気的に繋がっている」 … (5)
懐中電灯の重さは、300gを超えない。 … (6)
ここでは(6)は前提として成り立っているとし、無視する。機能と実体の二面について同時に考えるのはむずかしいので、棚上げにするという気持ちである。ということは、「懐中電灯」と言いながら「電池」であかりのつく製品について考えているということになるだろう。これでも「車のライト」は除外できていない気がするが、話を続ける。
(3)と(4)に加えて、(5)を加味して懐中電灯の機能を詳細化していく。詳細化というか、(3)や(4)で無視していた要素を追加していくということになる。「懐中電灯は」の部分は以下省略する。
「スイッチ」を入れても「電池」が空だと「ランプ」は灯らない。 … (7)
これは懐中電灯の機能ではないかもしれない。制約条件のようにも思う。
電池を考慮して(3)(4)を書き直す。
「スイッチ」を入れて「電池」が空でなければ「ランプ」が灯る。 … (3')
「スイッチ」を切ると「電池」にかかわらず「ランプ」は灯らない。 … (4')
「電気的につながっている」を考慮すると、こう書けるだろう。
「結線」が正しければ「スイッチ」を入れて「電池」が空でなければ「ランプ」が灯る。 … (8)
(8)は(3')に置き換わるものなので(3'')と書いても良いが、ここでは(8)とする。
「電気的につながっている」は文字数が多いので「結線が正しい」に言い換えた。
(4')でも同様に、次のようなことも言える。
「結線」が切れていれば、「スイッチ」や「電池」にかかわらず「ランプは灯らない。 … (9)
(9)は(4')を置き換えるものなので(4'')かもしれないが、ここでは(9)とする。
あと(7)はこのようになる。
「結線」が正しければ「スイッチ」を入れても「電池」が空だと「ランプ」は灯らない。 … (10)
これで必要な情報は全部書き出したと思う。
述語論理で書いてみる。
3. 述語論理で懐中電灯
[前提]
まず、私の視野には懐中時計が複数存在するとする。それらには名前(a,b,c…)を書いたシールが貼ってあるものとする。(名付けるということはシールを貼るということなのか?)
[述語]
懐中時計の名前を引数とする述語として次のものを使う。
スイッチON(x) : xのスイッチが入っているとき真
ランプ光る(x) : xのランプが光っているとき真
電池有(x) : xの電池が空でないとき真
結線(x) : xの部品の結線が繋がっているとき真
[書き方]
(8)(9)(10)を述語を使って書き直す。
「結線」が正しければ「スイッチ」を入れて「電池」が空でなければ「ランプ」が灯る。 … (8)
C2 ∀x +結線(x) ∧ +スイッチ(x) ∧ +電池有(x) ⇒ +ランプ光る(x)
「結線」が切れていれば、「スイッチ」や「電池」にかかわらず「ランプは灯らない。 … (9)
C3 ∀x -結線(x) ⇒ -ランプ光る(x)
「結線」が正しければ「スイッチ」を入れても「電池」が空だと「ランプ」は灯らない。 … (10)
C4 ∀x +結線(x) ∧ +スイッチON(x) ∧ -電池有(x) ⇒ -ランプ光る(x)
これらの条件ではxに何も代入されないので、実質命題論理だが、xにはaとかbとかを代入しても成り立つと考えたいのだろう。つまり懐中電灯の性質をこれらは述べている。
Σf = {C2, C3, C4}
とする
[故障]
Σfを前提とする。
clauseで書くとこうである。
C2 ∀x -結線(x) ∨ -スイッチ(x) ∨ -電池有(x) ∨ +ランプ光る(x)
C3 ∀x +結線(x) ∨ -ランプ光る(x)
C4 ∀x -結線(x) ∨ -スイッチON(x) ∨ +電池有(x) ∨ -ランプ光る(x)
さて、ある日、懐中電灯aのスイッチを入れたが灯らなかったとする。
これを次のように書く。
(Con1) -スイッチON(a) ∨ -ランプ光る(a)
Con1では「スイッチを押した結果としてランプが灯らない」という関係を示している。
これから¬Con1を作るとこうなる。
C1.1 +スイッチON(a)
C1.2 +ランプ光る(a)
¬Con1 = {C1.1, C1.2}
これからΣfとのresolventの集合はこうなる。
{-結線(a)∨-電池有(a)∨+ランプ光る(a), +ランプ光る(a)} … (13) from C2, C1.1
{+結線(a) } … (14) from C3, C1.2
{-結線(a)∨ +電池有(a)} … (15) from C4, C1.1, C1.2
まず、(13)は、C1.2からランプが光っているのがFactなので、左側のclauseは真となり、矛盾は生まれない。
次に、(14)からはaの結線が正しくなければならないと言われている。
最後に、(15)では、結線が正しいならば、電池が残っていてはならないと言われている。
つまり、
故障所の特定手順
1) 結線を調べる。
2) 結線に問題がなければ、電池を調べる。
となる。
人間は、先に電池を調べると思うが、何か書き方によるのかもしれない。
[C3の詳細化]
C3 ∀x +結線(x) ∨ -ランプ光る(x)
は次の4つを1つにまとめたものになっている。
C3.1 ∀x +結線(x) ∨ +スイッチON(x) ∨ +電池有(x) ∨ -ランプ光る(x)
C3.2 ∀x +結線(x) ∨ +スイッチON(x) ∨ -電池有(x) ∨ -ランプ光る(x)
C3.3 ∀x +結線(x) ∨ -スイッチON(x) ∨ +電池有(x) ∨ -ランプ光る(x)
C3.4 ∀x +結線(x) ∨ -スイッチON(x) ∨ -電池有(x) ∨ -ランプ光る(x)
ここからC1.1の+スイッチON(x)を含むものを除くとC3.3とC3.4になり、(14)の代わりに
{
C3.3' +結線(a) ∨ +電池有(a)} … (14.1}
C3.4' +結線(a) ∨ -電池有(a)} … (14.2)
}
とすると、(14.1)と(14.2)をresolveして+結線(a)がでてくるので、先の書き方と同じになる。
[Con1の変形]
Con1はこう書いてははだめなのだろうか。
つまり、スイッチを押して、ランプがつかない時点での状態は、こう書けるはずだ。
(Con1') +スイッチON(a) ∧ -ランプ光る(a)
である。これをconjectureとすると、¬conjは次のclausesになる。
C1.1' -スイッチON(a)
C1.2' +ランプ光る(a)
¬Con1' = {C1.1, C1.2}
とする。
¬Con1'を¬conjとしてΣfで反証してみるとC3とC4から次のresolventが生成される。
{ -結線(a)} … (a') from ¬Con1', C3
{ -結線(a)∨-スイッチON(a)∨+電池有(a), -スイッチON(a) } … (b) ¬Con1' & C4
(b)の場合、-スイッチON(a)がFactなので、左側のclauseも真になり、矛盾は生まれない。
(b)に-スイッチON(a)が残っていなければ、(b)は
{-結線(a) ∨ +電池有(a)} .. (c)
になり、故障箇所の手がかりが得られるのだが・・・
∧でつなぐのがだめな理由ははっきりとわからない。何らかの因果関係みたいなことを書く必要があるということなのか?
あるいは¬Con1'は、∧の否定なので、
¬Con1''={-スイッチON(a)∨+ランプ光る(a)}
なのだろうか。
これだとclauseのリテラルが減らないので、矛盾に至らないからだめだ。
今回も迷いながら終わる。