# 函数程序设计实验十二：带变量的布尔表达式

``````module Lab3 where
import Data.List

{-

-真命题(记作T)和假命题(记作F)是命题；
-由一个字母表示的命题变元是一个命题；
-如果P是命题,则它的否定是一个命题,记作~P；"~"称为否定联结词；
-如果p,q是命题,则它们的合取是一个命题,记作p&&q; "&&"称为合取联结词；
-如果p,q是命题,则它们的析取是一个命题,记作p||q; "||"称为析取联结词；
-如果p,q是命题,则它们的蕴含是一个命题,记作p=>q; "=>"称为蕴含联结词；
-所有的命题由以上规则经过有限步生成。

-}
data Prop=Const Bool
| Var Char
| Not Prop
| And Prop Prop
| Or Prop Prop
| Imply Prop Prop
deriving Eq

{-

-}
instance Show Prop where
show (Const True)="True"
show (Const False)="False"
show (Var x)=[x]
show (Not x)="~"++show x
show (And x y)=(show x)++"&&"++(show y)
show (Or x y)=(show x)++"||"++(show y)
show (Imply x y)=(show x)++"=>"++(show y)

{-

A&&~A
A||~A
A=>(A&&B)
-}
p1=And (Var 'A') (Not (Var 'A'))
p2=Or (Var 'A') (Not (Var 'A'))
p3=Imply (Var 'A') (And (Var 'A') (Var 'B'))

{-

-}
type Subst=[(Char,Bool)]

{-

-}
eval::Subst->Prop->Bool

{-

>eval [('A',True),('B',False)] p3
False
-}
eval sub (Const p)=p
eval sub (Var p)=(getBool sub p) where
getBool sub x=
if length xs >1
then error "Variable has more than 2 values."
where xs=[k|(y,k)<-sub,x==y]
eval sub (Not p)=not (eval sub p)
eval sub (And p q)=(eval sub p)&&(eval sub q)
eval sub (Or p q)=(eval sub p)||(eval sub q)
eval sub (Imply p q)=((eval sub p)&&(eval sub q))||(not (eval sub p))

{-

-}
vars::Prop->[Char]
substs::Prop->[Subst]

{-

vars p3=['A','B']
substs p3=
[
[('A',True),('B',True)],
[('A',True),('B',False)],
[('A',False),('B',True)],
[('A',False),('B',False)]
]
-}
vars (Const x)=[]
vars (Var x)=[x]
vars (Not p)=vars p
vars (And p q)=nub((vars p)++(vars q))
vars (Or p q)=nub((vars p)++(vars q))
vars (Imply p q)=nub((vars p)++(vars q))

substs p=getsub (vars p) where
getsub []=[]
getsub [x]=[[(x,True)]]++[[(x,False)]]
getsub (x:xs)=[(x,True):a|a<-getsub(xs)]++[(x,False):a|a<-getsub(xs)]

{-

-}
isTaut::Prop->Bool

{-

>isTaut p1
False
>isTaut p2
True
-}
isTaut p=testisTaut p (substs p) where
testisTaut p [x]=(eval x p)
testisTaut p (x:xs)=if (eval x p) then testisTaut p xs else False
``````