Fall 2001, CSE 520: Solution of Assignment 4

Exercise 1

The answer is yes. For instance, we can choose for N any typeable term, with type T, and for M the identity I = \x.x. Then have that, for every n:
   [n]IN = InN = N
   [n]IN : T
The latter is because [n]: (T->T)->(T->T), hence [n] I: (T->T), and therefore ([n]I)N : T.

Exercise 2

  1. beta->alpha
  2. Not tyepable for beta =/= alpha
  3. alpha

Exercise 3

We will prove by induction the following, more general statement: for every simply-typed term M, and every G, T1 and T2, if G |- M:T1 and G |- M:T2, then T1 = T2.

  1. Base case: M is a variable, say x. Then G |- x:T1 and G |- x:T2 is possible only if x:T1 and x:T2 are in G. But since all bound variables have different names, x can be present only once in G, and therefore it must be that T1 = T2.

  2. M is an abstraction, say \x:T.N. In this case, we must have T1 = T -> T3 for some T3, T2 = T -> T4 for some T4, G, x:T |- N:T3 and G, x:T |- N:T4. by inductive hypothesis, T3 = T4 and therefore T1 = T2.

    Note: this part is exactly what does not hold in the system of Curry: x is not obliged to have a specific type T and therefore we can assume different types for x, thus obtaining different types for \x.N.

  3. M is an application, say NP. In this case, we must have G |- N:T3->T1 (and G |- P:T3) for some T3, and G |- N:T4->T2 (and G |- P:T4) for some T4. By the inductive hypothesis, we have T3->T1 = T4->T2, which implies T1 = T2.

Exercise 4

  1. Both answer are yes. In fact, the church numerals [n] are all in normal form and all of them have type (alpha -> alpha) -> (alpha -> alpha).

Exercise 5

  1. Not normalizing. In fact the only reduction sequences are
       (\x. case(x,\x.Omega,I))(inl [false]) -> (\x. case(x,\x.Omega,I))(inl [false]) -> ...
                      -----                                    -----
       (\x. case(x,\x.Omega,I))(inl [false]) -> case(inl [false],\x.Omega,I) -> case(inl [false],\x.Omega,I) -> ...
       -------------------------------------                        -----                           -----
       (\x. case(x,\x.Omega,I))(inl [false]) -> case(inl [false],\x.Omega,I) -> Omega -> Omega -> ...
       ------------------------------------     ----------------------------    -----    -----

  2. Weakly normalizing. In fact we have at least one infinite reduction sequence
       (\x. case(x,\x.Omega,Y)(inr [false]) -> (\x. case(x,\x.Omega,Y)(inr [false]) -> ...
                      -----                                   -----
    and a normalizing reduction sequence
       (\x. case(x,\x.Omega,Y)(inr [false]) -> case(inr [false],\x.Omega,Y)
       ------------------------------------    ----------------------------           
                                            -> (\z.[false](zz))(\z.[false](zz))
                                            -> (\zy.y)(\z.[false](zz))
                                            -> \y.y (normal form)
    Note: By mistake the original term in this question was (\x. case(x,\x.Omega,Y)(inr [true]). This term is not normalizing.

Exercise 6

  1. Typeable. The principal type is (A->B) * A -> B

  2. Typeable. The principal type is A*B -> (A->C) -> (B->D) -> C*D

  3. Not typeable, because the rule for +elim needs the second and the third arguments of the case construct to be lambda abstractions. With the new rule proposed in the solution of Exercise 8, the term would be typeable and its principal type would be A+B -> (A->C)*(B->C) -> C.

Exercise 7

  1. Inhabited. A term with this type is \xy.snd x. The principal type of this term however is more general: it is A*B -> C -> B

  2. Inhabited. A term with this type is \x.inl x. It is the principal type.

  3. Not inhabited. The formula is not valid classically (take A = true and B = false) and therefore not valid intuitionistically either.

Exercise 8

           G |- M: A + B   G |- N: A -> C   G |- P: B -> C
   +elim ---------------------------------------------------  
                    G |- case(M, N, P) : C