Fall 2001, CSE 520: Solution of Assignment 3

Exercise 1

  1. (A -> A) -> (A -> A)
  2. ((A -> B) -> A) -> (A -> B) -> B
  3. (A -> (B -> C)) -> (A -> B) -> A -> C
  4. Not typeable, because (\g. g g) is not typeable
  5. A -> A

Exercise 2

  1. Not inhabited, because A -> (A -> B) is not a tautology (it is false for A = true and B = false)
  2. It is inhabited, for instance it is the principal type of the term \fgx. f (g x)
  3. It is inhabited, for instance it is a type of \x.x. But it is not its principal type, though.

Exercise 3

It cannot exit a M such that (Fix M) is typeable. In fact, if a term is typeable then it is strongly normalizing. But Fix M ->> M(Fix M) means that (Fix M) has an infinite derivation of the form 
   Fix M ->> M(Fix M) ->> M(M(Fix M)) ->> ...
and therefore it cannot be strongly normalizing.

Exercise 4

The answer is no. An example of type which is not the principal type of any term in normal form is  A -> A -> A. The proof is the following.

Assume by contradiction that such term  M  exists. Then  M  has the form  \x1x2...xn. x N1N2...Nk. Le t us construct the principal type of  M  by building a proof for  |- M:T, where  T  is a variable representing a type expression. Since  M  is typable, x cannot be a free variable, hence we must have  n>=1. Hence the first rule applied in the proof must be the abstraction rule, with a condition of the form  T = T1 -> T2  and a premise of the form 

  \x1:T1 |- \x2...xn. x N1N2...Nk : T2
Now, if n=1, then x1 = x, the next rule is the application, and one of the premises would be 
  \x1:T1|- x1 : T3 -> T2
The unification  T1 = T3 -> T2  however would imply that the type of  M  is not of the form  A -> A -> A (because  A  would have to be instantiated to a type of the form  T3 -> T4). Hence the above hypothesis is wrong, i.e. n must be at least 2. As a consequence, the next rule must be the abstraction rule again, with a condition of the form  T2 = T3 -> T4  and a premise of the form 
  \x1:T1, x2:T3 |- \x3...xn. x N1N2...Nk : T4
At this point we see that we cannot use neither the abstraction nor the application rule, for the same reason as above (we would instantiate the type too much). Hence we must apply necessarily the var rule, which means that k = 0, n = 2, and x must either be x1 or x2. In the first case, the type of  M  will be  T = T1 -> T3 -> T1, in the second case it will be  T = T1 -> T3 -> T3. In both cases,  T  is more general than  A -> A -> A.

Note: even though  A -> A -> A   is not the principal type of any term in normal form, there are terms (not in normal form, of course) that have  A -> A -> A   as principal type. We leave for exercise to find such a term.