Homework 09: Symbolic Evaluation of Boolean Expressions in Java
Due: 10am Wednesday, March 2531, 20092010
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
andF
denoting the boolean valuestrue
andfalse
; - boolean variables (represented by symbols other than
T
,F
,!
,
&
,|
,>
, and?=)
that can be bound to either=true
orfalse
. - the unary function
!
meaningnot
. - the binary functions
&
,|
, and>
meanding
denotingand
,or
, andimplies
, respectively), and - the ternary function
?
meaningif
.
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 nputsinputs.
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 classForm
representing boolean
expresssionsexpressions; - a Java library file
Parser.java
contain a classParser
with- a
read()
method that reads a boolean expression represented in "Scheme form" and returns the corresponsing JavaForm
abstract syntax tree and - a
reduce(
commented out)
simplify()
method that composes the visitors you must write inboolSimp.dj1
to simplify reduce whatever formula theParser
instance contains to simplified form.
- a
- a Java "stub" test file
boolSimpTest.java
that includes some rudimentary tests of the code in theboolSimp.dj1
stub file.
...
The file Parser.java
includes
two Parser constructors parseParser(File file)
and parseParser(String form)
for building parsers to parse the boolean expression (in external
text form) in the specified File
or String
, respectively. To construct a Parser
for the formula
in a file {{}} you must invoke
...
If you omit the new File(...)
construction in the argument to Parser
and use "
<}} fileName
{{><fileName>"
instead,
you will create a Parser
for the String "<
fileName
>
{}
" <fileName>"
. which is interpreted
as a simple boolean variable.
The File
input format is important because it enables us to
conveniently teat apply your simplifier on to formulas that are 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 OwlSpace 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 When using the "Save As" command, 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. file. The "Save" command always retains the file types of all files.
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 its LISP heritage) but Java does not. Hence the java
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.
...
- a boolean constant
true
andfalse
; - a symbol
S
representing a boolean variable; (make-Not X)
whereX
is aboolExp
;(make-And X Y) where =X
andY
are =boolExp=sboolExps
;(make-Or X Y) where =X
andY
are =boolExp=sboolExps
;(make-Implies X Y) where ={{X
andY
are =boolExp=sboolExps
; or(make-If X Y Z)
whereX
,Y
, andZ
are =boolExp=sboolExps
.
Note: The or
operator must be written a as
Code Block |
---|
\| |
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 functionconvert-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.
Code Block |
---|
(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:
Code Block |
---|
(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
Code Block |
---|
(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
Code Block |
---|
(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:
Code Block |
---|
(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:
Code Block |
---|
(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):
Code Block |
---|
(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 Markup |
---|
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
Code Block |
---|
(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
Code Block |
---|
(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
...
These phases are described in detail in HW6.
Hints on Writing Your Java Code
The Java abstract syntax classes include a separate composite hierarchy (called
IfForm
for representing boolean
expression as conditionals (the type ifForm
ifExp
in =boolsimp.ss
=). This representation inlcudes includes 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 (https:wikiriceedudisplayCSWIKI211hw9BoolSimpdj1)
- BoolSimpTest.java (https:wikiriceedudisplayCSWIKI211hw9BoolSimpTestjava)
- Parser.java (https:wikiriceedudisplayCSWIKI211hw9Parserjava)
- boolsimp.ss (https:wikiriceedudisplayCSWIKI211hw9boolsimpss)
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 (https:wikiriceedudisplayCSWIKI211hw9BoolSimpTestdj2)
- Parser.dj2 (https:wikiriceedudisplayCSWIKI211hw9Parserdj2)
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:
...
The visitor pattern is a straightforward but notationally involved alternative to the interpreter pattern.. You can mechanically translate interpreter pattern code to visitor pattern code. (Perhaps IDEs like Eclipse should support such transformations.) The interpreter solution to this assignment is easier to write than the visitor solution described in the preceding program description. If you are still learning Java mechanics, you are encouraged to write an interpreter solution first and translate it (if you can) to visitor form. A perfect interpreter solution will only be penalized 15% versus a perfect visitor solution. If you submit an interpreter solution, your program must conform to class signatures given in the interpreter pattern support code below (just as a visitor solution must conform to the class signatures given in the visitor pattern code below).
The interpreter version of the support code replaces the ConvertToIf
, Normalize
, HeadNormalize
, Evaluate
, and Print
visitors by methods named convertToIf
, normalize
, headNormalize
, eval
, and print
.
Support Code
Here are the links for the files:
- boolsimp.ss is the reference Scheme program.
- BoolSimp.dj1 is a stub program for a visitor solution.
- BoolSimpTest.java is a stub test file for a visitor solution.
- Parser.java is a parser file for a visitor solution.
- InterpBoolSimp.dj1 is a stub program for an interpreter solution.
- InterpBoolSimpTest.java is a stub test file for an interpreter solution.
- InterpParser.java is a parser file for an interpreter solution.
InterpParser.java
is distinct from Parser.java
because the code for the reduce
method embedded in the parser is different in the two versions.
...
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 (https:wikiriceedudisplayCSWIKI211hw9littleData1) -> "T"
- littleData2 (https:wikiriceedudisplayCSWIKI211hw9littleData2) -> "T"
- littleData3 (https:wikiriceedudisplayCSWIKI211hw9littleData3) ->
"(> h (> g (> f (> e (> d (> c (! b)))))))" - littleData4 (https:wikiriceedudisplayCSWIKI211hw9littleData4) ->
"(> h (> g (> f (> e (| d (| c (| b a)))))))" - bigData0 (https:wikiriceedudisplayCSWIKI211hw9bigData0) -> "T"
- bigData1 (https:wikiriceedudisplayCSWIKI211hw9bigData1) ->
"(> j (> i (> h (> g (> f (> e (| d (| c (| b a)))))))))"
Extra Credit
...