CIS 352   —   SPRING 2008

Homework 5

Coverage

Logistics

You may work singly or in pairs on this assignment.

What to Turn in:

• The work for problems 1 through 4 below.

  Note: It is OK to use any of the lambda-calculus evaluators to check your work for these problems.
  But you'll have to do some of this on the next test, so please, please, please work them out by hand first.

• A copy of the source code and verified test cases demonstrating that your code for problem 5 is correct.
• Be sure to include contract and purpose statements for each procedure you are asked to write. (See the Homework Policy for more details.)

EXERCISES

Note: Typos in Exercises 1c, 1d, and 3a have been fixed.
… and in Exercise 1b.

1. (28 points) Do the following substitutions. Do not change any bound variables unless the substitution requires it.

   1. (w y)[(x z)/w]
   2. (lambda (y) (((x y) t) (x w)))[(t x)/x]
   3. (t (z y))[(x z)/w]
   4. ((lambda (y)((x y) t)) (w x))[(t x)/x]
   5. (lambda (w) (w y))[(lambda (w) w)/y]
   6. ((w x) (lambda (u) (t x)))[(u t)/x]
   7. ((lambda (r) ((r x) (lambda (t) (y t)))))[(r t)/x]

2. (12 points) For each of the following expressions, alpha-convert the leftmost y to t.

   1. (lambda (y) ((lambda (y) (x y)) (w y)))
   2. (lambda (y) ((lambda (t) (y t)) (y t)))

3. (12 points) Use the normal-order reduction scheme to beta-reduce the following two expressions to normal-form. In each step do only one beta-reduction and underline the redex you are reducing.

   1. ((lambda (t) ((x z) (z x))) (((lambda (z) (lambda (u) (u z))) t) z))
   2. ((lambda (t) (t t)) ((lambda (z) (t z)) x))

4. (12 points) Use the applicative-order reduction scheme to beta-reduce the following two expressions to normal-form. In each step do only one beta-reduction and underline the redex you are reducing.

   1. Expression a from Problem 3.
   2. Expression b from Problem 3.

5. (36 points) Write two Scheme procedures:

   find-norm-redex

   that takes a lambda-calculus expression exp (in abstract syntax form) and returns the redex that would be reduced first under normal-order reduction. If the expression does not contain an redex, the procedure should return #f; and

   
   

   find-app-redex

   that does the same thing as find-norm-redex except for applicative-order reduction.

   For example:

   > (define exp1 '(lambda (x) ((lambda (y) (x y)) ((lambda (z) z) (t y)))))
   
   > (define display-result
       (lambda (exp)
         (if exp (unparse exp) #f)))
   
   > (display-result (find-norm-redex (parse exp1)))
   ((lambda (y) (x y)) ((lambda (z) z) (t y)))
   
   > (display-result (find-app-redex (parse exp1)))
   ((lambda (z) z) (t y))
   
   > (display-result (find-norm-redex (parse '(lambda (x) (x y)))))
   #f
   
   > (display-result (find-app-redex (parse '(lambda (x) (x y)))))
   #f
   

   As you no doubt figured out, this is the part you will need to build on the code in lambda-calc.scm.