isTaut

*Main> isTaut (Imply (And (Var 'A') (Var 'B')) (Var 'A'))
Const True
*Main> isTaut (Imply (And (Var 'A') (Not (Var 'A'))) (Const False))
Const True

恒等式かどうか判定するプログラム．これも『プログラミング Haskell』に載っていた例題だけどあっちでは真理値表を使っていたぽくてつまらないので，実際に式を組み換えて判定する物を書いてみた．

data Prop = Const Bool
          | Var Char
          | Not Prop
          | Or Prop Prop
          | And Prop Prop
          | Imply Prop Prop
          deriving (Eq, Ord, Show)


isTaut :: Prop -> Prop

isTaut (Const b) = (Const b)
isTaut (Var x) = (Var x)
isTaut (Not p) = rule (Not (isTaut p))
isTaut (Or p1 p2) = rule (Or (isTaut p1) (isTaut p2))
isTaut (And p1 p2) = rule (And (isTaut p1) (isTaut p2))
isTaut (Imply p1 p2) = rule (Or (isTaut (Not p1)) (isTaut p2))



rule :: Prop -> Prop


rule (Const b) = (Const b)
rule (Not (Const b)) = (Const (not b))
rule (Or (Const b1) (Const b2)) = (Const (b1 || b2))
rule (And (Const b1) (Const b2)) = (Const (b1 && b2))
rule (Imply (Const b1) (Const b2)) = (Const (not b1 && b2))


rule (Var x) = (Var x)


rule (Not (Not p)) = rule p
rule (Not (Or p1 p2)) = rule (And (rule (Not (rule p1))) (rule (Not (rule p2))))
rule (Not (And p1 p2)) = rule (Or (rule (Not (rule p1))) (rule (Not (rule p2))))


rule (Or (Const True) p) = (Const True)
rule (Or p (Const True)) = (Const True)
rule (Or (Const False) p) = p
rule (Or p (Const False)) = p

rule (Or (Not p1) p2) | (rule p1) == (rule p2) = (Const True)
rule (Or p1 (Not p2)) | p1 == p2 = (Const True)
rule (Or p1 p2)       | p1 == p2 = p1

rule (Or (Or p1 p2) p3) | p1 == p3 = rule (Or p2 p3)
                        | p2 == p3 = rule (Or p1 p3)
rule (Or (Or p1 p2) p3) | (p1 == (Not p3) || p2 == (Not p3)) = (Const True)
rule (Or (Or p1 p2) p3) | ((Not p1) == p3 || (Not p2) == p3) = (Const True)

rule (Or p1 (Or p2 p3)) | p1 == p2 = rule (Or p1 p3) 
                        | p1 == p3 = rule (Or p1 p2)
rule (Or p1 (Or p2 p3)) | ((Not p1) == p2 || (Not p1) == p3) = (Const True)
rule (Or p1 (Or p2 p3)) | (p1 == (Not p2) || p1 == (Not p3)) = (Const True)

rule (Or (And p1 p2) p3) | (p1 == p3 || p2 == p3) = p3
rule (Or (And p1 p2) p3) | p1 == (Not p3) = rule (And p2 p3)
                         | p2 == (Not p3) = rule (And p1 p3)
rule (Or p1 (And p2 p3)) | (p1 == p2 || p1 == p3) = p1
rule (Or p1 (And p2 p3)) | (Not p1) == p3 = rule (And p1 p2)
                         | (Not p2) == p3 = rule (And p1 p3)


rule (And (Const False) p) = (Const False)
rule (And p (Const False)) = (Const False)
rule (And (Const True) p) = p
rule (And p (Const True)) = p

rule (And (Not p1) p2) | p1 == p2 = (Const False)
rule (And p1 (Not p2)) | p1 == p2 = (Const False)
rule (And p1 p2) | p1 == p2 = p1

rule (And (And p1 p2) p3) | p1 == p3 = rule (And p2 p3)
                        | p2 == p3 = rule (And p1 p3)
rule (And (And p1 p2) p3) | (p1 == (Not p3) || p2 == (Not p3)) = (Const False)
rule (And (And p1 p2) p3) | ((Not p1) == p3 || (Not p2) == p3) = (Const False)

rule (And p1 (And p2 p3)) | p1 == p2 = rule (And p1 p3) 
                        | p1 == p3 = rule (And p1 p2)
rule (And p1 (And p2 p3)) | ((Not p1) == p2 || (Not p1) == p3) = (Const False)
rule (And p1 (And p2 p3)) | (p1 == (Not p2) || p1 == (Not p3)) = (Const False)

rule (And (Or p1 p2) p3) | (p1 == p3 || p2 == p3) = p3
rule (And (Or p1 p2) p3) | p1 == (Not p3) = rule (Or p2 p3)
                         | p2 == (Not p3) = rule (Or p1 p3)
rule (And p1 (Or p2 p3)) | (p1 == p3 || p1 == p2) = p1
rule (And p1 (Or p2 p3)) | (Not p1) == p3 = rule (Or p1 p2)
                         | (Not p2) == p3 = rule (Or p1 p3)


rule p = p