*Due:* Friday, Feburary 26, 2010

*Extra

{code}
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 {{boolExps

}};
* {{(make-Or X Y) where X}} and {{Y}} are {{boolExps

}};
* {{(make-Implies X Y)}} where {{X}} and {{Y}} are {{boolExps}}; or

* {{(make-If X Y Z)}} where {{X}} , {{Y}} , and {{Z}} are {{boolExps}}.

A bool-SchemeExp is either:

* a boolean constant {{true}} or {{false}};

* a symbol {{S

}};
* {{(list 'not X)}} where {{X}} is a {{bool\-SchemeExp

}} ;
* {{(list op X Y)}} where {{op}} is {{'and}} , {{'or

}} , or {{'implies}} where {{X}} and {{Y}} are {{bool\-SchemeExp}}s;

* {{(list 'if X Y Z)}} where {{X}}, {{Y}}, and {{Z}} are {{bool\-SchemeExp}}s.

The provided functions {{parse

consists of following four phases:

* Conversion to {{if}} form implemented by the function {{convert\-to\-if

reduces the number of logical connectives in the expression) 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 simple structural recursion.  For each of the boolean operators {{And}} , {{Or}} , {{Not}} , and {{Implies}} , reduce the component expressions first and then applying the matching reduction (except for {{if}} for which there is no top-level reduction).

The following examples illustrate the conversion process:

{code

}
(check-expect  (convert-to-if (make-Or (make-And 'x 'y) 'z))    (make-If (make-If 'x 'y false) true 'z))
(check-expect  (convert-to-if (make-Implies 'x (make-Not 'y))   (make-If 'x (make-If 'y false  true) true))
{code}

We suggest simply traversing the tree using the structural recursion template for type {{boolExp}} and converting all structures (other than {{if}}s) 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 the only constructor, other than variables and constants, for

{code

}
This transformation always terminates and yields a unique answer
 independent of the order in which rewrites are performed.
 The proof of this fact is left as an optional exercise.

In the {{normalize}} function, it is critically important not to duplicate any work, so
 the order in which reductions are made really matters.  Do *NOT* apply
 the normalization rule above unless {{U}} and {{V}} are already
 normalized, because the rule duplicates both {{U}} and {{V}}.  If you
 reduce the _{{consequent_}} and the _{{alternative_}} (={{U=}} and ={{V=}} in the left
 hand side of the rule above) before reducing the _{{test_}}, =normalize=
{{normalize}} runs in linear time (in the number of nodes in the input); if done in
 the wrong order it runs in exponential time in 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 ={{norm-ifExp=s =X=, =Y=ifExps}} {{X}}, {{Y}}, and =Z=
{{Z}} and constructs a ={{norm-ifExp=}} 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=}}. 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.

The following examples illustrate how the ={{normalize=}} and ={{head-normalize=}} functions behave:
{code}
(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-If 'y 'u 'v) (make-If 'z 'u 'v)))

(check-expect (head-normalize (make-If 'x (make-If 'yt 'yc 'ya) (make-If 'zt '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 (make-If 'y 'u 'v) (make-If 'z 'u 'v)))

{code

}

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 larger than the internal representation (because the internal representation can share subtrees).

Before you start writing ={{normalize=}}, write the template corresponding to the inductive data definition of ={{norm-ifExp=}}.

----+h1. Symbolic Evaluation

The symbolic evaluation process, implemented by the function ={{eval: norm-if-form environment \-> norm-if-form=}}, reduces a ={{norm\-if\-form=
}} 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=}}.
<p>
Symbolic evaluation applies the following rewrite rules to
 an expression until
 none is applicable (with one exception
discussed below):

{code}
(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\])

{code

}
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= 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)
 v)}} where s is a symbol (a variable) and v is a boolean value (an element of { =true=, =false= }.

An =environment= is a =(listOf binding)=.

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.
<p>
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 applied can affect the result in some cases.
However, the rewrite rules
do have the Church-Rosser property on expressions which are
tautologies or contradictions.
<p>
If the final rule is applied only when
=X= actually occurs in either
=Y= or =Z=,
then the symbolic evaluation process
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
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-expression.

----+Conversion to Boolean Form

The final phase converts an expression in (not necessarily reduced) =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
{code}
(make-If X Y Z)

{code

}
where one of the arguments {=X=, =Y=, =Z=} is a constant
{ =true=, =false=}.

Use the following set of reduction rules to perform this conversion
{code}
(make-If  X  false true)  =>  (make-Not X)

(make-If  X  Y  false)    =>  (make-And  X  Y)

(make-If  X  true  Y)     =>  (make-Or

  X  Y)

(make-If  X  Y  true)     =>  (make-Implies  X  Y)

YYYcodeYYY

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.