...
- 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.
...
The course staff is also providing a very simple test file for the eval
function and reduce
functions and a file containing a sequence of raw input formulas (to be parsed by parse
function in parse.ss). A good solution to this problem will include much more comprehensive test data for all functions, including some much larger test cases for reduce
. The normalize
function is difficult to test on large data because the printed output for some important normalized trees (represented as DAGs (Directed Acyclic Graphs) in memory) is so large.
...
Conversion to if
form
A boolean expression (boolExp
) can be converted to if
form by repeatedlyapplying repeatedly applying the following rewrite rules in any order until no rule is applicable.
Code Block |
---|
(make-Not X) => (make-If X false true) (make-And X Y) => (make-If X Y false) (make-Or X Y) => (make-If X true Y) (make-Implies X Y) => (make-If X Y true) |
In these rules, X
and Y
denote arbitrary boolExps}. The conversion process always terminates (since each rewrite strictly reduces the number of logical connectives
in the expressionexcluding {{make-If
) and yields a unique answer independent of the order in which the rewrites are performed. This property is called the Church-Rosser property, after the logicians (Alonzo Church and Barkley Rosser) who invented the concept.
Since the reduction rules for this phase are Church-Rosser, you can write the function convert-to-if
using simple structural recursion. For each of the boolean operators And
, Or
, Not
, Implies
, and Implies
if
, reduce the component expressions first and then applying the matching reduction (except for if
for which there is no top-level reduction).
...
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
.
A boolExp
is either:
- a boolean value
true
andfalse
; - a symbol
s
representing a boolean variable; (make-Not M)
whereM
is aboolExp
;(make-And M N)
whereM
andN
areboolExps
;(make-Or M N)
whereM
andN
areboolExps
;(make-Implies M N)
whereM
andN
areboolExps
; or(make-If M N P)
whereM
,N
, andP
areboolExps
.
The The provided function parse: input -> boolExp
takes a Scheme expression and returns the corresponding boolExp
.
...
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 {{ Wiki Markup 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 =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}} {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%)