**Due:** Wednesday, Oct 14, 2020 at 11:59PM

**200 pts.**

Write a Racket function `reduce`

that reduces boolean express=
ions (represented in Racket notation) to simplified form. For the purposes =
of this assignment, boolean expressions are Racket expressions constructed =
from:

- the boolean constants
`true`

and`false`

; - boolean variables (represented by symbols other than
`true`

,=`false`

,`not`

,`and`

,`or`

, <= code>implies, and`if`

) that can be bound to either`true or`

`false`

. - the unary operator
`not`

. - the binary operators
`and`

,`or`

, and`impli= es`

, and - the ternary operator
`if`

.

The course staff is providing functions `parse`

and ```
unp=
arse
```

in the file `parse.rkt`

that convert boolean expressions in Rack=
et notation to a simple inductively defined type called B`oolExp and vice-versa. The coding of `

`parse`

and `unparse`

=
is not difficult, but it is tedious (like most parsing) so the course staf=
f is providing this code rather than asking students to write it. The Racke=
t primitive `read: -> RacketExp`

is a procedure of no argumen=
ts that reads a Racket expression from the console. DrRacket pops up an inp=
ut box to serve as the console when `(read)`

is executed.

```
```These parsing functions rely on the following Racket data definitions. G=
iven

=20
(define-struct Not (arg))
(define-struct And (left right))
(define-struct Or (left right))
(define-struct Implies (left right))
(define-struct If (test conseq alt))

=20
a `BoolExp`

is either:

- a boolean constant
`true`

and `false`

;
- a symbol
`S`

representing a boolean variable;
`(make-Not X)`

where `X`

is a `BoolExp;`

```
````(make-And X Y) where X`

and `Y`

are ```
BoolEx=
p
```

s;
`(make-Or X Y) where X`

and `Y`

are ```
BoolExp=
```

s;
`(make-Implies X Y)`

where `X`

and `Y`

=
are `BoolExp`

s; or
`(make-If X Y Z)`

where `X`

, `Y`

, an=
d `Z`

are `BoolExp`

s.

```
```A BoolRacketExp is either:

```
```- a boolean constant
`true`

or `false`

;
- a symbol
`S`

;
`(list 'not X)`

where `X`

is a ```
BoolRacketEx=
p
```

;

`(list op X Y)`

where `op`

is `'and`

,=
`'or`

, or `'implies`

where `X`

and `Y`

are `BoolRacketExp`

s;
`(list 'if X Y Z)`

where `X`

, `Y`

, and=
`Z`

are `BoolRacketExp`

s.

The provided functions `parse`

and `unparse`

have =
the following signatures.

=20
parse: BoolRacketExp -> BoolExp
unparse: BoolExp -> BoolRacketExp

=20

`The course staff is also providing a very simple test file\ for the `

functions and a file\ containing a sequence of raw input formulas (to be parsed =
by `eval`

and `parse`

function in parse.ss\). A good solution to this problem will include m=
uch more comprehensive test data for all functions, including some much lar=
ger test cases for `reduce`

. The `normalize`

function=
is difficult to test on large data because the printed output for some imp=
ortant normalized trees (represented as DAGs (Directed Acyclic Graphs) in m=
emory) is so large.

Given a parsed input of type `BoolExp`

, the simplification p=
rocess consists of following four phases:

- Conversion to I
`f`

form implemented by the function`co= nvertToIf`

. - Normalization implemented by the function
`normalize`

. - Symbolic evaluation implemented by the function
`eval`

. - Conversion back to conventional
`boolean`

form implemented b= y the function`convertToBool`

.

A description of each of these phases follows. The `reduce`

f=
unction has type `BoolRacketExp -> BoolRacketExp`

.

`if`

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

=20

(make-Not X) =09=3D>=09(make-If X false true) (make-And X Y)=09=3D>=09(make-If X Y false) (make-Or X Y)=09=09=3D>=09(make-If X true Y) (make-Implies X Y)=09=3D>=09(make-If X Y true)=20

