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 = IⁿN = N

and

   [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

beta->alpha
Not tyepable for beta =/= alpha
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.

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.
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.
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

- The first answer is no. In fact, given a valid formula T, we know that it corresponds to an inhabited type T. Let M be a term with type T. Then also IM has type T, where I = \x.x. Since there is a one-to-one correspondence between terms and proofs, this means that we have at least two different proofs for T. In fact, we have infinitely many proofs, corresponding to M, IM ,IIM, IIIM, etc.
- The second answer is yes. In fact, take the formula alpha -> alpha. This is the (principal) type of the term I, which is in normal form. Observe now that I is the only term in normal form to have this type, in fact a normalized term must be of the form:
```
   \x₁x₂...x_n. x N₁N₂...N_k
```
  However, since we have only one -> in the type, n must be 1, and x must be x₁ because it can't be free. Moreover, k must be 0 because if we apply x₁ to any term then the type of x₁ cannot be simply alpha. In conclusion, the term must be \x₁. x₁, which is I.
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

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 -> ...
   ------------------------------------     ----------------------------    -----    -----

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

Typeable. The principal type is (A->B) * A -> B
Typeable. The principal type is A*B -> (A->C) -> (B->D) -> C*D
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

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
Inhabited. A term with this type is \x.inl x. It is the principal type.
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