...

Code Block |
---|

(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)) |

...

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`

.

...

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

...

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%)