Please write your solutions as clearly and concisely as possible.
Justify your answer.
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.
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.
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.
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) : CWe 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.xHowever, 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.