第10章 型とクラスの定義 #3

10.4 恒真式

命題論理式を表す型を作り、与えられた命題が恒真式（式に含まれる変数の値に関係なく、常に真となる式）かどうかを判定する関数を書く。

まずは命題の型を定義。

真理値(True, False)

Const Bool

変数(A, B, ... , Z)

Var Char

否定(￢)

Not Prop

論理積(∧)

And Prop Prop

論理包含(⇒)

Imply Prop Prop

data Prop = Const Bool
  | Var Char
  | Not Prop
  | And Prop Prop
  | Imply Prop Prop

変数名を真理値に対応付ける置換表を定義して、与えられた置換表を元に命題の値を評価する関数も書く。

type Subst = Assoc Char Bool

eval               :: Subst -> Prop -> Bool
eval _ (Const b)   =  b
eval s (Var x)     =  find x s
eval s (Not p)     =  not (eval s p)
eval s (And p q)   =  eval s p && eval s q
eval s (Imply p q) =  eval s p <= eval s q

命題の中から変数（重複あり）を抽出する関数は

vars             :: Prop -> [Char]
vars (Const _)   =  []
vars (Var x)     =  [x]
vars (Not p)     =  vars p
vars (And p q)   =  vars p ++ vars q
vars (Imply p q) =  vars p ++ vars q

変数の数に対応して、とり得る真理値の組み合わせを列挙する関数は

bools   :: Int -> [[Bool]]
bools 0 = [[]]
bools n = map (False:) bss ++ map (True:) bss
          where bss = bools (n-1)

-- bools n =  map (map conv . make n . int2bin) [0..limit]
--   where
--     limit = (2 ^ n) - 1
--     make n bs = take n (bs ++ repeat 0)
--     conv 0 = False
--     conv 1 = True
--     int2bin 0 = []
--     int2bin n = n `mod` 2 : int2bin (n `div` 2)

道具がそろってきたので、命題に含まれる変数がとり得る真理値の組み合わせを置換表にして列挙する関数を定義し、それを使って恒真式の判定関数を書く。

substs   :: Prop -> [Subst]
substs p =  map (zip vs) (bools (length vs))
            where vs = rmdups (vars p)

isTaut   :: Prop -> Bool
isTaut p =  and [eval s p | s <- substs p]