Homework 5: Continuations

1. Revisit the definition of values in figure 2.1 on page 99. Next, study the definition of the predefined function all? in section 2.8.3, which starts on page 135. Like many higher-order functions, all? has a subtle contract: it is permissible to call (all? p? xs) if and only if there exists a set A such that following are true:
   • Parameter p? is a function that accepts one argument, which must be a member of A. Then p? returns a Boolean.
   • Parameter xs is in LIST(A). That is, xs is a list of values, and every element of xs is a member of A.
   In other words, xs must be a list of values, each of which may be passed to p?. With this contract in mind, answer these questions:
   1. Write a value that is never permissible as the second, xs argument to all?, no matter what p? is.
   2. Write a value made with cons that is never permissible as the second, xs argument to all?, no matter what p? is.
   3. Write a value that may or may not be permissible as the second, xs argument to all?, depending on what p? is. Your value should be permissible if p? is number?, but impermissible if p? is prime?.
2. Study the description of function list-of? below, and also the hints. Now, for each value of xs that you listed in the previous question, answer whether it is permissible to pass that value to list-of? along with the predicate prime?, and if so, what result list-of? should return. Assume that we're using a version of prime? that accepts any value and returns #f for non-numbers.
   1. Permissible? If so, what does list-of? return?
   2. Permissible? If so, what does list-of? return?
   3. Permissible? If so, what does list-of? return?
3. Section 2.12.3, which starts on page 159, describes the semantics of the true-definition forms. Use the semantics to answer two questions about the following sequence of definitions:

   (val f (lambda () y))
   (val y 10)
   (f)

   Given evaluating lambda in an environment ρ creates a closure using that same ρ, if the definitions above are evaluated in an environment in which y ∈ dom ρ, then what is the result of the call to f? Pick A, B, or C.
   1. It returns 10.
   2. An error is raised: Run-time error: name y not found.
   3. It returns whatever value y had before the definitions were evaluated.
   If the definitions above are evaluated in an environment in which y ∉ dom ρ, what is the result of the call to f? Pick either A or B.
   1. It returns 10.
   2. An error is raised: Run-time error: name y not found.
