Exercise 1

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

Exercise 2

1. The answer is no. Let Omega be the term \x. x x, and let M = (\x y. y) Omega. Then M is untypeable (because Omega is untypeable). But M has normal form P = (\y. y), which is typeable. In fact, P : A -> A (principal type).
2. The answer is no again. In general, if M ->> P and P:T, we cannot deduce that M:T, even if we know that M is typeable. The problem is that we could have the situation in which M:T' and T' is (strictly) and instance of T. Example: let M be the term Mult [0] [2] where Mult = \p q x. p (q x) (see Assignment #1). Then we have M ->> [0] and [0] : A -> B -> B and M is typeable, but the principal type of M is (C -> C) -> B -> B which is a strict instance of the type of [0].

Exercise 3

1. (A -> B) -> A     is not inhabited, because (interpreted as a formula) is not a tautology.
2. (A -> B) -> (B -> C) -> A -> C     is inhabited. One possible term for that type is \x y z. y (x z).
3. (A -> B -> C) -> (A -> B) -> A -> C     is inhabited. One possible term for that type is \x y z. (x z) (y z).