M =def= Y (\m n p. p m (p n m))For explanation, and for a similar exercise, see Lecture Notes 6 and 8 (Section "The fixpoint operators in lambda calculus")

is_even(0) = true is_even(n+1) = if is_even(n) then false else truehence we can define

[is_even] =def= Y (\f x. [if_then_else] ([is_zero] x) [true] ([if_then_else] (f ([Predecessor] x)) [false] [true]) )

Another solution, more interesting, can be given by using the iteration capability of Church numeralas:

[is_even] = \x. x [not][true]where [not] is the encoding of the logical negation:

[not] = \b. [if_then_else] b [false] [true]

- Observe that the term in the text of the exercise is Y, the fixpoint of Curry
**(a)**The answer is yes. See Lecture Notes 3, 4 and 5 for the proof that Y F = F (Y F) for any F.**(b)**The answer is no. In fact the only possible reduction chains from Y F are of the form:Y F ->> (\f. f...f (\x. f (x x))(\x. f (x x))) F -> F...F (\x. F (x x))(\x. F (x x))) ->> F...F...F (\x. F (x x))(\x. F (x x))) ...

and none of these terms are alpha equivalent to F(Y F)

- Let M =def= (\f x. f (x x f)). The term in the text of the exercise can then be written as M M.
**(a)**The answer is no: there exists an F such that M M F is not lambda convertible to F (M M F). In fact, we have:M M F -> (\x. M (x x M)) F -> M (F F M) -> \x. (F F M) (x x (F F M))

In order to reduce it to a normal form, define F =def= [true] = \x y. x. We have:M M [true] ->> \x. ([true] [true] M) (x x ([true] [true] M)) ->> \x. [true] (x x [true]) -> \x y. x x [true] (normal form)

On the other hand, we have[true] (M M [true]) -> \z. M M [true] ->> \z x y. x x [true] (normal form)

Since the normal forms are different, by the Church-Rosser theorem, the two terms are not lambda convertible.**(b)**The answer is no, and it is an immediate consequence of previous answer (if two terms are not lambda convertible then they are not beta reducible either).

- (A -> A) -> A is not inhabited. In fact, this type, seen as a formula, is not classically valid. In fact, A -> A is always true, hence (A -> A) -> A is false for A = false.
- A -> B -> A*B is inhabited. One term with this type is \x y (x,y)
- A -> (A -> B) -> B is inhabited. One term with this type is \x y. y x.

n = 0 and n = 1 are special cases. We have [0] : A -> B -> B, and [1] : (A -> B) -> A -> B.

- A possible solution is
val rec iterate = fn f => fn n => fn x => if n=0 then x else f (iterate f (n-1) x);

- A possible solution is
val Church_num = swap iterate;

where swap is the function that inverts the arguments of a function (swap g x y = g y x), see Exercise 4.3 in Assignment 3.