Note: the equality symbol in this text denotes lambda conversion, unless specified otherwise.

Please write your solutions as clearly and concisely as possible.

1. (10 pts) Consider the following lambda terms:

   ADD = \p q x y. p x (q x y)

   and

   MULT = \p q x. p (q x)

   Prove that they represent the addition and multiplication respectively, i.e. that for every natural number m and n,

   ADD [m][n] = [m+n]

   and

   MULT [m][n] = [m*n]

2. (15 pts) Prove that, if we add the axiom [1] = [2] to the theory of the lambda calculus, then the theory becomes inconsistent, in the sense that we can derive M = N for every lambda terms M and N.

   Hint: Consider the addition of the axiom [true] = [false]. Would the theory become inconsistent, in the above sense?

3. (15 pts) Give a possible definition of the logical disjunction, i.e. define a lambda term OR such that

   OR [true] [true] = [true],
   OR [true] [false] = [true],
   OR [false] [true] = [true],
   OR [false] [false] = [false].
   

4. (10 pts) For each of the following equations, define a lambda term M which satisfies the equation, for every N and P
   1. M N P = P (M P)
   2. M N P P = M P N
   Hint: Transform each equation into an equation of the form M = F M and then use the fixpoint operator.

5. (25 pts) Give a representation in the lambda calculus of the data type list in ML, namely give an encoding for the following functions and constant:
   1. nil, the empty_list
   2. cons, the function which adds an element at the beginning of a list. For example, cons(a,cons(b,cons(c,nil))) represents the list [a,b,c]
   3. is_empty, the function that takes a list and returns true if the list is nil, false otherwise (note: here the square brackets are the ML notation for lists)
   4. head, the function which takes a list and returns its first element, if the list is not empty (otherwise it is undefined)
   5. tail, the function which takes a list L and returns the list obtained by removing the first element of L, if L is non empty (otherwise it is undefined).
   Hint: One possible way to solve this exercise is to use the Pair operator to represent cons. For instance, the list [a,b,c] would be represented as (a,(b,(c,nil))). In this way, head can be defined as the projection function First, and tail can be defined as the projection function Second. It only remains to define nil and is_empty so that they have the proper behavior.

6. (25 pts) Define the function append in the lambda calculus. Namely, define a lambda term [append] such that, whenever applied to the lambda representations L1, L2 of two lists l1 and l2, we have that

   [append] L1 L2 = [append(l1,l2)]