## Exercise 1

A possible solution is
M =def= Y (\m n p. n m (p n))
In fact the equation
M N P = N M (P N)
is satisfied if the equation
M = (\m n p. n m (p n)) M
is satisfied. This is a fixpoint equation that can be solved by applying the fixpoint operator Y.

## Exercise 2

One solution is to give a recursive definition and then make the usual fixpoint construction. Note in fact that factorial can be defined recursively as:
```   factorial(0) = 1
factorial(n) = n * factorial(n-1)   if n > 0
```
hence we can define
```   [factorial] =def= Y (\f x. [if_then_else] ([is_zero] x) [1]  ([mult] x (f ([Predecessor] x))))
```

## Exercise 3

1. False: Omega has an infinite chain of reductions:
Omega -> Omega -> Omega -> ...
Hence, for any M, also the term M Omega has an infinite chain of reductions:
M Omega -> M Omega -> M Omega -> ...

2. True. For instance,
[true] [0] Omega -> (\y. [0]) Omega -> Omega
hence it is sufficient to consider M = [true] [0].

3. False. Following the same resoning as in (1) we get an infiite chain of reductions also for Omega M:
Omega M -> Omega M -> Omega M -> ...

4. False. Even if M has a normal form, Omega M does not have a normal form. In fact, Omega only reduces to itself, so Omega M can never reduce to a lambda redex. Therefore Omega and M reduce independently, and, even if M reduces to a normal form N, the Omega in front keeps reducing to itself
Omega M -> ... -> Omega N -> Omega N -> Omega N -> ...

## Exercise 4

1. Not typeable
2. (A -> (A -> B)) -> A -> B
3. ((A -> B) -> (B -> C)) -> (A -> B) -> A -> C

## Exercise 5

1. (B -> A) -> A is not inhabited. In fact, this type, seen as a formula, is not classically valid. In fact for B = true and A = false the formula is false.
2. A -> B -> B -> A is inhabited. One term with this type is \x y z. x. note that it is not the principal type, though. The principal type is A -> B -> C -> A
3. (A -> B) -> B -> A is not inhabited. For A = false and B = true the formula is false.