Distributed: Published on the web on Oct 1.

Due: Oct 11 (in class)

Total maximum score: 100 points + 20 points of "bonus".

The purpose of this assignment is to provide experience with the simply typed lambda calculus.

Please write your solutions as clearly and concisely as possible.

**(50 pts)**For each of the following terms, 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. Please illustrate in detail all the steps of the unification algorithm.`\f x. f (f x)``\f x. x (f x)``\f g x. (f x) (g x)``(\f x. x) (\g. g g)``(\f x. x) (\g. g)`

Note: the type of a term can easily be found out by using the ML compiler. For this reason, a correct answer without justification will not get any credit.

**(30 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.`A -> (A -> B)``(A -> B) -> (C -> A) -> (C -> B)``(A -> (B -> C)) -> (A -> (B -> C))`

**(20 pts)**A fixpoint operator`Fix`is any lambda term that satisfies the equation`Fix M = M (Fix M)`for every`M`(where`=`here means lambda-convertibility). Some fixpoint operators (for instance the Turing's fixpoint operator) also have the property that`Fix M ->> M (Fix M)`.Assume that

`Fix`satisfies the property`Fix M ->> M (Fix M)`. Does it exist a`M`such that`Fix M`is typeable? Find such`M`or give a proof that such`M`cannot exist.**(20 pts, bonus question)**If a type`T`is inhabited, does it necessarily exist a term`M`**in normal form**such that`T`is the principal type of`M`? Justify your answer.**Hint:**If`M`is in normal form, then`M`has the form\x

with_{1}x_{2}...x_{n}. x N_{1}N_{2}...N_{k}`n, k >= 0`and where`N`are also terms in normal form. The variable_{1}, N_{2}, ..., N_{k}`x`can be one of the`x`or can be different._{1}, x_{2}, ..., x_{n}