Please write your solutions as clearly and concisely as possible.

1. (30 pts) For each of the following pairs of lambda terms, say whether they are lambda convertible or not. In the positive case, please indicate which rules have to be applied for the conversion (alpha, beta, symmetry, transitivity, congruence 1 and 2, xi).
   1. \x.xy   and   \x.xz
   2. \x.xy   and   \y.yy
   3. \x.xy   and   \z.zy
   4. (\x.xy)(\z.z)   and   y
   5. (\x.xy)(\z.z)y   and   yy
   6. (\xz.x)(\w.w)y   and   \z.y
   7. (\xz.x)(\w.w)y   and   \w.w
   8. (\xz.x²z)(\y.y)   and   \z.z
   9. (\xz.x²z)(\y.y)   and   (\w.w)(\z.z)
   10. (\xz.x²z)(\y.y)   and   (\zw.zw)

2. (9 pts) Consider the following definitions:
   • S = \xyz.xz(yz)
   • K = \xy.x
   • B = \xyz.x(yz)
   • I = \x.x
   Prove that:
   1. SKK   and   I   are lambda convertible.
   2. S(KS)K   and   B   are lambda convertible.
   3. S(KI)   and   BI   are lambda convertible.

3. (20 pts) Prove that, if we added the axiom   \xy.xy = \xy.yx   to the theory of lambda convertibility, then all terms would become equal (i.e. lambda convertible).

4. (15 pts) Consider the function   exp(m,n) = n^m.   Prove that this function is Recursive by showing that it can be obtained from the Initial functions by using composition, primitive recursion, and minimalization. You can use the functions already defined in class and/or in the lecture notes. For every new definition, give the details of the construction (for instance, if you use primitive recursion, say what exactly are the functions g and h).

5. (26 pts) Define in lambda calculus the function   rem2 : N -> N,   which returns 0 if the argument is even, and 1 if the argument is odd (for instance,   rem2(0) = 0, rem2(1) = 1, rem2(2) = 0, rem2(3) = 1,   etc.). Namely, construct the lambda-term   [rem2]. You can use the functions already defined in class and/or in the lecture notes.

   ---