Exercise 1

A possible solution is
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")

Exercise 2

One solution is to give a recursive definition and then make the usual fixpoint construction. Note in fact that is_even can be defined recursively as:
```   is_even(0) = true
is_even(n+1) = if is_even(n) then false else true
```
hence 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]
```

Exercise 3

1. 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)

2. 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).

Exercise 4

1. (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.
2. A -> B -> A*B is inhabited. One term with this type is \x y (x,y)
3. A -> (A -> B) -> B is inhabited. One term with this type is \x y. y x.

Exercise 5

All Church numerals [n] have type (A -> A) -> A -> A, which is also the principal type for n >= 2. This can be shown by induction: The base case (n=2) is immediate. For the inductive case, note that [n+1] = [succ][n] and that, if [n] has principal type (A -> A) -> A -> A, then [succ][n] has the same principal type (this can be shown easily by constructing a type proof for [succ][n]).

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

Exercise 6

1. 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);
```
2. 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.