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 foo 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
Code Block |
---|
(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
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
.
A bool-SchemeExp is either:
- a boolean constant
true
orfalse
; - a symbol
S
; (list 'not X)
whereX
is abool-SchemeExp
;(list op X Y)
whereop
is'and
,'or
, or'implies
whereX
andY
are {{bool-
SchemeExp}}sSchemeExps
;(list 'if X Y Z)
whereX
,Y
, andZ
are {{bool-
SchemeExp}}sSchemeExps
.
The provided functions parse
and unparse
have the following signatures.
Code Block |
---|
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 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. The reduce
function has type bool-SchemeExp -> bool-SchemeExp
.
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.
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 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 functionconvert-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.
Code Block |
---|
(make-Not X) |
Code Block |
(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 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.
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 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 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).
The following examples illustrate the conversion process:
Code Block |
---|
(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
Code Block |
---|
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=
|
the conversion process:
Code Block |
---|
(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
) 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
.
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
...
test
positions inside 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. Do NOT apply the normalization rule above unless U
and V
are already normalized, because the rule duplicates both U
and V
. If you reduce the consequent
and the alternative
(U
and V
in the left hand side of the rule above) before reducing the test
, normalize
runs in linear time (in the number of nodes in the input); if done in the wrong order it runs in exponential time in the worst case. (And some of our test cases will exhibit this worst case behavior.)
Hint: define a sub-function head-normalize that takes three norm-ifExps
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, do not try to print it unless you know that the formula is small! The printed form can be exponentially larger than the internal representation (because the internal representation can share subtrees).
Before you start writing normalize
, write the template corresponding to the inductive data definition of norm-ifExp
.
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 (make-If X Y Z) U V) => (make-If X (make-If Y U V) (make-If Z U V)).
Code Block |
---|
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. Do *NOT* apply
the normalization rule above unless =U= and =V= are already
normalized, because the rule duplicates both =U= and =V=. If you
reduce the _consequent_ and the _alternative_ (=U= and =V= in the left
hand side of the rule above) before reducing the _test_, =normalize=
runs in linear time (in the number of nodes in the input); if done in
the wrong order it runs in exponential time in the worst case. (And
some of our test cases will exhibit this worst case behavior.)
Hint: define a sub-function head-normalize that takes 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)))
Code Block |
---|
Once a large formula has been normalized, do not try to print it unless you know that the formula is small!
The printed form can be exponentially larger than the internal representation (because the internal representation can share subtrees).
Before you start writing =normalize=, write the template corresponding to the inductive data definition of =norm-ifExp=.
----+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=.
<p>
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,
...
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
...
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
...
(list-of 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.
...
We
...
recommend
...
applying
...
the
...
rules
...
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 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
}.
Use 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)
|
(make-If X Y Z)
Code Block |
---|
where one of the arguments {=X=, =Y=, =Z=} is a constant
{ =true=, =false=}.
Use the following set of reduction rules to perform this conversion
|
...
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%)