Homework 6: Symbolic Evaluation of Boolean Expressions

Due: Friday Monday, Feburary 26March 1, 2010

Extra Credit (100 pts.)

Overview

Write a Scheme function reduce that reduces boolean expressions (represented in Scheme notation) to simplified form. For the purposes of this assignment, boolean expressions are Scheme expressions constructed from:

...

The course staff is providing function functions parse and unparse in the file parse.ss that convert boolean expressions in Scheme notation to a simple inductively defined type called boolExp and vice-versa. The coding of parse and unparse is not difficult, but it is tedious (like most parsing) so the course staff is providing this code rather than asking students to write it. The Scheme primitive read: -> SchemeExp is a procedure of no arguments that reads a Scheme expression from the console. DrScheme pops up an input box to serve as the console when (read) is executed.

These parsing functions rely on the following Scheme data definitions:. Given

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

...

• 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}}sSchemeExps;
• (list 'if X Y Z) where X, Y, and Z are {{bool-SchemeExp}}sSchemeExps.

The provided functions parse and unparse have the following signatures.

parse: bool-SchemeExp -> boolExp
unparse: boolExp -> bool-SchemeExp

Given a parsed input of type boolExp , the simplification process consists of following four phases:

• Conversion to if form implemented by the function convert-to-if .
• Normalization implemented by the function normalize .
• Symbolic evaluation implemented by the function eval .
• Conversion back to conventional boolean form implemented by the function convert-to-bool .

A description of each of these phases follows. The reduce function has type bool-SchemeExp -> bool-SchemeExp .

Conversion to if form

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

The course staff is also providing a very simple test file for the eval and reduce functions and a file containing a sequence of raw input formulas (to be parsed by parse function in parse.ss). A good solution to this problem will include much more comprehensive test data for all functions, including some much larger test cases for reduce. The normalize function is difficult to test on large data because the printed output for some important normalized trees (represented as DAGs (Directed Acyclic Graphs) in memory) is so large.

Given a parsed input of type boolExp , the simplification process consists of following four phases:

• Conversion to if form implemented by the function convert-to-if.
• Normalization implemented by the function normalize.
• Symbolic evaluation implemented by the function eval.
• Conversion back to conventional boolean form implemented by the function convert-to-bool.

A description of each of these phases follows. The reduce function has type bool-SchemeExp -> bool-SchemeExp.

Conversion to if form

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

(make-Not  X)   

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

The conversion process always terminates (since each rewrite strictly 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.

(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 excluding {{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 if, reduce the component expressions first and then applying the matching reduction 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).

...

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

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

A boolExp is either:

...

   (make-If 'x (make-If 'y false  true) true))

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

...

.

The provided function parse: input -> boolExp takes a Scheme expression and returns the corresponding boolExp.

...

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

Wiki MarkupThe 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}} {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 }.

...

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

• convert-to-if (10%)
• normalize (20%)
• eval (20%)
• convert-to-bool (10%)
• reduce (40%)