...

Conversion to if form

A boolean expression (boolExp) can be converted to if form by repeatedlyapplying repeatedly applying the following rewrite rules in any order until no rule is applicable.

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

In these rules, X and Y denote arbitrary boolExps}. The conversion process always terminates (since each rewrite strictly reduces the number of logical connectives in the expressionexcluding {{make-If) 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 , Implies , and Implies if , reduce the component expressions first and then applying the matching reduction (except for if for which there is no top-level reduction).

...