## Exercise 1

 ADD [m][n] = (\p q x y. p x (q x y)) [m] [n] = \x y. [m] x ([n] x y) = \x y. xm (xn y) = \x y. xm+n y = [m+n]
 MULT [m][n] = (\p q x. p (q x)) [m] [n] = \x. [m] ([n] x) = \x (\w y. w m y) ([n] x) = \x y. ([n] x)m y = \x y. ([n] x ([n] x (...([n] x y)...)))    m times = \x y. (xn (xn (...(xn y)...)))    m times = [m*n]

## Exercise 2

A possible proof is the following. Consider the encoding of the test is_zero and of the function predecessor seen in class:
[is_zero] = \z. z ([true][false])[true]
[predecessor] = \z. Second (z [aux] (Pair [0] [0]))
We have that [is_zero] ([predecessor] [1]) = [is_zero] [0]= [true] and [is_zero] ([predecessor] [2]) = [is_zero] [1] = [false]. If [1] = [2], then by the congruence rule we have [true] = [false], from which we derive, for every term M and N:
M = [true] M N = [false] M N = N.

## Exercise 3

A possible definition is
OR = \a b. [if_then_else] a [true] b
where [if_then_else] is the encoding of the conditional operator seen in class:
[if_then_else] = \x y z. x y z

Another (simpler, but equivalent) definition is

OR = \a b. a [true] b
Note that in both cases OR is short-circuit, i.e. if the first argument is [true], then the second does not need to be evaluated.

## Exercise 4

1. Observe that the equation   M N P = P (M P)   is satisfied if the equation   M = (\x y z. z (x z)) M   is satisfied. Then define   M =def= Y (\x y z. z (x z))   where   Y   is the fixpoint operator seen in class.
2. Observe that the equation   M N P P = M P N   is satisfied if the equation   M = (\x y z w. x z y) M   is satisfied. Then define   M =def= Y (\x y z w. x z y)
Alternatively, consider that the equation   M N P P = M P N   is satisfied if the equation   (\x y z. x z y y) M = M   is satisfied. Then define   M =def= Y (\x y z. x z y y).
Note that the two definitions are not equivalent, but they are both solutions.

## Exercise 5

One possible encoding of the data type "list", in the lambda calculus, is the following:
1. [nil] =def= \z. [true]
2. [cons] =def= Pair = \x y z. z x y
3. [head] =def= First = \p. p [true]
4. [tail] =def= Second = \p. p [false]
5. [is_empty] =def= \l. l (\x y. [false])
Note that we have
[is_empty] [nil] = (\l. l (\x y. [false])) (\z. [true]) = (\z. [true]) (\x y. [false]) = [true]
and
[is_empty] ([cons] A L) = (\l. l (\x y. [false])) (\z. z A L) = (\z. z A L) (\x y. [false]) = (\x y. [false]) A L = [false]

## Exercise 6

The function append can be defined recursively as follows:
append l k = if is_empty l then k else cons (head l) (append (tail l) k)
or equivalently, using the lambda notation:
append = (\f l k. if is_empty l then k else cons (head l) (f (tail l) k)) append
This is a fixpoint equation, hence we can solve it by using the fixpoint operator Y. Therefore we can define
[append] =def= Y (\f l k. ([is_empty] l) k ([cons] ([head] l) (f ([tail] l) k))
Where [is_empty], [cons], [head] and [tail] are the lambda terms previously defined.