...
- a boolean constant
true
orfalse
; - a symbol
S
; (list 'not X)
whereX
is abool-SchemeExp
;(list op X Y)
whereop
is'and
,'or
, or'implies
whereX
andY
are {{bool-
SchemeExp}}sSchemeExps
;(list 'if X Y Z)
whereX
,Y
, andZ
are {{bool-
SchemeExp}}sSchemeExps
.
The provided functions parse
and unparse
have the following signatures.
...
We suggest simply traversing the tree using the structural recursion template for type boolExp
and converting all structures (other than if}}s
) to the corresponding {{if
structures.
Write an inductive data definition and template for boolean formulas in if
form, naming this type ifExp
. (Note: make-If
is the only constructor, other than variables and constants, for ifExp
.
...
Code Block |
---|
(make-If true X Y) => X (make-If false X Y) => Y (make-If X true false) => X (make-If X Y Y) => Y (make-If X Y Z) => (make-If X Y\[X <\- true\] Z\[X <\- false\]) |
...
The notation {{M
\[X
<-
N
\]
}} means {{M
}} with all occurrences of the symbol {{X
}} replaced by the expression {{N}}. It is very costly to actually perform these subtitutions on expression N
. It is very costly to actually perform these subtitutions on =norm-if-form= data. To avoid this computational expense, we simply maintain a list of bindings which are pairs consisting of symbols (variable names) and boolean values {{{true
}}, {{false
}}. The following data definition definition formally defines the {{binding
}} type.
A binding
is a pair (make-binding s v)
where s is a symbol (a variable) and v
is a boolean value (an element of { true
, false
}.
...
where X
, Y
, and Z
are arbitrary If
forms. This set of rules is Church-Rosser, so the rules can safely be applied using simple structural recursion.
Points Dsitribution
- convert-to-if (10%)
- normalize (20%)
- eval (20%)
- convert-to-bool (10%)
- reduce (40%)