• Oct 23 - Deadline extended to Thu, Oct 24. However, no late assignments accepted
• Oct 22 - Add a side condition for the 'capture case
• Oct 18 - Fixed typo in example call to step.
• Oct 16 - Various clarifications replacing x by 'x and trying to make clear where there are symbols. Added another side condition to capture-avoiding substitution.

This assignment will give you practice working with lambda calculus. Recall there is no textbook chapter on the lambda calculus. Instead, see the readings linked on the schedule on the class web page. (Note the second Ramsey handout includes a little bit of ML; you can ignore that and read the rest of the handout safely without understand it.) You can also look on Wikipedia.

There are no reading comprehension problems for this homework. Through this homework, we write \ for λ

Put your solutions to these problems in a file written.pdf.

1. For each of the following lambda terms, add parentheses to show how the term is parsed. For example, given \x.x x x, write \x.((x x) x). For this problem only, you should check your answers with the TAs, who will tell you whether they are correct or not.
   1. \x.x y
   2. \x.x \y.y
   3. \x.\y.x y y
   4. x \x.x y \y.y
2. For each of the following lambda terms, add an index to each variable so that it's obvious which variables correspond to which lambda bindings. Leave free variables without indices. For example, given x \x.x, write x \x1.x1. Each binding should have a unique index.
   1. \x.x y
   2. \x.x \x.x
   3. \x.\y.x y y
   4. \f.(\x.f (x x)) (\x.f (x x))
3. Write the result of each of the following substitutions on lambda terms. For example, given (\x.x y)[y ↦ z], write \x.x z. If necessary, alpha-convert to avoid capture.
   1. (y \x.x)[y ↦ z]
   2. (x \x.x)[x ↦ z]
   3. (x \x.y)[y ↦ z]
   4. (\x.x x)[x ↦ z]
   5. (\x.x y)[y ↦ x]
   6. (\x.\y.x y (x z))[z ↦ x]
4. Recall the rules for taking a single step in the lambda calculus (these rules exclude Eta-reduction and alpha conversion):

   
      ----------------------------- [Beta]
           (\x.M) N  →  M[x↦N]
   
                   M → M'
      ----------------------------- [Nu]
                 M N → M' N
   
                   N → N'
      ----------------------------- [Mu]
                 M N → M N'
   
                   M → M'
      ----------------------------- [Xi]
                \x.M → \x.M'
   

   Draw a derivation showing that each of the following reductions is possible following the rules above. For applications of [Beta], write the substitution above the line. For example, given \x.(\y.y) z → \x.z, you would write

   
            y[y↦z] = z
     ------------------- [Beta]
          (\y.y) z → z
    ------------------------- [Xi]
     \x.(\y.y) z → \x.z
   

   1. (\x.x) y → y
   2. (\x.y) z → y
   3. (\x.\y.x) w z →(\y.w) z
5. Using the reduction rules listed for the previous problem, reduce each of the following terms to normal form. Do not write the full derivation of each step of reduction. For example, given (\x.(\y.y) z) w, write (\x.(\y.y) z) w → (\x.z) w → z or write (\x.(\y.y) z) w → (\y.y) z → z.
   1. (\x.\y.x) w z
   2. (\n.(n \z.w) y) (\f.\x.f x)
   3. (\x.\y.\z.(x z) (y z)) (\a.a) (\b.b) c

In class, we saw how Church numerals can be written in µScheme with the following definitions:

