...

The course staff is providing functions `parse`

and `unparse`

in the file `parse.`

rkt that `rkt`

that convert boolean expressions in Racket notation to a simple inductively defined type called B`oolExp`

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 Racket primitive `read: -> RacketExp`

is a procedure of no arguments that reads a Racket expression from the console. DrRacket pops up an input box to serve as the console when `(read)`

is executed.

...

- a boolean constant
`true`

and`false`

; - 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`

`BoolExp`

s;`(make-Or X Y) where X`

and`Y`

are`BoolExps`

`BoolExp`

s;`(make-Implies X Y)`

where`X`

and`Y`

are`BoolExps`

`BoolExp`

s; or`(make-If X Y Z)`

where`X`

,`Y`

, and`Z`

are`BoolExps`

`BoolExp`

s.

A bool-RacketExp BoolRacketExp is either:

- a boolean constant
`true`

or`false`

; - a symbol
`S`

; `(list 'not X)`

where`X`

is a`bool-RacketExp`

`BoolRacketExp`

;`(list op X Y)`

where`op`

is`'and`

,`'or`

, or`'implies`

where`X`

and`Y`

are`bool-RacketExps`

`BoolRacketExp`

s;`(list 'if X Y Z)`

where`X`

,`Y`

, and`Z`

are`bool-RacketExps`

`BoolRacketExp`

s.

The provided functions `parse`

and `unparse`

have the following signatures.

Code Block |
---|

parse: bool-RacketExpBoolRacketExp -> BoolExp unparse: BoolExp -> bool-RacketExpBoolRacketExp |

The course staff is also providing a very simple test file\ for the `eval`

and `reduce`

functions and a file\ containing a sequence of raw input formulas (to be parsed by `parse`

function in parse.ss\). A good solution to this problem will include much more comprehensive test data for all functions, including some much larger test cases for `reduce`

. The `normalize`

function is difficult to test on large data because the printed output for some important normalized trees (represented as DAGs (Directed Acyclic Graphs) in memory) is so large.

Given a parsed input of type `BoolExp`

, the simplification process consists of following four phases:

- Conversion to
`if`

I`f`

form implemented by the function`convert-to-if`

`convertToIf`

. - 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`

`convertToBool`

.

A description of each of these phases follows. The `reduce`

function has type `boolBoolRacketExp -RacketExp -> bool-RacketExpBoolRacketExp`

.

# Conversion to `if`

form

A boolean expression (`BoolExp`

) can be converted to `if`

form (a boolean expression where the only constructor is `make-If`

) by repeatedly applying the following rewrite rules in any order until no rule is applicable.

...

In these rules, `X`

and `Y`

denote arbitrary `BoolExpsBoolExp`

s`}. `

The conversion process always terminates (since each rewrite strictly reduces the number of logical connectives excluding` {{make make-If`

) and 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 `convertToIf`

using simple structural recursion. For each of the boolean operators `And`

, `Or`

, `Not`

, `Implies`

, and `if`

I`f`

, reduce the component expressions first and then applying the matching reduction (except for `if`

I`f`

for which there is no top-level reduction).

...

Code Block |
---|

(check-expect (convert-to-ifConverToIf (make-Or (make-And 'x 'y) 'z)) (make-If (make-If 'x 'y false) true 'z)) (check-expect (convert-to-ifConverToIf (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 template for type `BoolExp`

and converting all structures (other than `if`

`If`

) 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 is the only constructor, other than variables and constants, for `ifExp`

.

The provided function `parse: input -> boolExpBoolExp`

takes a Racket expression and returns the corresponding `boolExp`

`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`

.

...

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 ConverToIf (10%)
- normalize (20%)
- eval (20%)
- convert-to-bool (10%)
- reduce (40%)