Please write your solutions as clearly and concisely as possible.

1. (30 pts) Complete the proof of the lambda-definability of recursive functions (Lecture 2) by defining the function "predecessor". Namely, find a lambda term P such that P [n+1] =_beta [n], where [n] is the encoding (Church's numeral) of the natural number n and =_beta stands for lambda conversion.

   Hint: the predecessor function pred can be defined in pseudo-code by the following declarations:

   fun aux(m,n) = (m+1,m)
   fun pred(n) = (auxⁿ(0,0)) Second

   Where Second is the projection on the second element of a pair, i.e. (a,b) Second = b. To see that the above is a correct definition, note that auxⁿ (0,0) = (n,n-1), hence (auxⁿ(0,0)) Second = n-1.

   As for the iteration of application, needed for encoding auxⁿ(0,0), note that the Church's numerals provide this capability. In fact, we have [n] M N =_beta MⁿN.

   Finally, for representing pairs (which are argument and result of aux), note that we can encode the pair (M,N) as \x. x M N. The projections First and Second will then be provided by the terms [True] and [False]. In fact: (\x. x M N)[True] =_beta [True] M N =_beta M and (\x. x M N)[False] =_beta [False] M N =_beta N. (Notation: the symbol "\" stands for the Greek letter lambda; [True] and [false] are the encodings of True and False as defined in Lecture 2). See also Barendregt92, Section 2.2 for the definition and use of the pairing construct.

2. (30 pts) Assume given the lambda terms P and T defining the "predecessor" and the "times" (multiplication) functions respectively, and define the function "factorial" as a lambda term.

3. (20 pts) Find a lambda term M such that, for every term N, M N =_beta N M holds. Hint: derive an equivalent equation of the form M = ... and use the fixpoint operator.

4. (10 pts)
   1. Prove that [True] and [False] are not lambda-convertible.
   2. Prove that, if we add the equation [True] =_beta [False] as an axiom of the theory, then all terms become convertible. I.e. we can derive M =_beta N for any M and N.

5. (10 pts) Assume that two lambda terms M₁ and M₂ are such that M₁ N =_beta M₂ N holds for every lambda term N. Does it follow that M₁ =_beta M₂? (Prove that it does follow or give a counterexample.)