Fall 2001, CSE 520: Assignment 4

Distributed: Published on the web on Oct 15.
Due: Nov 8 (in class)
Total maximum score: 100 points.

The purpose of this assignment is to provide experience with various concepts about types.

Please write your solutions as clearly and concisely as possible.

1. (10 pts) Say whether it is possible to find two lambda terms M and N such that

• [0]MN = [1]MN = [2]MN = [3]MN = ... = [n]MN = ... where = here denotes lambda-conversion

• All the above terms are typeable and have the same type

2. (15 pts) For each of the following simply-typed terms, say whether it is typeable or not in the system of Church, and give the type if it exists. Justify your answer by constructing the proof, if the term is typeable, or by showing that a proof cannot be constructed. Note: in this exercise, alpha and beta represent basic types, and as such they cannot be equal to any other type.

1. \x:alpha->beta->alpha.\y:alpha.xy

2. \x:alpha->beta->alpha.\y:alpha.xyy

3. \x:alpha->(beta->beta)->alpha.\y:alpha.xy(\z:beta.z)

3. (15 pts) Prove by induction that if a term is typeble, in the system of Church, then its type is unique.

Note: remember that when we construct a proof in the type system we assume that all bound variables in the term are renamed so to have different names.

4. (20 pts) By using the Curry-Howard isomorphism, answer the following questions, and motivate your answer. Note:In both cases, ``formula'' refers to a formula of the implicational propositional fragment, namely a formula which is constituted by propositional names and implications only.

1. Does it exists a formula intuitionistically valid that has only one (intuitionistic) proof? And what is the answer if we consider only normalized proofs?

2. Does it exists a formula that has infinitely many (intuitionistic) proofs? And what is the answer if we consider only normalized proofs?

Note: it may be useful for this exercise to consider the characterization of normal forms for lambda terms given in the bonus question of Assignment 3.

5. (10 pts) For each of the following terms in the enriched lambda calculus, say whether it is normalizing, weakly normalizing, or not normalizing and, in the firts two cases, give its normal form. Omega represents the term (\z.zz)(\z.zz), I represents the term \z.z (identity), and Y represents the Church's fixpoint operator \z.(\w.z(ww))(\w.z(ww)).

1. (\x. case(x,\x.Omega,I))(inl [false])

2. (\x. case(x,\x.Omega,Y)(inr [false])

Note: In this enriched language, the characterization of normal forms given in the bonus question of Assignment 3 is not valid anymore. For instance, (\x. case(x,\y.y,\y.y)) is a term in normal form, although it is not in the form showed in Assignment 3.

6. (15 pts) For each of the following terms in the enriched lambda calculus, 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.

1. \x. (fst x) (snd x)

2. \xfg. (f(fst x), g(snd x))

3. \xy. case(x, fst y, snd y)

7. (15 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*B -> A -> B

2. A -> A+B

3. A -> A*B

8. (20 pts, bonus question) Note: The description of this exercise is long, but to my opinion the solution is rather easy, once you have understood the description.

In the enriched lambda calculus described in Lecture notes 12 and 13, the case construct has the form

```   case(Term, \Var.Term, \Var.Term)
```
And the corresponding typing rule is:
```           G |- M: A + B   G, x:A |- N: C   G, y:B |- P: C
+elim ---------------------------------------------------
G |- case(M, \x.N, \y.P) : C
```
We would like to modify the grammar so to allow a more general case construct of the form
```   case(Term, Term, Term)
```
The idea is that it should be permitted to use a construct like case(M,N,P), where N and P are arbitrary terms, provided that they reduce to terms that denote functions. For instance, we would like to be allowed to write terms like
```   case(inl(\x.x),(\y.y)(\z.z),\w.w)
```
This term is not allowed in the lecture notes because (\y.y)(\z.z) is not a lambda abstraction, although it reduces to the lambda abstraction \z.z.

If we just modify the grammar, then the reduction rules would still work and would allow for instance the following reduction sequence:

```  case(inl(\x.x),(\y.y)(\z.z),\w.w) -> case(inl(\x.x),\z.z,\w.w) -> \x.x
```
However, the term case(inl(\x.x),(\y.y)(\z.z),\w.w) would not pass the type-checking phase, because the typing rule above can only match with case-terms whose 2nd and 3rd arguments are lambda abstractions.

The exercise consists in modifying the typing rule for the case-terms so that a construct like case(inl(\x.x),(\y.y)(\z.z),\w.w) becomes typeable, while maintaining the same properties of the old type system (in particular, subject reduction). Of course, in order to maintain the correspondence with the OR-elimination rule of the logic, also the latter needs to be modified accordingly.

Note: This exercise is motivated by ML and other functional languages, which adopt the more permissive typing rule for the union type.