Out: October 2, 2007
Due: October 9, 2007
Last year, on the corresponding problem set, the median reported time on task was 10.5 hours.
I've collected some FAQs for this problem. Please look at this archive before asking questions about the interpretation of the problem.
For this machine problem, you will extend a language discussed in class. Please note the requirement on page 67:
Your base interpreter is the one in http://www.ccs.neu.edu/course/csg111/interps/lecture03/letrec-lang/.
Test your solution by adding new tests to tests.scm. Be sure to keep all the existing texts so that you don't break anything.
Be sure to add enough test items to the test suite so that your extensions will be adequately tested. As before, you will be graded on the quality of your test suite.
Each exercise is worth 5 points.
Expression ::= allof Expression {and Expression}* endThis expression takes the conjunction (``and'') of several expressions, such as
allof zero?(x) end allof zero?(x) and zero?(y) end allof zero?(x) and zero?(-(y,1)) end allof zero?(x) and not(zero?(y)) and zero?(-(u,x)) endThis is to evaluate the expressions from left to right, and produce a true value iff all expressions have a true value, so that one could write an expression like if allof x and y end then x else z. It is, however, a ``short-cutting'' operator: if one expression gives a false value, then the rest of the expressions should not be evaluated. Here are a couple of tests to get you started:
(allof-1-arg-1 "if allof zero?(0) end then 3 else 4" 3) (allof-2-get-second " let x = 0 in let y = 1 in if allof zero?(x) and zero?(y) end then 33 else 44" 44) (allof-2-check-shortcutting " let f = proc (x) aha % raises error if called in if allof zero?(1) and (f 1) end then 3 else 4" 4)
In this exercise, questions you need to answer or code you need to write is indicated in bold.
Consider the following programming language CNF-LET: Class Dictionary and sample programs
The class dictionary defines an XML-like language for CNF-LET programs. There is also a sample program that shows an example reduction sequence.
An XML user would write a XML schema or an DTD instead of a class dictionary. (Are there any XML experts in the class? If so, share the corresponding XML schema or DTD with the class on the mailing list.) The mark-up language syntax makes it really easy to satisfy the LL(1) condictions. Why is that?
Note that the programming language PROC in chapter 3 provides the techniques to implement this language CNF-LET. With PROC we can express the equivalent of the following Scheme function:
;; curry : (A * B -> C) * A -> (B -> C) ;; Given a two argument function (f x y), and a first argument x, ;; returns a function g such that (g y) = (f x y). ;; Examples: ;; ((curry + 3) 4) ==> 7 ;; (let ([add1 (curry + 1)]) ;; (list (add1 2) (add1 3))) ==> '(3 4) ;; (curry + 0) ==> (lambda (y) (+ 0 y)) (define curry (lambda (f x) (lambda (y) (f x y))))A potential problem with beta reduction is that the interpreter only keeps the argument information in a closure. Remember that the procedure datatype has 3 fields: argument, body, and saved env. Suppose we had a function f of 101 arguments to which we supply 100, naming the new function f100. The 100 arguments we've given so far are all stored in the saved env, and only when we supply an additional arguments to f100 does any evaluation actually occur. Even if most of the work could be done without the last argument, the interpreter redoes all the work each time f100 is used! Notice in the last example for curry that since 0 + y = y, if we're clever we could make (curry + 0) evalute to just (lambda (y) y) instead. If we computed (curry + 0) once and used the resulting function many times, we'd save the trouble of doing the redundant addition of 0 each time. This technique is called partial evaluation.
Now let's again consider the language CNF-LET. Language PROC has ExpVal = Int + Bool + Proc = DenVal. What are the denoted and expressed values for CNF-LET? In CNF-LET, all our Boolean expressions are in CNF, and therefore doing a the reduction for setting a literal v to true (or false) is straightforward. Some clauses will become satisfied or unsatisfied and others will be reduced by one literal. Under what conditions does assigning one literal cause a clause to be satisfied, unsatisfied, or shrink? One application of a partially-evaluating CNF-LET is to compute the Shannon decomposition of a Boolean function: F(x) = E where E is a Boolean expression in conjunctive normal form. The Shannon decomposition has many applications, for example in SAT and MAXSAT solvers. The Shannon decomposition of F(x) is given by:
F(x) = x * F(x=1) + !x * F(x=0)If we have two variables, we can express this using curry:
;; red_1, red_0: (Bool * Bool -> Bool) -> (Bool -> Bool) ;; Partially apply a two argument function on true (or false), ;; yielding a one argument function. (define (red_1 f) (curry f #t)) (define (red_0 f) (curry f #f)) ;; shannon: (Bool * Bool -> Bool) * Bool * Bool -> Bool ;; Shannan-decompose a two argument boolean function and apply ;; it to boolean arguments. (define shannon (lambda (f x y) (or (and x ((red_1 f) y)) (and (not x) ((red_0 f) y))))) (define or-fun (lambda (x y) (or x y))) (define imp-fun (lambda (x y) (or (not x) y))) (define test (lambda (f x y) (eq? (f x y) (shannon f x y)))) (test or-fun #t #t) (test or-fun #t #f) (test or-fun #f #t) (test or-fun #f #f) (test imp-fun #t #t) (test imp-fun #t #f) (test imp-fun #f #t) (test imp-fun #f #f)With your implementation of CNF-LET it will be easy to print the Shannon factor (red_1 f) and cofactor (red_0 f) for function f.
Implement a partially-evaluating interpreter for CNF-LET. You will of course need to implement a parser for CNF-LET's concrete syntax, and define a datatype to represent its abstract syntax. Your interpreter should provide these two functions:
;; cnf-let-reduce : cnf-let-program -> cnf-let-program ;; Perform one reduction step of a CNF-LET program. Partially ;; evaluates the outermost let of each expression in the ;; program. In the output program, each expression has one fewer ;; let than before, and the variable bound by the reduced ;; let no longer appears in the cnf. Any expressions that are ;; fully reduced to cnf are left unchanged. ;; Examples: See the sample program. This is a single program with ;; with three expressions, but the expressions themselves form a ;; reduction sequence; the final expression is fully reduced. ;; value-of-cnf-let : cnf-let-program -> [List-of Integer] ;; Reduce a CNF-LET program completely. Performs reduction a la ;; cnf-let-reduce until no redexes remain, and then returns ;; a list of integer results for each expression, where the ;; value of an expression is the difference sat - unsat. ;; ;; Examples: See the example program.How could reduction go wrong? In what situation could it be impossible to reduce an expression all the way? Your code should address any such situation.
Use adequate test cases. As usual, you will be graded on the quality of your testing.
Hint: As you reduce one let expression into the cnf, build a new clause list. Add weights of any satisfied clauses to sat and the weights of any unsatisfied clauses to unsat. Clauses that are unchanged or have a literal removed are added to the new clause list.
To-do list:
Last modified: Fri Feb 9 07:15:43 EST 2007