CC BY 4.0 (除特别声明或转载文章外)
如果这篇博客帮助到你,可以请我喝一杯咖啡~
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
module Lab3 where
import Data.List
{-
一个布尔表达式就像一个算术表达式,只是这里的值都是布尔值True和False,
其中的变量也只能代入布尔值,各种运算用运算表给出。
布尔表达式的另一种解读是表示命题,如文件lab3.pdf所讲。
如果不理解命题,就看作布尔表达式好了。
本作业要求判断一个布尔表达式是不是永真式:即无论将变量代入什么值,其结果总是True。
一、定义命题类型及其Show特例
命题的集合可以如下定义
-真命题(记作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
{-
习题1
试将类型Prop定义成类Show的特例,使得Prop中元素能够显示成定义中我们习惯的表示。
例如,Var 'A',And (Var 'P') (Var 'Q')分别显示成A和P&&Q等。
-}
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)
{-
习题2
定义下列值p1,p2,p3::Prop
使得它们个表示下列命题:
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'))
{-
二、命题真值表
一个命题或者真,或者假。
例如,不包含变元的命题T表示真命题,命 题F表示假命题。
包含变元的命题的真假依赖于变元表示命题的真假,
所以,一个命题可以看作它包含的变元的函数,称为真值函数,
其中每个变元的取 值为真或者假,分别用TVue和False表示。
每个命题的取值和其中变元的关系可以用一个表来表示,称之为命题函数的真值表。
以下是命题联结词的真值表:
对应任意的命题函数,给定变元的一个代换,根据上述真值表可计算相应的真值。
例如,命题p3:A=>(A && B)在代换[('A',True),('B',False)]的真值是False。
我们可以用下列类型表示代换:
-}
type Subst=[(Char,Bool)]
{-
习题3
试根据以上解释定义函数:
-}
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."
else head xs
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))
{-
习题4
试定义下列函数:
-}
vars::Prop->[Char]
substs::Prop->[Subst]
{-
其中vars p给出命题p中出现的所有不同变元,substs p给出命题p中变元的所有可能代换。例如
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)]
{-
三、定义一个判断命题是否永真的函数
如果一个命题函数在变元的任意代换下真值是True,则称之为永真式。
例如,命题p2是永真式。
试定义判定一个命题是否永真式的函数,并说明你的函 数定义的正确性:
习题5
-}
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