4. Read the definition of eval-formula below, including the definition of the environment used by eval-formula. What is the result of evaluating the following Boolean formulas in an environment where x is #t, y is #f, and z is #f? (For each formula, answer #t, “true”, #f, or “false.”)
   1. x, which in μScheme is constructed by 'x
   2. ¬x, which in μScheme is constructed by (make-not 'x)
   3. ¬y ∧ x, which in μScheme is constructed by (make-and (list2 (make-not 'y) 'x))
   4. ¬x ∨ y ∨ z, which in μScheme is constructed by (make-or (list3 (make-not 'x) 'y 'z))
   5. Formula (make-not (make-or (list1 'z))), which has a tricky make-or applied to a list of length 1, and so can’t be written using infix notation
5. Read about the Boolean-satisfaction problem for CNF formulas, in section 2.10.1, which starts on page 145. The rules for satisfaction are the same for all Boolean formulas, even those that are not in CNF.For example:
   • x‌ ∨ y ∨ z, which in μScheme is constructed by (make-or '(x y z)), is solved by '((x #t))
   • x ∧ y ∧ z, which in μScheme is constructed by (make-and '(x y z)), is solved by '((x #t) (y #t) (z #t))
   • x ∧ ¬x, which in μScheme is constructed by (make-and (list2 'x (make-not 'x))), has no solution
   For each of the following Boolean formulas, if there is an assignment to x, y, and z that satisfies the formula, write the words “is solved by” and a satisfying assignment. Incomplete assignments are OK. If there is no satisfying assignment, write the words “has no solution.”:
   1. (x ∨ ¬x) ∧ y, which in μScheme is constructed by (make-and (list2 (make-or (list2 'x (make-not 'x))) 'y))
   2. (x ∨ ¬x) ∧ ¬x, which in μScheme is constructed by (make-and (list2 (make-or (list2 'x (make-not 'x))) (make-not 'x))),
   3. (x ∨ y ∨ z) ∧ (¬x ∧ x) ∧ (x ∨ ¬y ∨ ¬z), which in μScheme is constructed by

      (make-and 
          (list3 (make-or (list3 'x 'y 'z)) 
                 (make-and (list2 (make-not 'x) 'x))
                 (make-or (list3 'x (make-not 'y) (make-not 'z))))))

Your SAT solver will represent boolean formulae the same way as in the textbook: A formula is either a symbol such as 'x, representing a variable, or a record constructed using the following definitions:

(record not [arg])
(record or  [args])
(record and [args])

• Define a function (list-of? A? v) that takes a predicate A? that can be applied to any value and an arbitrary μScheme value v, and returns a Boolean that is #t if v is a list of values, each of which satisfies A?. Otherwise, (list-of? A? v) returns #f. You must write algebraic laws. The last law may include a side condition “all other forms.” Hints:
  • The forms of data for arbitrary μScheme values can be deduced from the definition of values in Figure 2.1 on page 99. Function list-of? must correctly handle fully general S-expressions like (cons 'COMP 105).
  • Provided A? is a good predicate, (list-of? A? v) never causes a checked run-time error, no matter what v is. This property distinguishes list-of? from all?.
  • Every one of the primitive type predicates, like symbol? and procedure?, is a good predicate to pass to list-of?.
  • For testing, I encourage you to define and use the following additional predicate:

    (define value? (_) #t) ;; tell if the argument is a value

    You can then identify any list of values with (list-of? value? v).
  • Test with several different predicates. For each one, write check-assert tests with both true and false results.
  • Remember that for every A, the empty list is a list of A.
• Define a function (formula? v) that, when given an arbitrary μScheme value v, returns #t if v represents a Boolean formula and #f otherwise. Follow the above definition of formulas exactly. You must write algebraic laws. You can use a side condition like “v has none of the forms above” in the last law. Hints:
  • Function formula? must analyze every possible μScheme value, no matter what its form, and must always return #t or #f. Every possible form of μScheme value must therefore be handled by some case. (If it turns out that one case can handle multiple forms of input, that is OK. It is even good practice.)
  • Function formula? must identify, out of all possible values, which ones are formulas. Every possible form of formula must therefore be handled by a case that returns #t.
  • Just because some clown puts a list of values in a record, it doesn’t mean that the record holds a list of formulas.
  • Because formula? must analyze every possible μScheme value, it is not possible to violate its contract!
• Define a function (eval-formula f env) that takes a formula f and an environment env, where an environment is an association list in which each key is a symbol and each value is a Boolean. Function (eval-formula f env) returns #t if the formula is satisfied in env, and #f otherwise. Evaluation is defined by induction:
  • The result of evaluating a symbol is the result of looking that symbol up in the environment.
  • The result of evaluating (make-not f) is the complement of the result of evaluating f.
  • The result of evaluating (make-or fs) is true if and only if the list of formulas fs contains a formula that evaluates to true.
  • The result of evaluating (make-and fs) is true if and only if every formula in the list of formulas fs evaluates to true.
  It is part of the contract of eval-formula that (eval-formula f env) may be called only when every variable in formula f is bound in env.

  You must write algebraic laws. Your laws should cover only those inputs permitted by eval’s contract. Do not include any laws for inputs that violate the contract. (And in the code, do not include any cases for inputs that violate the contract.)

• Create three test cases for find-formula-true-asst, described below. Your test cases will be represented by six val bindings, to variables f1, s1, f2, s2, f3, and s3. Each fi should be a Boolean formula as described above, e.g., (val f1 (make-not 'x)). Each si should be an association list that represents a satisfying assignment for the corresponding fi, e.g., (val s1 '((x #f))) solves formula f1. If no satisfying assignment exists, si should be the symbol no-solution. Put your test cases into a file solver-tests.scm. In comments in your test file, explain why these particular test cases are important. Your test cases must not be too complicated to be explained, and they should be designed to find bugs in solvers. No algebraic laws are needed.
• Finally, write a function (find-formula-true-asst f fail succ) that takes a formula f and continuations fail and succ. If f is satisfiable, then (find-formula-true-asst f fail succ) calls (succ env resume) with a satisfying assignment env (an association list) and a resume continuation resume (which does not take any arguments). Otherwise, it calls (fail) with no arguments. Use the ideas of Section 2.10.1, but you won't be able to use the code directly. Instead, try using letrec to define the following mutually recursive functions:
  • Calling (find-formula-asst f bool cur fail succ) extends assignment cur to find an assignment that makes the single f equal to bool.
  • Calling (find-all-asst fs bool cur fail succ) extends cur to find an assignment that makes every formula in the list fs equal to bool.
  • Calling (find-any-asst fs bool cur fail succ) extends cur to find an assignment that makes any one of the fs equal to bool.
  • Calling (find-formula-symbol x bool cur fail succ), where x is a symbol, does one of three things:
    • If x is bound to bool in cur, succeeds with environment cur and resume continuation fail
    • If x is bound to (not bool) in cur, fails
    • If x is not bound in cur, extends cur with a binding of x to bool, then succeeds with the extended environment and resume continuation fail

  Hints: Remember De Morgan’s laws, one of which is mentioned on page 137. Formulas may be nested with one kind of operator under another. In all the functions above, bool is #t or #f. Before defining each of the functions, we recommend completing the following algebraic laws:

  (find-formula-asst x            bool cur fail succ) == ..., where x is a symbol
  (find-formula-asst (make-not f)  bool cur fail succ) == ...
  (find-formula-asst (make-or  fs) #t   cur fail succ) == ...
  (find-formula-asst (make-or  fs) #f   cur fail succ) == ...
  (find-formula-asst (make-and fs) #t   cur fail succ) == ...
  (find-formula-asst (make-and fs) #f   cur fail succ) == ...
  
  (find-all-asst '()         bool cur fail succ) == ...
  (find-all-asst (cons f fs) bool cur fail succ) == ...
  
  (find-any-asst '()         bool cur fail succ) == ...
  (find-any-asst (cons f fs) bool cur fail succ) == ...
  
  (find-formula-symbol x bool cur fail succ) == ..., where x is not bound in cur
  (find-formula-symbol x bool cur fail succ) == ..., where x is bool in cur
  (find-formula-symbol x bool cur fail succ) == ..., where x is (not bool) in cur

  Include the completed laws in your solution.

  The following unit tests will help make sure your function has the correct interface:

  (check-assert (procedure? find-formula-true-asst))    ; correct name
  (check-error (find-formula-true-asst))                ; not 0 arguments
  (check-error (find-formula-true-asst 'x))             ; not 1 argument
  (check-error (find-formula-true-asst 'x (lambda () 'fail)))   ; not 2 args
  (check-error
     (find-formula-true-asst 'x (lambda () 'fail) (lambda (c r) 'succeed) 'z)) ; not 4 args

  These additional checks also probe the interface, but they require at least a little bit of a solver—enough so that you call the success or failure continuation with the right number of arguments:

  (check-error (find-formula-true-asst 'x (lambda () 'fail) (lambda () 'succeed)))
      ; success continuation expects 2 arguments, not 0
  (check-error (find-formula-true-asst 'x (lambda () 'fail) (lambda (_) 'succeed)))
      ; success continuation expects 2 arguments, not 1
  (check-error (find-formula-true-asst
                     (make-and (list2 'x (make-not 'x)))
                     (lambda (_) 'fail)
                     (lambda (_) 'succeed)))
      ; failure continuation expects 0 arguments, not 1

  And here are some more tests that probe if you can solve a few simple formulas, and if so, if you can call the proper continuation with the proper arguments.

  (check-expect   ; x can be solved
     (find-formula-true-asst 'x
                             (lambda () 'fail)
                             (lambda (cur resume) 'succeed))
     'succeed)
  
  (check-expect   ; x is solved by '((x #t))
     (find-formula-true-asst 'x
                             (lambda () 'fail)
                             (lambda (cur resume) (find 'x cur)))
     #t)
  
  (check-expect   ; (make-not 'x) can be solved
     (find-formula-true-asst (make-not 'x)
                             (lambda () 'fail)
                             (lambda (cur resume) 'succeed))
     'succeed)
  
  (check-expect   ; (make-not 'x) is solved by '((x #f))
     (find-formula-true-asst (make-not 'x)
                             (lambda () 'fail)
                             (lambda (cur resume) (find 'x cur)))
     #f)
  
  (check-expect   ; (make-and (list2 'x (make-not 'x))) cannot be solved
     (find-formula-true-asst (make-and (list2 'x (make-not 'x)))
                             (lambda () 'fail)
                             (lambda (cur resume) 'succeed))
     'fail)

• cqs.continuations.txt containing your answers to the reading comprehension questions.
• solver-tests.scm containing the definitions of formulas f1, f2, and f3 and the definitions of solutions s1, s2, and s3.
• solution.scm containing the remaining functions.