Please write your solutions as clearly and concisely as possible.

1. (50 pts) For each of the following terms, say whether it is typeable or not, and, in the positive case, give its principal type. Justify your answer by constructing the proof, if the term is typeable, or by showing that a proof cannot be constructed. Please illustrate in detail all the steps of the unification algorithm.
   1. \f x. f (f x)
   2. \f x. x (f x)
   3. \f g x. (f x) (g x)
   4. (\f x. x) (\g. g g)
   5. (\f x. x) (\g. g)

   Note: the type of a term can easily be found out by using the ML compiler. For this reason, a correct answer without justification will not get any credit.

2. (30 pts) For each of the following types, say whether it is inhabited (i.e. there exists a term with such type) or not. Justify your answer by showing a term which has such type, or by proving that such term cannot exist. In case you find a term which has that type, say whether it is the principal type or not.
   1. A -> (A -> B)
   2. (A -> B) -> (C -> A) -> (C -> B)
   3. (A -> (B -> C)) -> (A -> (B -> C))

3. (20 pts) A fixpoint operator  Fix  is any lambda term that satisfies the equation   Fix M = M (Fix M)  for every   M   (where  =  here means lambda-convertibility). Some fixpoint operators (for instance the Turing's fixpoint operator) also have the property that   Fix M ->> M (Fix M).

   Assume that   Fix  satisfies the property   Fix M ->> M (Fix M). Does it exist a   M  such that   Fix M  is typeable? Find such   M  or give a proof that such   M  cannot exist.

4. (20 pts, bonus question) If a type   T  is inhabited, does it necessarily exist a term   M  in normal form such that   T  is the principal type of   M ? Justify your answer.

   Hint: If  M  is in normal form, then  M  has the form

      \x1x2...xn. x N1N2...Nk 
   

   with   n, k >= 0   and where   N₁, N₂, ..., N_k  are also terms in normal form. The variable   x   can be one of the   x₁, x₂, ..., x_n  or can be different.