Exercises on Scheme (4)

命題論理の論理式の標準形

2値命題論理の論理式には，標準形がある．ここでは，そのうちのひとつ，論理和標準形を求めるプログラムを書いてみることにする． (上のリンク先はWikipediaです)．

論理和標準形を求める過程は，通常次のような手順を経る．ただし，∧と∨が本来は引数2つのオペレータであるのを，結合法則と交換法則が成り立つため，n-aryのオペレータとして扱う．この場合，引数0個の∧は真，引数0個の∨は偽，として扱う．

->を，∨と￢を使って表す．
ド=モルガンの法則を使って，￢を最も内側まで移動する．
二重否定(￢￢)を除去する．
∧と∨の分配法則を使って，∧を最も内側まで移動する．

この時点で，トップレベルが∨，2レベル目が∧,3レベル目が命題変数,定数かその否定となる．その後，以下を繰り返し行って単純化を行う．単純化は，行えなくなるまで，あるいはそれが保証されるまで繰り返すことになる．

命題変数Aと￢Aが∧で結ばれている場合には，その∧で結ばれた部分全体は偽となるので，その部分全体を消す．また，∧で結ばれている中に真が現れていればその真を消し，偽が現れている場合には∧で結ばれた部分全体を消す．
L1∧L2∧...∧Lk-1∧Ak∧Lk+1∧...∧Lnと L1∧L2∧...∧Lk-1∧￢Ak∧Lk+1∧...∧Lnが現れている場合には，単純化してL1∧L2∧...∧Lk-1∧Lk+1∧...∧Lnとする．
トップレベルの∨で結ばれた中に真または引数0個の∧が現れていれば全体を真に書換える．

2つ目の単純化では，並び順を変えられることに注意すること．

別のアルゴリズムとして以下のようなものも考えられる．

(define (-> x y) (or (not x) y))として関数->を定義する．
与えられた論理式から命題変数を抜き出し，論理式をlambda式化する．例:(and (or x y) (not z)) -> (lambda (x y z) (and (or x y) (not z))).
命題変数のすべての真偽値の組合せに対して，論理式の真偽値を求める (すなわち，真理値表を作成する. この作業は次の項目と一体化して行えばよいかもしれない).
論理式の真偽値が真となった命題変数の真偽値の組合せ毎に，その状態を表す論理式を作成する．例: x:#t, y:#f, z:#fで論理式が真になれば，(and x (not y) (not z))という式を作る．
これらをorで結んだ式を作る．

この時点で，やはりトップレベルが∨，2レベル目が∧,3レベル目が命題変数,定数かその否定となる．その後，上に書かれた単純化をを繰り返し行う．

[kadaib32]

2値命題論理の論理式の論理和標準形を求めるプログラムを記述せよ．命題定数としては#t,#fをそれぞれ真，偽として扱い，命題変数は任意のシンボルで表すとする．入力の論理式は以下のように定義される．

命題定数と命題変数は論理式である．
0個以上の論理式を引数に持つ，andまたはorを関数とする式は論理式である．
->(imply,ならば)を関数とする，2つの論理式を引数とする式は論理式である．
notを関数とする，1つの論理式を引数とする式は論理式である．
以上のようにして帰納的にできるものだけが論理式である．

ここでは，標準形とは以下のような論理式とする．

#t,#fは標準形である．
命題変数と(not 命題変数)は標準形である(これらをリテラルと呼ぶ)．
リストであって以下を満たすものは標準形である (これを双対節とここでは呼んでおく(一般的な名前ではない))．
- 最初の要素がandである．
- 各要素はシンボルかリテラルである．
- 同じリテラルは高々1回現れる(片方が冗長)．
- あるリテラルとその否定が現れない(この場合には式全体が#fとなる)．
- 長さが3以上である(andの引数が2つ以上ある)．
- 2つ目以降の要素はリテラルの命題変数の名前の辞書式順序 (これをリテラルの順序という)でソートされている．
リストであって以下を満たすものは標準形である.
- 最初の要素がorである．
- 各要素はシンボルかリテラルか双対節である．
- 式全体が恒真式とはならない(この場合には式全体が#tと表される).
- 2つ目以降の要素が双対節の場合，その双対節は上に書かれた双対節の条件を満たしている．
- 以上を満たす同等の論理式のうちで，orの引数の個数が最小である ((or (and x y) y)は(or y)と同等であるし， (or (and x y) (and x (not y)))は(or x)と同等なのでこの条件を満たさない. また，(or (and x y z) (and x z))は(or (and x z))と同等であり， (or (and x (not y) z) (and x (not y) (not z)) t)は(or (and x (not y)) t)と同等である)．
- 長さが3以上である(orの引数が2つ以上ある.引数が1つの時にはトップレベルのorを消去できる)．
- 以下は並び順についての条件である．
  - 最初にリテラルが，双対節についての条件と同じ順序で並んでいる．
  - その後に双対節が並んでいる．
  - 双対節はソートされている．その順序は，リテラルの順序を元にした辞書式順序である．

ヒント:このページの上の方に書いてある，標準形を求めるためのどちらかの方法に従ってプログラムを書けばよい．ただし，最初のアルゴリズムの方が効率が良い場合が多いであろう．効率が良くなるようにアルゴリズムを変形できればもっと良い．

もう一つの方法として，最初に論理式から命題変数を抜き出してリストを作り，それらから考えられる限りの標準形を生成して，元の論理式と同等かどうかを一つ一つ確かめてゆくアルゴリズムが考えられる (上の条件を満たすような，一定個数の命題変数を持つ論理式は有限個しかないために，停止性は保証される)．このアルゴリズムによっても問題を解くことができるが，効率が良くないであろうと思われる．

(この課題は，命題論理の論理式の充足可能性問題を拡張したものとなっていて，NP困難であり，そのことからも多項式時間ではおそらく解けないことがすぐにわかる．したがって計算量の理論で通常いわれているいい方をすると，問題自体が実用的に解ける問題ではないということになる．しかし，それでも小さい論理式については計算機で実際に解を求めることができるし，アルゴリズムによる計算量の差も当然あり得る．)

動作例:

	==>> (and-or-normal-form '(and (or a b) (or c d)))
	(or (and a c) (and a d) (and b c) (and b d))
	==>> (and-or-normal-form '(and (or) (or c d)))
	#f
	==>> (and-or-normal-form '(or (and) (or c d)))
	#t
	==>> (and-or-normal-form '(and (and a b))
	(and a b)

自動証明に興味がある人は， Resolution や Presburger Arithmetic について調べてみるとよい．

Schemeの課題 --- (kadaib)

命題論理の論理式の標準形