(val true (lambda (x) (lambda (y) x)))
(val false (lambda (x) (lambda (y) y)))
(val zero (lambda (f) (lambda (x) x)))
(val one (lambda (f) (lambda (x) (f x))))
(val two (lambda (f) (lambda (x) (f (f x)))))
(val three (lambda (f) (lambda (x) (f (f (f x))))))
(val succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(val plus (lambda (n) (lambda (m) ((n succ) m))))

Implement the following µScheme functions involving Church numerals. You do not need to submit algebraic laws for these functions, but we highly encourage you to think through them and follow the usual design proces. You must, however, write test cases. Write your answers to this part and the next part in a file lambda.scm.

• Write a function (church-to-nat cn) that takes a Church numeral cn and returns the corresponding µScheme natural number. For example, (church-to-nat two) returns 2.
• Write a function (nat-to-church n) that takes a µScheme natural number n and returns the corresponding Church numeral. For example, (church-to-nat (nat-to-church 2)) returns 2.
• Write a function (parity cn) that, given a Church numeral cn, returns either zero if cn is even or one if cn is odd. Your parity function may only use lambda, variables, and application, i.e., it must be in the lambda calculus fragment of µScheme. For example, (church-to-nat (parity three)) returns 1 and (church-to-nat (parity two)) returns 0. Your solution must not use a fixpoint combinator.

Next, you will implement call-by-value beta-reduction on lambda terms. You will write your code for this part of the project using μScheme. You do not need to write algebraic laws, but you should write test cases. We will represent lambda terms using records constructed with the following definitions:

(record l-var [name])   ; variable
(record l-lam  [name body]) ; lambda
(record l-app [left right]) ; application

For example, here are some lambda terms and their representations:

    (make-l-lam 'x (make-l-var 'x))              ; \x.x

    (make-l-app (make-l-var 'x) (make-l-var 'y)) ; x y

    (make-l-lam 'x (make-l-lam 'y                ; \x.\y.x y
                               (make-l-app (make-l-var 'x)
                                           (make-l-var 'y))))

Implement the following functions over lambda terms.

• (free-in x t) returns #t if x occurs free in t and #f otherwise, where x is a symbol representing a variable. For example, (free-in 'x (make-l-var 'x)) returns #t.
• (free-vars t) returns a list (possibly with duplicates) of the free variables in lambda term t. For example, (free-vars (make-l-var 'x)) returns '(x)
• (subst 'x M N) returns N['x↦M], or returns 'capture if the substitution would cause a variable to be captured. Your function should obey these algebraic laws, where 'x and 'y are symbols representing variables and N and M are terms:
  • (subst 'x N (make-l-var 'x)) = N
  • (subst 'x N (make-l-var 'y)) = (make-l-var 'y) if 'x≠'y
  • (subst 'x N (make-l-app M1 M2)) = (make-l-app (subst 'x N M1) (subst 'x N M2))
  • (subst 'x N (make-l-lam 'x M)) = (make-l-lam 'x M)
  • (subst 'x N (make-l-lam 'y M)) = (make-l-lam 'y (subst 'x N M)) if 'x≠'y and ('y is not free in N or 'x is not free in M)
  • (subst 'x N (make-l-lam 'y M)) = 'capture if 'x≠'y and 'x is free in M and 'y is free in N
  (We're not having you implement capture-avoiding substitution in part because it would require a fair amount of tedium in µScheme and in part because it's a bit of a pain to grade.)
• Below are the two reduction rules for call-by-name lambda calculus, which excludes the Mu and Xi rules.

  
     ----------------------------- [Beta]
          (\x.M) N  →  M[x↦N]
  
                  M → M'
     ----------------------------- [Nu]
                M N → M' N
  

  Write a function (step M) that, using [Beta] and [Nu], performs one reduction step and returns the resulting term. If there is no possible reduction step, (step M) should return 'stuck. For example, (step (make-l-app (make-l-lam 'x (make-l-var 'x)) (make-l-var 'y)) should return (make-l-var 'y). As another example, (step (make-l-app (make-l-var 'x) (make-l-var 'y))) should return 'stuck. Assume that capture-avoiding substitution will never be needed, i.e., internal calls to subst will never evaluate to 'capture.
• Write a function (normal-form M) that keeps applying step to M until the term cannot be reduced any more, and then returns the result. Assume that capture-avoiding substitution will never be needed.

• File written.pdf, containing your answers to Part A.
• File lambda.scm containing your solutions to Parts B and C.