Homework 09: Symbolic Evaluation of Boolean Expressions in Java

Due: Wednesday, March 25, 2009

Overview

Write a Java program boolSimp.dj1 that reduces boolean expressions (represented in the input and output streams in Scheme-like notation) to simplified form. For the purposes of this assignment, boolean expressions are Scheme expressions constructed from:

• the symbols T and F denoting the boolean values true and false;
• boolean variables (represented by symbols other than T, F, !, &, |, >, and ?) that can be bound to either true or false.
• the unary function ! meaning not.
• the binary functions &, |, and > meanding and, or, and implies, respectively), and
• the ternary function ? meaning if.

The shorter names T, F, !, &, |, >, and ? are used instead of true, false, not, and, or, implies, and if) for notational brevity which matters in very large nputs.

The course staff is providing:

• a Scheme program in the file boolsimp.ss equivalent to the Java program that you are required to write;
• a Java "stub" file boolSimp.dj1 that defines a composite hierarchy

of "abstract syntax" tree classes rooted in the class Form representing boolean expresssions;

• a Java library file Parser.java contain a class Parser with
  • a read() method that reads a boolean expression represented in "Scheme form" and returns the corresponsing Java Form abstract syntax tree and
  • a (commented out) simplify() method that composes the visitors you must write in boolSimp.dj1 to simplify whatever formula the Parser instance contains.
• a Java "stub" test file boolSimpTest.java that includes some rudimentary tests of the code in the boolSimp.dj1 stub file.

The stub file BoolSimp.dj1 also includes comments showing you exactly what code you have to write to complete writing your simplifier. Of course, you also need to write corresponding tests and add them to the file BoolSimpTest.java.

The file Parser.java includes two Parser constructors parse(File file) and parse(String form) for building parsers to parse the boolean expression (in external form) in the specified File or String, respectively. To construct a Parser for the formula in a file you must invoke

new Parser(new File("<fileName>"));

If you omit the new File(...) construction in the argument to Parser and use "< fileName >" instead, you will create a Parser for the String "< fileName >" which is interpreted as a simple boolean variable.

The File input format is important because it enables us to conveniently teat your simplifier on formulas thousands of symbols long).

As a result, you only have to translate the Scheme code in boolsimp.ss into corresponding cleanly-written OO Java code by filling in the gaps in our Java stub file boolSimp.dj1. You are expected to appropriately use the composite, interpreter, singleton, and visitor patterns in the code that you write. Since the only stub files that you have to modify are boolSimp.dj1 and boolSimpTest.java, simply submit expanded versions of these files via OwlNet^? to submit your assignment. Warning: we will run your program on large inputs to determine if you wrote the code correctly. Try using the large test files provided on the course wiki.

We have formatted the test files as a .java file rather than a .dj1 because the Language Levels facility peforms no useful augmentation of JUnit test classes and bypassing the language levels translator avoids some annoying bugs in the implementation of that facility. Please remember to save you file boolSimpTest.java as a .java file not as a .dj1 file.

Correction: we now recommend using Advanced Level (.dj2) files instead of Full Java (.java) files in mixed compilation with Intermediate Level files. You should be able to consistently use .dj2 files instead of .java files if you download the latest version of DrJava from www.cs.rice.edu/~javaplt/drjavarice. See the Addendum below.

The Scheme file boolsimp.ss includes Scheme functions parse and unparse to translate Scheme lists into abstract syntax trees and vice-versa. Scheme provides a simple external syntax for lists (in homage to is LISP heritage) but Java does not. Hence the java Parser class works on Java strings instead of lists. The Java visitor class Print in the BoolSimp.java file performs unparsing of the abstract syntax types Form and IfForm to type String.

The Scheme parsing functions rely on the following Scheme data definitions.

Given

(define-struct ! (arg))
(define-struct & (left right))
(define-struct \| (left right))
(define-struct > (left right))
(define-struct ? (test conseq alt))

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

Note: The or operator must be written a \| in Scheme instead of | because | is a metasymbol with a special meaning in Scheme (akin to ').

Description of the Provided Scheme program

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.

Conversion to if form

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

(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)
(make-Not  X)      =>   (make-If  X  false true)

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.

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:

(convert-to-if (make-Or  (make-And  'x  'y)  'z))  =>  (make-If  (make-If  'x  'y  false)  true  'z)
(convert-to-if (make-Implies  'x  (make-Not  'y) )  =>  (make-If  'x  (make-If  'y  false  true)  true)

The Scheme conversion function convert-to-if traverses the tree using the structural recursion template for type boolExp, converting all structures (other than if forms) to the corresponding if structures.

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

(make-If (make-If X Y Z) U V))

