...
| 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, 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 }.
...
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
...
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-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 code
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.