Please write your solutions as clearly and concisely as possible.

1. (35 pts) A lambda-term M is weakly normalizing if it reduces to a normal form, i.e. there exists M_n such that M ->_beta M₁ ->_beta M₂ ->_beta -> ... ->M_n and M_n is in normal form, i.e. M_n -/->_beta. Prove that all symply-typed lambda terms are weakly normalizing.

   Hint: Remember that the basic case of beta-reduction is (\x.M) N ->_beta M[N/x]. Note that, if (\x.M) and N are typeable, then we must have (\x.M) : A -> B, N : A, and M[N/x] : B, for some A and B.
   Define the order of a type as follows:

   • order(A) = 0 if A is in TVar
   • order(A -> B) = max(order(A)+1, order(B))
   and define the order of a typeable beta-redex (\x.M) N to be order(A -> B), where A -> B is the type of (\x.M).
   Now observe that in general, if M is typeable, then all its subterms are typeable, in particular the beta-redexes. We can then define a measure for M as the maximum of the orders of its beta-redexes.
   What is left to show, at this point, is that the measure of a term strictly decreases when applying a particular beta-reduction strategy, and use the (obvious) fact that the order of a beta-redex must be positive.

2. (35 pts) Consider an extension of the lambda Caluclus with pairing and projection operators (see notes of Lecture 11), and consider the language of types

      Type ::= TVar            % type variable
             | Type -> Type    % functional type
             | Type * Type     % cartesian product type
   

   For each of the following types, say whether it is inhabited or not. Justify the answer.
   1. (A -> (B -> C)) -> (A -> B) -> (A -> C)
   2. (A -> B) -> (B -> A)
   3. (A * B) -> A
   4. A -> (A * B)
   5. (A -> (B -> C)) -> ((A * B) -> C)

   Hint: To show that a type A is inhabited, it is sufficient to show that there exists a term M such that |- M : A can be proved in the type system of Curry. The idea is to try to construct such a proof, with M unspecified at the beginning, and then let M be determined by the construction of the proof.
   To show that a type A is not inhabited, one can proceed in two ways:

   • Show directly that such a proof (in the type system) cannot be built for any M, or
   • Use the Curry-Howard isomorphism and the fact that intuitionistic provability implies classical provability. (Thus, if a formula is not valid in classical logic, it is not provable in intuitionistic logic either.) Remember that, in the interpretation of types as formulas, -> stand for "logical implication" and * for "logical and".

3. (30 pts) Define in CCS a buffer with n cells, by recursion on n, and using one-cell buffers (see notes of Lecture 15). You can use equations and input-output actions with parameter-passing.

   Hint: Generalize the method explained in Lecture 16 for obtaining a two-cells buffer from two one-cell buffers.