Fall 2000, CSE 520: Assignment 3

Distributed: Published on the web on Oct 5.
Due: Oct 19 (in class) Note: because of the Midterm, I need to publish the solutions on the web on Oct 19, so no turnins will be accepted after this date..
Total maximum score: 100 points.
The purpose of this assignment is to provide experience with the simply typed lambda calculus.

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 x)(f x)
    2. \f x. (f x)(f x x)
    3. \f g x. f (g x)
    4. \f g x. (f g) x
    5. \f g x. (f g)(g x)

    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. (20 pts) Consider a lambda term M and assume that it is weakly normalizing. Assume that the normal form of M has type T.
    1. Does it follow that M has type T as well?
    2. If M ->> N and N is typeable, does it follow that N has type T?
    For each answer, prove formally that it is true, or give a counterexample.

  3. (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 such type, or by proving that such term cannot exist.
    1. (A -> B) -> A
    2. (A -> B) -> (B -> C) -> (A -> C)
    3. (A -> (B -> C)) -> (A -> B) -> (A -> C)