Skip to content
Skip to breadcrumbs
Skip to header menu
Skip to action menu
Skip to quick search
Spaces
Quick Search
Help
Online Help
Keyboard Shortcuts
Feed Builder
What’s new
Available Gadgets
Log In
Comp 311 - Functional Programming
Pages
Course Offerings
2020-Fall
Copy Page
You are not logged in. Any changes you make will be marked as
anonymous
. You may want to
Log In
if you already have an account. You can also
Sign Up
for a new account.
This page is being edited by
.
image-effects
image-attributes
search
attachments
weblink
advanced
Paragraph
Paragraph
Heading 1
Heading 2
Heading 3
Heading 4
Heading 5
Heading 6
Preformatted
Quote
Bold
Italic
Underline
Colour picker
More colours
Formatting
Strikethrough
Subscript
Superscript
Monospace
Clear Formatting
Bullet list
Numbered list
Task list
Outdent
Indent
Align left
Align center
Align right
Link
Table
Insert
Insert Content
Image
Link
Attachment
Symbol
Emoticon
Wiki Markup
Horizontal rule
Task List
Insert Macro
User Mention
Info
JIRA Issue
Status
Gallery
Table of Contents
Other Macros
Page Layout
No Layout
Two column (simple)
Two column (simple, left sidebar)
Two column (simple, right sidebar)
Three column (simple)
Two column
Two column (left sidebar)
Two column (right sidebar)
Three column
Three column (left and right sidebars)
Undo
Redo
Find/Replace
Keyboard Shortcuts Help
Hide the toolbars
Launch editor full screen
<h1>Homework 5: Symbolic Evaluation of Boolean Expressions</h1><p><strong>Due:</strong> Wednesday, Oct 14, 2020 at 11:59PM</p><p><strong>200 pts.</strong></p><h1>Overview</h1><p>Write a Racket function <code>reduce</code> that reduces boolean expressions (represented in Racket notation) to simplified form. For the purposes of this assignment, boolean expressions are Racket expressions constructed from:</p><ul><li>the boolean constants <code>true</code> and <code>false</code> ;</li><li>boolean variables (represented by symbols other than <code>true</code>, <code>false</code>, <code>not</code>, <code>and</code>, <code>or</code>, <code>implies</code>, and <code>if</code>) that can be bound to either <code>true</code> or <code>false</code>.</li><li>the unary operator <code>not</code> .</li><li>the binary operators <code>and</code>, <code>or</code>, and <code>implies</code>, and</li><li>the ternary operator <code>if</code>.</li></ul><p>The course staff is providing functions <code>parse</code> and <code>unparse</code> in the file <code><a class="confluence-link unresolved" data-filename="parse.ss.txt" data-linked-resource-default-alias="parse.ss.txt" href="#">parse.</a>rkt</code> that convert boolean expressions in Racket notation to a simple inductively defined type called B<code>oolExp</code> and vice-versa. The coding of <code>parse</code> and <code>unparse</code> 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 <code>read: -> RacketExp</code> 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 <code>(read)</code> is executed.</p><p>These parsing functions rely on the following Racket data definitions. Given</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>(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)) </pre></td></tr></table><p>a <code>BoolExp</code> is either:</p><ul><li>a boolean constant <code>true</code> and <code>false</code> ;</li><li>a symbol <code>S</code> representing a boolean variable;</li><li><code>(make-Not X)</code> where <code>X</code> is a <code>BoolExp</code>;</li><li><code>(make-And X Y) where X</code> and <code>Y</code> are <code>BoolExp</code>s;</li><li><code>(make-Or X Y) where X</code> and <code>Y</code> are <code>BoolExp</code>s;</li><li><code>(make-Implies X Y)</code> where <code>X</code> and <code>Y</code> are <code>BoolExp</code>s; or</li><li><code>(make-If X Y Z)</code> where <code>X</code> , <code>Y</code> , and <code>Z</code> are <code>BoolExp</code>s.</li></ul><p>A BoolRacketExp is either:</p><ul><li>a boolean constant <code>true</code> or <code>false</code>;</li><li>a symbol <code>S</code>;</li><li><code>(list 'not X)</code> where <code>X</code> is a <code>BoolRacketExp</code> ;</li><li><code>(list op X Y)</code> where <code>op</code> is <code>'and</code> , <code>'or</code> , or <code>'implies</code> where <code>X</code> and <code>Y</code> are <code>BoolRacketExp</code>s;</li><li><code>(list 'if X Y Z)</code> where <code>X</code>, <code>Y</code>, and <code>Z</code> are <code>BoolRacketExp</code>s.</li></ul><p>The provided functions <code>parse</code> and <code>unparse</code> have the following signatures.</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>parse: BoolRacketExp -> BoolExp unparse: BoolExp -> BoolRacketExp </pre></td></tr></table><p>The course staff is also providing a very simple <a class="confluence-link unresolved" data-filename="evalData" data-linked-resource-default-alias="evalData" href="#">test file\</a> for the <code>eval</code> and <code>reduce</code> functions and a <a class="confluence-link unresolved" data-filename="input" data-linked-resource-default-alias="input" href="#">file\</a> containing a sequence of raw input formulas (to be parsed by <code>parse</code> function in <a class="confluence-link unresolved" data-filename="parse.ss.txt" data-linked-resource-default-alias="parse.ss.txt" href="#">parse.ss\</a>). A good solution to this problem will include much more comprehensive test data for all functions, including some much larger test cases for <code>reduce</code>. The <code>normalize</code> 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.</p><p>Given a parsed input of type <code>BoolExp</code> , the simplification process consists of following four phases:</p><ul><li>Conversion to I<code>f</code> form implemented by the function <code>convertToIf</code>.</li><li>Normalization implemented by the function <code>normalize</code>.</li><li>Symbolic evaluation implemented by the function <code>eval</code>.</li><li>Conversion back to conventional <code>boolean</code> form implemented by the function <code>convertToBool</code>.</li></ul><p>A description of each of these phases follows. The <code>reduce</code> function has type <code>BoolRacketExp -> BoolRacketExp</code>.</p><h1>Conversion to <code>if</code> form</h1><p>A boolean expression (<code>BoolExp</code>) can be converted to <code>if</code> form (a boolean expression where the only constructor is <code>make-If</code>) by repeatedly applying the following rewrite rules in any order until no rule is applicable.</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>(make-Not X) => (make-If X false true) (make-And X Y) => (make-If X Y false) (make-Or X Y) => (make-If X true Y) (make-Implies X Y) => (make-If X Y true) </pre></td></tr></table><p>In these rules, <code>X</code> and <code>Y</code> denote arbitrary <code>BoolExp</code>s<code>}. </code>The conversion process always terminates (since each rewrite strictly reduces the number of logical connectives excluding<code> make-If</code> 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.</p><p>Since the reduction rules for this phase are Church-Rosser, you can write the function <code>convertToIf</code> using simple structural recursion. For each of the boolean operators <code>And</code>, <code>Or</code>, <code>Not</code>, <code>Implies</code>, and I<code>f</code>, reduce the component expressions first and then applying the matching reduction (except for I<code>f</code> for which there is no top-level reduction).</p><p>The following examples illustrate the conversion process:</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>(check-expect (convertToIf (make-Or (make-And 'x 'y) 'z)) (make-If (make-If 'x 'y false) true 'z)) (check-expect (convertToIf (make-Implies 'x (make-Not 'y)) (make-If 'x (make-If 'y false true) true)) </pre></td></tr></table><p>We suggest simply traversing the tree using the structural recursion template for type <code>BoolExp</code> and converting all structures (other than <code>If</code>) to the corresponding <code>if</code> structures.</p><p>Write an inductive data definition and template for boolean formulas in <code>if</code> form, naming this type <code>ifExp</code>. (Note: <code>make-If</code> is the only constructor, other than variables and constants, for <code>ifExp</code>.</p><p>The provided function <code>parse: input -> BoolExp</code> takes a Racket expression and returns the corresponding <code>BoolExp</code>.</p><h1>Normalization</h1><p>An <code>ifExp</code> is <em>normalized</em> iff every sub-expression in <code>test</code> position is either a variable (symbol) or a constant (<code>true</code> or <code>false</code>). We call this type <code>NormIfExp</code> .</p><p>For example, the <code>ifExp</code> <code>(make-If (make-If X Y Z) U V))</code> is not a <code>NormIfExp</code> because it has an <code>If</code> construction in <code>test</code> position. In contrast, the equivalent <code>ifExp</code> <code>(make-If X (make-If Y U V) (make-If Z U V))</code> is normalized and hence is an <code>NormIfExp</code>.</p><p>The normalization process, implemented by the function <code>normalize: ifExp -> NormIfExp</code> eliminates all <code>if</code> constructions that appear in <code>test</code> positions inside <code>if</code> constructions. We perform this transformation by repeatedly applying the following rewrite rule (to any portion of the expression) until it is inapplicable:</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>(make-If (make-If X Y Z) U V) => (make-If X (make-If Y U V) (make-If Z U V)). </pre></td></tr></table><p>This transformation always terminates and yields a unique answer independent of the order in which rewrites are performed. The proof of this fact is left as an optional exercise.</p><p>In the <code>normalize</code> function, it is critically important not to duplicate any work, so the order in which reductions are made really matters. Do <strong>NOT</strong> apply the normalization rule above unless <code>U</code> and <code>V</code> are already normalized, because the rule duplicates both <code>U</code> and <code>V</code>. If you reduce the <code>consequent</code> and the <code>alternative</code> (<code>U</code> and <code>V</code> in the left hand side of the rule above) before reducing the <code>test</code>, <code>normalize</code> runs in linear time (in the number of nodes in the input); if done in the wrong order it runs in exponential time in the worst case. (And some of our test cases will exhibit this worst case behavior.)</p><p>Hint: define a sub-function head-normalize that takes three <code>NormIfExps</code> <code>X</code>, <code>Y</code>, and <code>Z</code> and constructs a <code>NormIfExp</code> equivalent to <code>(makeIf X Y Z)</code>. This help function processes <code>X</code> because the <code>test</code> position must be a variable or a constant, yet <code>X</code> can be an arbitrary <code>NormIfExp</code>. In contrast, <code>(head-normalize X Y Z)</code> never even inspects <code>Y</code> and <code>Z</code> because they are already normalized and the normalizing transformations performed in <code>head-normalize</code> never place these expressions in <code>test</code> position.</p><p>The following examples illustrate how the <code>normalize</code> and <code>head-normalize</code> functions behave:</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>(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-If 'y 'u 'v) (make-If 'z 'u 'v))) (check-expect (head-normalize (make-If 'x (make-If 'yt 'yc 'ya) (make-If 'zt '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 (make-If 'y 'u 'v) (make-If 'z 'u 'v))) </pre></td></tr></table><p>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).</p><p>Before you start writing <code>normalize</code>, write the template corresponding to the inductive data definition of <code>NormIfExp</code>.</p><h1>Symbolic Evaluation</h1><p>The symbolic evaluation process, implemented by the function <code>eval: NormIfExp environment -> NormIfExp</code>, reduces a <code>NormIfExp</code> to simple form. In particular, it reduces all tautologies (expressions that are always true) to <code>true</code> and all contradictions (expressions that are always false) to <code>false</code>.</p><p>Symbolic evaluation applies the following rewrite rules to an expression until none is applicable (with one exception discussed below):</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>(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]) </pre></td></tr></table><p>The notation <code>M[X <- N]</code> means <code>M</code> with all occurrences of the symbol <code>X</code> replaced by the expression <code>N</code>. It is very costly to actually perform these substitutions on <code>NormIfExp</code> data. To avoid this computational expense, we simply maintain a list of bindings which are pairs consisting of symbols (variable names) and boolean values {<code>true</code>, <code>false</code>. The following data definition definition formally defines the <code>binding</code> type.</p><p>A <code>binding</code> is a pair <code>(make-binding s v)</code> where s is a symbol (a variable) and <code>v</code> is a boolean value (an element of { <code>true</code>, <code>false</code> }.</p><p>An <code>environment</code> is a <code>binding-list</code>.</p><p>When the <code>eval</code> 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><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><p>If the final rule is applied only when <code>X</code> actually occurs in either <code>Y</code> or <code>Z</code>, 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.</p><p>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 subexpression.</p><h1>Conversion to Boolean Form</h1><p>The final phase converts an expression in (not necessarily reduced or normalized) <code>If</code> form to an equivalent expression constructed from variables and { <code>true</code>, <code>false</code>, <code>And</code>, <code>Or</code>, <code>Not</code>, <code>Implies</code>, <code>If</code>. This process eliminates every expression of the form</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>(make-If X Y Z) </pre></td></tr></table><p>where one of the arguments {<code>X</code>, <code>Y</code>, <code>Z</code> is a constant { <code>true</code>, <code>false</code> }.</p><p>Use the following set of reduction rules to perform this conversion</p><table class="wysiwyg-macro" data-macro-name="code" style="background-image: url(/confluence/plugins/servlet/confluence/placeholder/macro-heading?definition=e2NvZGV9&locale=en_GB&version=2); background-repeat: no-repeat;" data-macro-body-type="PLAIN_TEXT"><tr><td class="wysiwyg-macro-body"><pre>(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) </pre></td></tr></table><p>where <code>X</code> , <code>Y</code> , and <code>Z</code> are arbitrary <code>If</code> forms. This set of rules is Church-Rosser, so the rules can safely be applied using simple structural recursion.</p><h1>Points Dsitribution</h1><ul><li>convertToIf (10%)</li><li>normalize (20%)</li><li>eval (20%)</li><li>convertToBool (10%)</li><li>reduce (40%)</li></ul>
If you are unable to use this CAPTCHA please
contact your administrator
for assistance.
Attachments
Labels
Location
Edit
Preview
Save
Cancel
Next hint