Homework 5: Symbolic Evaluation of Boolean Expressions
Due: Wednesday, Oct 14, 2020 at 11:59PM
200 pts.
Overview
Write a Racket function reduce
that reduces boolean expressions (represented in Racket notation) to simplified form. For the purposes of this assignment, boolean expressions are Racket expressions constructed from:
...
The course staff is providing functions parse
and unparse
in the file parse.
rkt that rkt
that convert boolean expressions in Racket notation to a simple inductively defined type called BoolExp
and vice-versa. The coding of parse
and unparse
is not difficult, but it is tedious (like most parsing) so the course staff is providing this code rather than asking students to write it. The Racket primitive read: -> RacketExp
is a procedure of no arguments that reads a Racket expression from the console. DrRacket pops up an input box to serve as the console when (read)
is executed.
...
- a boolean constant
true
andfalse
; - a symbol
S
representing a boolean variable; (make-Not X)
whereX
is aBoolExp
;(make-And X Y) where X
andY
areBoolExps
BoolExp
s;(make-Or X Y) where X
andY
areBoolExps
BoolExp
s;(make-Implies X Y)
whereX
andY
areBoolExps
BoolExp
s; or(make-If X Y Z)
whereX
,Y
, andZ
areBoolExps
BoolExp
s.
A bool-RacketExp BoolRacketExp is either:
- a boolean constant
true
orfalse
; - a symbol
S
; (list 'not X)
whereX
is abool-RacketExp
BoolRacketExp
;(list op X Y)
whereop
is'and
,'or
, or'implies
whereX
andY
arebool-RacketExps
BoolRacketExp
s;(list 'if X Y Z)
whereX
,Y
, andZ
arebool-RacketExps
BoolRacketExp
s.
The provided functions parse
and unparse
have the following signatures.
Code Block |
---|
parse: bool-RacketExpBoolRacketExp -> BoolExp unparse: BoolExp -> bool-RacketExpBoolRacketExp |
The course staff is also providing a very simple test file\ for the eval
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.
Given a parsed input of type BoolExp
, the simplification process consists of following four phases:
- Conversion to
if
If
form implemented by the functionconvert-to-if
convertToIf
. - Normalization implemented by the function
normalize
. - Symbolic evaluation implemented by the function
eval
. - Conversion back to conventional
boolean
form implemented by the functionconvert-to-bool
convertToBool
.
A description of each of these phases follows. The reduce
function has type boolBoolRacketExp -RacketExp -> bool-RacketExpBoolRacketExp
.
Conversion to if
form
A boolean expression (BoolExp
) can be converted to if
form (a boolean expression where the only constructor is make-If
) by repeatedly applying the following rewrite rules in any order until no rule is applicable.
...
In these rules, X
and Y
denote arbitrary BoolExpsBoolExp
s}.
The conversion process always terminates (since each rewrite strictly reduces the number of logical connectives excluding {{make make-If
) and 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 convertToIf
using simple structural recursion. For each of the boolean operators And
, Or
, Not
, Implies
, and if
If
, reduce the component expressions first and then applying the matching reduction (except for if
If
for which there is no top-level reduction).
...
Code Block |
---|
(check-expect (convert-to-ifconvertToIf (make-Or (make-And 'x 'y) 'z)) (make-If (make-If 'x 'y false) true 'z)) (check-expect (convert-to-ifconvertToIf (make-Implies 'x (make-Not 'y)) (make-If 'x (make-If 'y false true) true)) |
We suggest simply traversing the tree using the structural recursion template for type BoolExp
and converting all structures (other than if
If
) 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 is the only constructor, other than variables and constants, for ifExp
.
The provided function parse: input -> boolExpBoolExp
takes a Racket expression and returns the corresponding boolExp
BoolExp
.
Normalization
An ifExp
is normalized iff every sub-expression in test
position is either a variable (symbol) or a constant (true
or false
). We call this type norm-ifExp
NormIfExp
.
For example, the ifExp
(make-If (make-If X Y Z) U V))
is not a norm-ifExp
NormIfExp
because it has an If
construction in test
position. In contrast, the equivalent ifExp
(make-If X (make-If Y U V) (make-If Z U V))
is normalized and hence is an norm-ifExp
NormIfExp
.
The normalization process, implemented by the function normalize: ifExp -> norm-ifExpNormIfExp
eliminates all if
constructions that appear in test
positions inside if
constructions. We perform this transformation by repeatedly applying the following rewrite rule (to any portion of the expression) until it is inapplicable:
...
Hint: define a sub-function head-normalize that takes three norm-ifExps
NormIfExps
X
, Y
, and Z
and constructs a norm-ifExp
NormIfExp
equivalent to (makeIf X Y Z)
. This help function processes X
because the test
position must be a variable or a constant, yet X
can be an arbitrary norm-ifExp
NormIfExp
. In contrast, (head-normalize X Y Z)
never even inspects Y
and Z
because they are already normalized and the normalizing transformations performed in head-normalize
never place these expressions in test
position.
...
Before you start writing normalize
, write the template corresponding to the inductive data definition of norm-ifExp
NormIfExp
.
Symbolic Evaluation
The symbolic evaluation process, implemented by the function eval: norm-if-form : NormIfExp environment -> norm-if-formNormIfExp
, reduces a norm-if-form
NormIfExp
to simple form. In particular, it reduces all tautologies (expressions that are always true) to true
and all contradictions (expressions that are always false) to false
.
...
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 =norm-if-form= datasubstitutions on NormIfExp
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
}.
An environment
is a (list-of binding)
binding-list
.
When the eval
function encounters a variable (symbol), it looks up the symbol in the environment and replaces the symbol it's boolean value if it exists.
...
We recommend applying the rules in the order shown from the top down until no more reductions are possible (using the constraint on the final rule). Note that the last rule should only be applied once to a given sub-expressionsubexpression.
Conversion to Boolean Form
The final phase converts an expression in (not necessarily reduced or normalized) If
form to an equivalent expression constructed from variables and { true
, false
, And
, Or
, Not
, Implies
, If
. This process eliminates every expression of the form
...
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 convertToIf (10%)
- normalize (20%)
- eval (20%)
- convert-to-bool convertToBool (10%)
- reduce (40%)