###
*Fall 2001, CSE 520: Solution of MT exam*

## Exercise 1

A possible solution is
M =def= Y (\m n. n m n)

In fact the equation
M ([true] N P) = N M N

is satisfied if the equation
M N = N M N

is satisfied, and the latter is satisfied if is satisfied if the equation
M = (\m n. n m n) M

is satisfied. This is a fixpoint equation that can be solved
by applying the fixpoint operator Y.
## Exercise 2

One solution is to give a recursive definition and then
make the usual fixpoint construction. Note in fact that fibo can be defined
recursively as:
fibo = \x. if x = 0 then 1 else if x = 1 then 1 else fibo(x-1) + fibo(x-2)

hence we can define
[fibo] =def= Y (\f x. [if_then_else] ([is_zero] x)
[1]
([if_then_else] ([is_zero] ([predecessor] x))
[1]
([plus] (f ([predecessor] x)) (f ([predecessor] ([predecessor] x))))
)
)

## Exercise 3

- True, because we have at least one infinite derivation
M -> M -> M -> ...

**Note:** In the text which was distributed in class,
by mistake I wrote M ->> M instead of M -> M (which
was my intention and corresponds to the sentence "M is beta-reducible to itself").
Therefore the answers "false" here and in the last question of this exercise,
with the motivation that ->> is reflexive, are also considered correct.
- False. For instance, take M = [false] Omega, where
Omega = (\x.xx)(\y.yy). Then M -> M but M has also a normalizing derivation:
M -> \z.z

- True: all typeable terms are strongly normalizing.

## Exercise 4

The correct answer is the second: T_{1} and T_{2} must be instances of a common type.
In fact, by the Church-Rosser theorem, there must be a term M such that M_{1} ->> M
and M_{2} ->> M. By the subject reduction theorem, we have that M : T_{1} and
M : T_{2}. Thus, if T is the principal type of M,
T_{1} and T_{2} must be instances of T.
Note that T_{1} and T_{2} in general are not identical, because in the Curry
system the same term can have different types.

## Exercise 5

- ((A -> B -> A) -> C) -> C
- not typeable
- A -> (B -> A -> C) -> B -> C

## Exercise 6

- Inhabited. A term with that type is \xy.yx (it is not its principal type, though).
- Not inhabited: for beta = false, the formula is false.
- Inhabited. A term with that type is \fxy.fyx (and it is its principal type).