Date: Thu, 28 Mar 2024 20:47:17 -0500 (CDT) Message-ID: <1451195388.1075.1711676837760@wiki-n2.rice.edu> Subject: Exported From Confluence MIME-Version: 1.0 Content-Type: multipart/related; boundary="----=_Part_1074_524469359.1711676837759" ------=_Part_1074_524469359.1711676837759 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Content-Location: file:///C:/exported.html
Due: Wednesday, Mar. 9, 2011
Extra Credit (100 pts.)
Write a Scheme function reduce
that reduces boolean express=
ions (represented in Scheme notation) to simplified form. For the purposes =
of this assignment, boolean expressions are Scheme expressions constructed =
from:
true
and false
;true
,=
false
, not
, and
, or
, <=
code>implies, and if
) that can be bound to either true
or false
.not
.and
, or
, and impli=
es
, andif
.The course staff is providing functions parse
and unp=
arse
in the file parse.ss\ that convert boolean ex=
pressions in Scheme notation to a simple inductively defined type called parse
and read: -> SchemeExp
is a proced=
ure of no arguments that reads a Scheme expression from the console. DrSche=
me pops up an input box to serve as the console when (read)
is=
executed.
These parsing functions rely on the following Scheme data definitions. G= iven
(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 boolExp
is either:
true
and false
;S
representing a boolean variable;(make-Not X)
where X
is a boolExp
;(make-And X Y) where X
and Y
are boolEx=
ps
;(make-Or X Y) where X
and Y
are boolExp=
s
;(make-Implies X Y)
where X
and Y
=
are boolExps
; or(make-If X Y Z)
where X
, Y
, an=
d Z
are boolExps
.A bool-SchemeExp is either:
true
or false
;S
;(list 'not X)
where X
is a bool-SchemeE=
xp
;(list op X Y)
where op
is 'and
,=
'or
, or 'implies
where X
and Y
are bool-SchemeExps
;(list 'if X Y Z)
where X
, Y
, and=
Z
are bool-SchemeExps
.The provided functions parse
and unparse
have =
the following signatures.
parse: = bool-SchemeExp -> boolExp unparse: boolExp -> bool-SchemeExp
The course staff is also providing a very simple test file\ for the eva=
l
and reduce
functions and a file\ containing a sequence of raw in=
put formulas (to be parsed by parse
function in =
parse.ss\). A good solution to this problem will include much more comp=
rehensive test data for all functions, including some much larger test case=
s for reduce
. The normalize
function is difficult=
to test on large data because the printed output for some important normal=
ized trees (represented as DAGs (Directed Acyclic Graphs) in memory) is so =
large.
Given a parsed input of type boolExp
, the simplification p=
rocess consists of following four phases:
if
form implemented by the function co=
nvert-to-if
.normalize
.eval
.boolean
form implemented b=
y the function convert-to-bool
.A description of each of these phases follows. The reduce
f=
unction has type bool-SchemeExp -> bool-SchemeExp
.
if
f=
ormA boolean expression (boolExp
) can be converted to if=
form by repeatedly applying the following rewrite rules in any orde=
r until no rule is applicable.
(make-N= ot X) =09=3D>=09(make-If X false true) (make-And X Y)=09=3D>=09(make-If X Y false) (make-Or X Y)=09=09=3D>=09(make-If X true Y) (make-Implies X Y)=09=3D>=09(make-If X Y true)
In these rules, X
and Y
denote arbitrary boolExps}. The conversion process always terminates (since each rewrite st=
rictly 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 t=
he logicians (Alonzo Church and Barkley Rosser) who invented the concept.=
p>
Since the reduction rules for this phase are Church-Rosser, you can writ=
e the function convert-to-if
using simple structural recursion=
. For each of the boolean operators And
, Or
, Implies
, and if
, reduce the compone=
nt expressions first and then applying the matching reduction (except for <=
code>if for which there is no top-level reduction).
The following examples illustrate the conversion process:
(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 tem=
plate for type boolExp
and converting all structures (other th=
an if
) to the corresponding if
structures.
Write an inductive data definition and template for boolean formulas in =
if
form, naming this type ifExp
. (Note: mak=
e-If
is the only constructor, other than variables and constants, fo=
r ifExp
.
The provided function parse: input -> boolExp
takes a Sc=
heme expression and returns the corresponding boolExp
.
An ifExp
is normalized iff every sub-expression in=
test
position is either a variable (symbol) or a constant (false
). We call this type norm-ifExp<=
/code> .
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 (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
construct=
ions. We perform this transformation by repeatedly applying the following r=
ewrite rule (to any portion of the expression) until it is inapplicable:
(make-I= f (make-If X Y Z) U V) =3D>=09 (make-If X (make-If Y U V) (m= ake-If Z U V)).
This transformation always terminates and yields a unique answer indepen= dent of the order in which rewrites are performed. The proof of this fact i= s left as an optional exercise.
In the normalize
function, it is critically important not t=
o duplicate any work, so the order in which reductions are made really matt=
ers. Do NOT apply the normalization rule above unless V
are already normalized, because the rule dupl=
icates both U
and V
. If you reduce the cons=
equent
and the alternative
(U
and V<=
/code> in the left hand side of the rule above) before reducing the
t=
est
, normalize
runs in linear time (in the number of no=
des in the input); if done in the wrong order it runs in exponential time i=
n 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-i=
fExps
X
, Y
, and Z
and constru=
cts a norm-ifExp
equivalent to (makeIf X Y Z)
. Th=
is help function processes X
because the test
pos=
ition must be a variable or a constant, yet X
can be an arbitr=
ary norm-ifExp
. In contrast, (head-normalize X Y Z) never even inspects
Y
and Z
because they are a=
lready normalized and the normalizing transformations performed in he=
ad-normalize
never place these expressions in test
posi=
tion.
The following examples illustrate how the normalize
and
(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-I= f 'y 'u 'v) (make-If 'z 'u 'v))) (check-expect (head-normalize (make-If 'x (make-If 'yt 'yc 'ya) (make-If 'z= t '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 (m= ake-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 l= arger than the internal representation (because the internal representation= can share subtrees).
Before you start writing normalize
, write the template corr=
esponding to the inductive data definition of norm-ifExp
.
The symbolic evaluation process, implemented by the function eval:=
norm-if-form environment -> norm-if-form
, reduces a norm-i=
f-form
to simple form. In particular, it reduces all tautologies (ex=
pressions 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-I= f true X Y)=09 =3D>=09X (make-If false X Y)=09 =3D>=09Y (make-If X true false) =3D>=09X (make-If X Y Y) =09 =3D>=09Y (make-If X Y Z)=09 =3D>=09(make-If X Y\[X <\- true\] Z\[X <= ;\- false\])
The notation M[X <- N]
means M
with all occ=
urrences of the symbol X
replaced by the expression N. It is very costly to actually perform these subtitutions on =3Dnorm-i=
f-form=3D data. To avoid this computational expense, we simply maintain a l=
ist of bindings which are pairs consisting of symbols (variable names) and =
boolean values {
true
, false
. The following data d=
efinition 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 l=
ooks 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 appli= ed can affect the result in some cases. However, the rewrite rules do have = the Church-Rosser property on expressions which are tautologies or contradi= ctions.
If the final rule is applied only when X
actually occurs in=
either Y
or Z
, then the symbolic evaluation proc=
ess 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 unt= il 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-expres= sion.
The final phase converts an expression in (not necessarily reduced or no=
rmalized) If
form to an equivalent expression constructed from=
variables and { true
, false
, And
, <=
code>Or, Not
, Implies
, If
. Th=
is process eliminates every expression of the form
(make-I= f 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
(make-I= f X false true) =3D> (make-Not X) (make-If X Y false) =3D> (make-And X Y) (make-If X true Y) =3D> (make-Or X Y) (make-If X Y true) =3D> (make-Implies X Y)
where X
, Y
, and Z
are arbitrary=
If
forms. This set of rules is Church-Rosser, so the rules ca=
n safely be applied using simple structural recursion.