-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathp3.sc
181 lines (160 loc) · 6.19 KB
/
p3.sc
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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
;;From p2.sc solutions
(define (propositions-in formula)
(cond ((symbol? formula) (list formula))
((boolean? formula) '())
((and (list? formula) (not (null? formula)))
(case (first formula)
((not) (if (= (length formula) 2)
(propositions-in (second formula))
(panic "Unrecognized formula")))
((and) (reduce unionq (map propositions-in (rest formula)) '()))
((or) (reduce unionq (map propositions-in (rest formula)) '()))
(else (panic "Unrecognized formula"))))
(else (panic "Unrecognized formula"))))
;;From p2.sc solutions
(define (all-truth-assignments propositions)
(if (null? propositions)
'(())
(let ((truth-assignments (all-truth-assignments (rest propositions))))
(append (map (lambda (truth-assignment)
(cons (list (first propositions) #t) truth-assignment))
truth-assignments)
(map (lambda (truth-assignment)
(cons (list (first propositions) #f) truth-assignment))
truth-assignments)))))
;;From p2.sc solutions
(define (lookup-proposition proposition truth-assignment)
(cond ((null? truth-assignment) (panic "Proposition not in truth assignment"))
((eq? proposition (first (first truth-assignment)))
(second (first truth-assignment)))
(else (lookup-proposition proposition (rest truth-assignment)))))
;;From p2.sc solutions
(define (boolean-evaluate formula truth-assignment)
(cond ((symbol? formula) (lookup-proposition formula truth-assignment))
((boolean? formula) formula)
((and (list? formula) (not (null? formula)))
(case (first formula)
((not) (if (= (length formula) 2)
(not (boolean-evaluate (second formula) truth-assignment))
(panic "Unrecognized formula")))
((and) (every (lambda (formula)
(boolean-evaluate formula truth-assignment))
(rest formula)))
((or) (some (lambda (formula)
(boolean-evaluate formula truth-assignment))
(rest formula)))
(else (panic "Unrecognized formula"))))
(else (panic "Unrecognized formula"))))
;;From p2.sc solutions
(define (truth-table formula)
(map (lambda (truth-assignment)
(list truth-assignment (boolean-evaluate formula truth-assignment)))
(all-truth-assignments (propositions-in formula))))
;;From slides lecture 6
(define (boolean-simplify e) (rewrite *rules* e))
;;From rewrite.sc
(define (pattern-variable? p) (member p '(phi phi1 phi2 phi3)))
;;From slides lecture 6
(define (pattern-list-variable? p) (member p '(phi... phi1... phi2... phi3...)))
;;From rewrite.sc
(define (inconsistent-binding? b1 b2)
(and (eq? (first b1) (first b2)) (not (equal? (second b1) (second b2)))))
;;From rewrite.sc
(define (inconsistent-bindings? r1 r2)
(some (lambda (b1) (some (lambda (b2) (inconsistent-binding? b1 b2)) r2)) r1))
;;From rewrite.sc
(define (merge-results-of-match r1 r2)
(if (or (eq? r1 #f) (eq? r2 #f) (inconsistent-bindings? r1 r2))
#f
(append r1 r2)))
;;From slides lecture 6
(define (match pattern expression)
(cond ((pattern-variable? pattern) (list (list pattern expression)))
((pattern-list-variable? pattern)
(panic "Pattern list variable not at end of list"))
((and (list? pattern)
(= (length pattern) 1)
(pattern-list-variable? (first pattern)))
(list (list (first pattern) expression)))
((and (list? pattern) (not (null? pattern)))
(if (and (list? expression) (not (null? expression)))
(append (match (first pattern) (first expression))
(match (rest pattern) (rest expression)))
(list #f)))
((equal? pattern expression) '())
(else (list #f))))
;;From slides lecture 6
(define (instantiate pattern bindings)
(cond ((pattern-variable? pattern)
(lookup-pattern-variable pattern bindings))
((pattern-list-variable? pattern)
(panic "Pattern list variable not at end of list"))
((and (list? pattern)
(= (length pattern) 1)
(pattern-list-variable? (first pattern)))
(lookup-pattern-variable (first pattern) bindings))
((and (list? pattern) (not (null? pattern)))
(cons (instantiate (first pattern) bindings)
(instantiate (rest pattern) bindings)))
(else pattern)))
;;From slides lecture 6
(define (lookup-pattern-variable p bindings)
(cond ((null? bindings) (panic "unbound pattern variable"))
((eq? (first (first bindings)) p) (second (first bindings)))
(else (lookup-pattern-variable p (rest bindings)))))
;;From slides lecture 6
(define (applicable? rule expression)
(not (memq #f (match (first rule) expression))))
;;From slides lecture 6
(define (first-applicable-rule rules expression)
(cond ((null? rules) #f)
((applicable? (first rules) expression) (first rules))
(else (first-applicable-rule (rest rules) expression))))
;;From slides lecture 6
(define (apply-rule rule expression)
(instantiate (third rule) (match (first rule) expression)))
;;From slides lecture 6
(define (apply-rules rules expression)
(let ((rule (first-applicable-rule rules expression)))
(if rule
(rewrite rules (apply-rule rule expression))
expression)))
;;From slides lecture 6
(define (rewrite rules expression)
(if (list? expression)
(apply-rules
rules
(map (lambda (expression) (rewrite rules expression))
expression))
expression))
(define *rules*
'(((not #f) -~> #t)
((not #t) -~> #f)
((not (not phi)) -~> (phi))
((and) -~> #t)
((and phi) -~> phi)
((and phi #f) -~> #f)
((and phi #t) -~> (and phi))
((and #t phi...) -~> (and phi...))
((and #f phi...) -~> #f)
((and phi1 phi2 phi3 phi...) -~> (and phi1 (and phi2 (and phi3 phi...))))
((and phi (not phi) phi...) -~> #f)
((and (not phi) phi phi...) -~> #f)
((or) -~> #f)
((or phi) -~> phi)
((or phi #f) -~> (or phi))
((or phi #t) -~> #t)
((or #t phi...) -~> #t)
((or #f phi...) -~> (or phi...))
((or phi1 phi2 phi3 phi...) -~> (or phi1 (or phi2 (or phi3 phi...))))
((or phi (not phi) phi...) -~> #t)
((or (not phi) phi phi...) -~> #t)))
(define (truth-tables-match? p pp)
(let ((I (all-truth-assignments (propositions-in p))))
(equal?
(map (lambda (truth-assignment)
(list truth-assignment
(boolean-evaluate p truth-assignment))) I)
(map (lambda (truth-assignment)
(list truth-assignment
(boolean-evaluate pp truth-assignment))) I))))