# 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.

...

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 `NormIfExp`

.

...

Before you start writing `normalize`

, write the template corresponding to the inductive data definition of `NormIfExp`

.

# Symbolic Evaluation

The symbolic evaluation process, implemented by the function `eval: NormIfExp environment -> NormIfExp`

, reduces a `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 substitutions 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.

...

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 subexpression.

# 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

- convertToIf (10%)
- normalize (20%)
- eval (20%)
- convertToBool (10%)
- reduce (40%)