is not a norm-ifExp 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.

The normalization process, implemented by the function normalize: ifExp -> norm-ifExp eliminates all if constructions that appear in the test position of other if constructions. We perform this transformation by repeatedly applying the following rewrite rule (to any portion of the expression) until it is inapplicable:

(make-If  (make-If  X  Y  Z)  U  V)  =>    (make-If  X  (make-If  Y  U  V) (make-If Z  U  V)).

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. The rule is ONLY applied when U and V are already normalized, because the rule duplicates both U and V. Reducing the consequent and the alternative (U and V in the left hand side of the rule above) before reducing the test, is catastrophic. It degrades the worst case running time of normalize from linear time (in the number of nodes in the input) to exponential time. (And some of our test cases will exhibit this worst case behavior.)

The Scheme simplifier define a help function head-normalize that takes the three norm-ifExp=s =X, Y, and 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:

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

Once a large formula has been normalized, the Scheme simplifier does not print it! The printed form can be exponentially larger than the internal representation (because the internal representation can share subtrees).

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.

Symbolic evaluation applies the following rewrite rules to an expression until none is applicable (with one exception discussed below):

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

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, the Scheme simplifier maintains a list of variable 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 (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.

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.

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.

The rules are applied 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 normalized or 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

 (make-If X Y Z)

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

This phase uses the following set of reduction rules to perform this conversion

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

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.

Hints on Writing Your Java Code

You may need to compile your files individually to work around a Language Levels bug. The command to compile the current file (document) is located on the Tools menu.

The Java abstract syntax classes include a separate composite hierarchy (called IfForm for representing boolean expression as conditionals (the type ifForm in boolsimp.ss). This representation inlcudes only three concrete variant classes, making it much easier to write the visitors that perform normalization, evaluation, and clean-up.

Support Code

Here are the links for the files:

• BoolSimp.dj1
• BoolSimpTest.java
• Parser.java
• boolsimp.ss

Addendum Concerning Language Levels

A careful reading the Language Levels code base reveals that the code base does not support intermixing the compilation of language levels files (.dj0, .dj1, .dj2) and full Java (.java) files. In some cases, intermixed compilation happens to work, but I no longer recommend trying it.

Although intermixed compilation is certainly a desirable goal and may be added to DrJava at a future date, the Advanced Language Level (.dj2) of DrJava is reasonably close to full Java, so we can use .dj2 files instead of .java files when performing intermixed compilation. The Advanced Language Level does not perform any code augmentation; it merely prohibits some more advanced language features such as synchronization and threads and ostensibly provides better syntax diagnositcs.

I have attached the .dj2 equivalents of BoolSimpTest.java and Parser.java. To my knowledge, the Advanced Language Level has not been used by students in a course prior our usage, so we may encounter a few bugs.

Here are the links for the new .dj2 files:

• BoolSimpTest.dj2
• Parser.dj2

Further Addendum

I have cleaned up BoolSimp.dj1 and BoolSimpTest.dj2 slightly, changing parameter to names in visitor classes to follow the convention of using host in place of this (which I did not follow when I originally wrote this code) and adding comments to explain the commented out unit tests in BoolSimpTest.dj2. I discovered that nothing in BoolSimpTest.dj2 is incompatible with the Intermediate Language Level so I have renamed the new version as BoolSimpTest.dj1. The new BoolSimp.dj1 file replaces the old one.

Here are the links for the new .dj1 files:

• BoolSimp.dj1
• BoolSimpTest.dj1

Sample Input Files

The following files contain large formulas that can be reduced by your simplifier. Only the file named bigData* require a larger thread stack size than the default on my laptop. I used the JVM argument -Xss64M for the Interactions JVM to get the bigData* files to run.

• littleData1 -> "T"
• littleData2 -> "T"
• littleData3 -> "(> h (> g (> f (> e (> d (> c (! b)))))))"
• littleData4 -> "(> h (> g (> f (> e (| d (| c (| b a)))))))"

• bigData0 -> "T"
• bigData1 -> "(> j (> i (> h (> g (> f (> e (| d (| c (| b a)))))))))"

Extra Credit

Do not attempt this section until you have a well-written solution to the preceding assignment. You can eliminate essentially all of the embedded casts in your code if you use Java generics to parameterize the visitor interface including the accept method embedded in all of the abstract syntax classes. DrJava language levels does not support generics, so you have to use full Java to do the extra credit assignment. You can start with .java files generated for your non-generic solution (written using Language Levels), but please try to clean up the generated code (condensing the formatting) which is rather space inefficient.