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:

...

A description of each of these phases follows. The reduce function has type BoolRacketExp -> BoolRacketExp.

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.

...

(check-expect  (ConverToIfconvertToIf (make-Or (make-And 'x 'y) 'z))    (make-If (make-If 'x 'y false) true 'z))
(check-expect  (ConverToIfconvertToIf (make-Implies 'x (make-Not 'y))   (make-If 'x (make-If 'y false  true) true))

...

The provided function parse: input -> BoolExp takes a Racket expression and returns the corresponding 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.

...

(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

• ConverToIf convertToIf (10%)
• normalize (20%)
• eval (20%)
• convert-to-bool convertToBool (10%)
• reduce (40%)