###
*Fall 2001, CSE 520: Solution of Assignment 3*

## Exercise 1

- (A -> A) -> (A -> A)
- ((A -> B) -> A) -> (A -> B) -> B
- (A -> (B -> C)) -> (A -> B) -> A -> C
- Not typeable, because (\g. g g) is not typeable
- A -> A

## Exercise 2

- Not inhabited, because A -> (A -> B) is not a tautology (it is false for A = true and B = false)
- It is inhabited, for instance it is the principal type of the term \fgx. f (g x)
- It is inhabited, for instance it is a type of \x.x. But it is not its principal type, though.

## Exercise 3

It cannot exit a M such that (Fix M) is typeable.
In fact, if a term is typeable then it is strongly normalizing. But Fix M ->> M(Fix M) means that
(Fix M) has an infinite derivation of the form
Fix M ->> M(Fix M) ->> M(M(Fix M)) ->> ...

and therefore it cannot be strongly normalizing.
## Exercise 4

The answer is no. An example of type which is not the principal type
of any term in normal form is `A -> A -> A`. The proof is the following.
Assume by contradiction that such term `M` exists. Then
`M` has the form
`\x`_{1}x_{2}...x_{n}.
x N_{1}N_{2}...N_{k}.
Le t us construct the principal type of `M` by building a proof
for `|- M:T`, where `T` is a variable representing
a type expression.
Since `M` is typable, x cannot be a free variable, hence we must have
`n>=1`.
Hence the first rule applied in the proof must be the abstraction rule,
with a condition of the form `T = T`_{1} -> T_{2}
and a premise of the form

\x_{1}:T_{1} |- \x_{2}...x_{n}. x N_{1}N_{2}...N_{k} : T_{2}

Now, if n=1, then x_{1} = x, the next rule is the application, and one of the premises would be
\x_{1}:T_{1}|- x_{1} : T_{3} -> T_{2}

The unification `T`_{1} = T_{3} -> T_{2}
however would imply that the type of `M` is not of the form
`A -> A -> A` (because `A`
would have to be instantiated to a type of the form
`T`_{3} -> T_{4}). Hence the above
hypothesis is wrong, i.e. n must be at least 2.
As a consequence, the next rule must be the abstraction rule again,
with a condition of the form
`T`_{2} = T_{3} -> T_{4} and a premise
of the form
\x_{1}:T_{1}, x_{2}:T_{3} |- \x_{3}...x_{n}. x N_{1}N_{2}...N_{k} : T_{4}

At this point we see that we cannot use neither the abstraction nor the application rule,
for the same reason as above (we would instantiate the type too much). Hence we
must apply necessarily the var rule, which means that k = 0, n = 2, and x must either be
x_{1} or x_{2}. In the first case, the type of `M` will be
`T = T`_{1} -> T_{3} -> T_{1}, in the second case it will be
`T = T`_{1} -> T_{3} -> T_{3}. In both cases,
`T` is more general than `A -> A -> A`.
Note: even though `A -> A -> A` is not the principal
type of any term in normal form, there are terms (not in normal form, of course) that have
`A -> A -> A` as principal type.
We leave for exercise to find such a term.