Page History

...

• 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 {{boolExp}}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 , and Z are {{boolExp}}s.

...

• 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 and unparse have the following signatures.

...

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

...

We suggest simply traversing the tree using the structural recursion template
for type boolExp and converting all structures (other than =ifs=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 ifExp

a ={{boolExp=}} is either:
   *  a boolean value ={{true=}} and ={{false=}};
   *  a symbol ={{s=}} representing a boolean variable;
   *  ={{(make-Not M)=}} where ={{M=}} is a ={{boolExp=}};
   *  ={{(make-And M N)}} where ={{M=}} and ={{N=}} are ={{boolExps=}};
   *  ={{(make-Or M N)}} where ={{M=}} and ={{N=}} are ={{boolExps=}};
   *  =(make-Implies M N) where =M= and =N= are =boolExps=; or
   *  =(make-If M N P)= where =M=, =N=, and =P= are =boolExps=.

The provided function ={{parse: input -> boolExp=}} takes a Scheme 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=.

For example, the =ifExp=

...