...
Homework
...
6:
...
Symbolic
...
Evaluation
...
of
...
Boolean
...
Expressions
...
Due:
...
Friday,
...
Feburary
...
26,
...
2010
...
Extra Credit
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 boolean constants
true
andfalse
; - boolean variables (represented by symbols other than
true
,false
,not
,and
,or
,implies
, andif
) that can be bound to eithertrue
orfalse
. - the unary operator
not
. - the binary operators
and
,or
, andimplies
, and - the ternary operator
if
.
The course staff is providing function 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
Code Block |
---|
Credit* h1. 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 boolean constants {{true}} and {{false}} ; * boolean variables (represented by symbols other than {{true}}, {{false}}, {{not}}, {{and}}, {{or}}, {{implies}}, and {{if}}) that can be bound to either {{true}} or {{false}}. * the unary operator {{not}} . * the binary operators {{and}}, {{or}}, and {{implies}}, and * the ternary operator {{if}}. The course staff is providing function {{parse}} and {{unparse}} in the file [parse.ss|^parse.ss.txt] 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} (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)) {code} a {{boolExp}} is either: * a boolean constant {{true}} and {{false}} ; * a symbol {{S}} representing a boolean variable; * {{ |
a boolExp
is either:
- a boolean constant
true
andfalse
; - a symbol
S
representing a boolean variable; (make-Not
...
X)
...
- where
...
X
...
- is
...
- a
...
boolExp
...
- ;
(make-And
...
X
...
Y)
...
where
...
X
...
- and
...
Y
...
- are
...
boolExps
...
- ;
(make-Or
...
X
...
Y)
...
where
...
X
...
- and
...
Y
...
- are
...
boolExps
...
- ;
(make-Implies
...
X
...
Y)
...
- where
...
X
...
- and
...
Y
...
- are
...
boolExps
...
- ;
...
- or
...
(make-If
...
X
...
Y
...
Z)
...
- where
...
X
...
- ,
...
Y
...
- ,
...
- and
...
Z
...
- are
...
boolExps
...
- .
...
A
...
bool-SchemeExp
...
is
...
either:
...
- 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}}s;
...
(list 'if
...
X
...
Y
...
Z)
...
- where
...
X
...
- ,
...
Y
...
- ,
...
- and
...
Z
...
- are
...
- {{bool
...
- -SchemeExp}}s.
...
The
...
provided
...
functions
...
parse
...
and
...
unparse
...
have
...
the
...
following
...
signatures.
Code Block |
---|
} parse: bool-SchemeExp -> boolExp unparse: boolExp -> bool-SchemeExp {code} |
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 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 can be converted to if
form by repeatedlyapplying the following rewrite rules in any order until no rule is applicable.
Code Block |
---|
}} . * 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}} . h1. 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. {code} (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) {code} |
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 |
---|
} (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)) {code} |
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:
...
- a boolean value
true
andfalse
; - a symbol
s
representing a boolean variable; (make-Not
...
M)
...
- where
...
M
...
- is
...
- a
...
boolExp
...
- ;
(make-And
...
M
...
N)
...
- where
...
M
...
- and
N
areboolExps
; (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)
whereM
,N
, andP
areboolExps
.
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 |
---|
}} where {{M}}, {{N}}, and {{P}} are {{boolExps}}. The provided function {{parse: input -> boolExp}} takes a Scheme expression and returns the corresponding {{boolExp}}. h1. 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} (make-If (make-If X Y Z) U V) => (make-If X (make-If Y U V) (make-If Z U V)). {code}. |
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))) {code} |
Once
...
a
...
large
...
formula
...
has
...
been
...
normalized,
...
do
...
not
...
try
...
to
...
...
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 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\]) {code} |
The
...
notation
...
M
...
...
...
...
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-oof 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 |
---|
----+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} (make-If X Y Z) {code} |
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)
...
YYYcodeYYY
...
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.