In these rules, `X`

and `Y`

denote arbitrary `BoolExps`

`}. `

The conversion process always terminates (s=
ince each rewrite strictly reduces the number of logical connectives exclud=
ing` make-If`

and yields a unique answer independent o=
f the order in which the rewrites are performed. This property is called th=
e Church-Rosser property, after the logicians (Alonzo Church and Barkley Ro=
sser) who invented the concept.

Since the reduction rules for this phase are Church-Rosser, you can writ=
e the function `convertToIf`

using simple structural recurs=
ion. For each of the boolean operators `And`

, `Or`

, <=
code>Not, `Implies`

, and I`f`

, reduce the comp=
onent expressions first and then applying the matching reduction (except fo=
r I`f`

for which there is no top-level reduction).

The following examples illustrate the conversion process:

=20

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

We suggest simply traversing the tree using the structural recursion tem=
plate for type `BoolExp`

and converting all structures (other th=
an `If`

) to the corresponding `if`

structures.

Write an inductive data definition and template for boolean formulas in =
`if`

form, naming this type `ifExp`

. (Note: ```
mak=
e-If
```

is the only constructor, other than variables and constant=
s, for `ifExp`

.

The provided function `parse: input -> BoolExp`

takes a Ra=
cket expression and returns the corresponding `BoolExp`

.

An `ifExp`

is *normalized* iff every sub-expression in=
`test`

position is either a variable (symbol) or a constant (`false`

). We call this type `NormIfExp .`

```
```

`For example, the `

`ifExp`

```
(make-If (make-If X Y Z) U V))=
```

is not a `NormIfExp`

because it has an `If`

c=
onstruction in `test`

position. In contrast, the equivalent `(make-If X (make-If Y U V) (make-If Z U V))`

is =
normalized and hence is an `NormIfExp`

.

The normalization process, implemented by the function ```
normalize: =
ifExp -> NormIfExp
```

eliminates all `if`

constructions t=
hat appear in `test`

positions inside `if`

constructi=
ons. We perform this transformation by repeatedly applying the following re=
write rule (to any portion of the expression) until it is inapplicable:

=20

(make-If (make-If X Y Z) U V) =3D>=09 (make-If X (m= ake-If Y U V) (make-If Z U V)).=20

This transformation always terminates and yields a unique answer indepen= dent of the order in which rewrites are performed. The proof of this fact i= s left as an optional exercise.

In the `normalize`

function, it is critically important not t=
o duplicate any work, so the order in which reductions are made really matt=
ers. Do **NOT** apply the normalization rule above unless `V`

are already normalized, because the rule dupl=
icates both `U`

and `V`

. If you reduce the ```
cons=
equent
```

and the `alternative`

(`U`

and ```
V<=
/code> in the left hand side of the rule above) before reducing the
```

```
t=
est
```

, `normalize`

runs in linear time (in the number of no=
des in the input); if done in the wrong order it runs in exponential time i=
n the worst case. (And some of our test cases will exhibit this worst case =
behavior.)

```
```Hint: define a sub-function head-normalize that takes three ```
NormIf=
Exps
```

`X`

, `Y`

, and `Z`

and construc=
ts a `NormIfExp`

equivalent to `(makeIf X Y Z)`

. This=
help function processes `X`

because the `test`

posit=
ion must be a variable or a constant, yet `X`

can be an arbitrar=
y `NormIfExp`

. In contrast, `(head-normalize X Y Z)`

=
never even inspects `Y`

and `Z`

because they are alre=
ady normalized and the normalizing transformations performed in ```
head-=
normalize
```

never place these expressions in `test`

positio=
n.

`The following examples illustrate how the `

functions behave:`normalize`

and

=20

(check-expect (head-normalize 'x 'y 'z) (make-If 'x 'y 'z)) (check-expect (head-normalize true 'y 'z) (make-If true 'y 'z)) (check-expect (head-normalize false 'y 'z) (make-If false 'y 'z)) (check-expect (head-normalize (make-If 'x 'y 'z) 'u 'v) (make-If 'x (make-I= f 'y 'u 'v) (make-If 'z 'u 'v))) (check-expect (head-normalize (make-If 'x (make-If 'yt 'yc 'ya) (make-If 'z= t 'zc 'za)) 'u 'v) (make-If 'x (make-If 'yt (make-If 'yc 'u 'v) (make-If 'ya 'u 'v)) (make-If = 'zt (make-If 'zc 'u 'v) (make-If 'za 'u 'v)))) (check-expect (normalize true) true) (check-expect (normalize false) false) (check-expect (normalize 'x) 'x) (check-expect (normalize (make-If 'x 'y 'z)) (make-If 'x 'y 'z)) (check-expect (normalize (make-If (make-If 'x 'y 'z) 'u 'v)) (make-If 'x (m= ake-If 'y 'u 'v) (make-If 'z 'u 'v)))=20

Once a large formula has been normalized, do not try to print it unless = you know that the formula is small! The printed form can be exponentially l= arger than the internal representation (because the internal representation= can share subtrees).

Before you start writing `normalize`

, write the template corr=
esponding to the inductive data definition of `NormIfExp`

.

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 (express=
ions that are always false) to `false`

.

```
```Symbolic evaluation applies the following rewrite rules to an expression=
until none is applicable (with one exception discussed below):

=20
(make-If true X Y)=09 =3D>=09X
(make-If false X Y)=09 =3D>=09Y
(make-If X true false) =3D>=09X
(make-If X Y Y) =09 =3D>=09Y
(make-If X Y Z)=09 =3D>=09(make-If X Y[X <- true\] Z[X <- =
false])

=20
The notation `M[X <- N]`

means `M`

with all occ=
urrences of the symbol `X`

replaced by the expression `N. It is very costly to actually perform these substitutions on ````
No=
rmIfExp
```

data. To avoid this computational expense, we simply ma=
intain a list of bindings which are pairs consisting of symbols (variable n=
ames) and boolean values {`true`

, `false`

. The follow=
ing data definition definition formally defines the `binding`

ty=
pe.

```
```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 `binding-list`

.

When the `eval`

function encounters a variable (symbol), it l=
ooks up the symbol in the environment and replaces the symbol it's boolean =
value if it exists.

These rewrite rules do not have the Church-Rosser property. The last two=
rewrite rules are the spoilers; the relative order in which they are appli=
ed can affect the result in some cases. However, the rewrite rules do have =
the Church-Rosser property on expressions which are tautologies or contradi=
ctions.

If the final rule is applied only when `X`

actually occurs in=
either `Y`

or `Z`

, then the symbolic evaluation proc=
ess is guaranteed to terminate. In this case, every rule either reduces the=
size of the expression or the number of variable occurrences in it.

We recommend applying the rules in the order shown from the top down unt=
il 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 subexpress=
ion.

# Conversion to Boolean Form

```
The final phase converts an expression in (not necessarily reduced or no=
rmalized)
````If`

form to an equivalent expression constructed from=
variables and { `true`

, `false`

, `And`

, <=
code>Or

, `Not`

, `Implies`

, `If`

. Th=
is process eliminates every expression of the form

=20
(make-If X Y Z)

=20
where one of the arguments {`X`

, `Y`

, `Z is a constant { ``true`

, `false`

}.

```
```Use the following set of reduction rules to perform this conversion

=20
(make-If X false true) =3D> (make-Not X)
(make-If X Y false) =3D> (make-And X Y)
(make-If X true Y) =3D> (make-Or X Y)
(make-If X Y true) =3D> (make-Implies X Y)

=20
where `X`

, `Y`

, and `Z`

are arbitrary=
`If`

forms. This set of rules is Church-Rosser, so the rules ca=
n safely be applied using simple structural recursion.

# Points Dsitribution

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

```
------=_Part_24700_1032227747.1652829415162--
```