Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Migrated to Confluence 5.3

...

  • 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}}sSchemeExps;
  • (list 'if X Y Z) where X, Y, and Z are {{bool-SchemeExp}}sSchemeExps.

The provided functions parse and unparse have the following signatures.

...

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
(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 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 }.

...

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%)