...
| 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=
|
...
| Code Block |
|---|
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 |
|---|
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):
|
| Wiki Markup |
|---|
\(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 Block |
|---|
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 =(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. <p> 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. <p> 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 |
|---|
where one of the arguments {=X=, =Y=, =Z=} is a constant
{ =true=, =false=}.
Use the following set of reduction rules to perform this conversion
|
...