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

## Exercise 1

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

In fact the equation
M N P = N M (P N)

is satisfied if the equation
M = (\m n p. n m (p 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 factorial can be defined
recursively as:
factorial(0) = 1
factorial(n) = n * factorial(n-1) if n > 0

hence we can define
[factorial] =def= Y (\f x. [if_then_else] ([is_zero] x) [1] ([mult] x (f ([Predecessor] x))))

## Exercise 3

- False: Omega has an infinite chain of reductions:
Omega -> Omega -> Omega -> ...

Hence, for any M, also the term M Omega has an infinite chain of reductions:
M Omega -> M Omega -> M Omega -> ...

- True. For instance,
[true] [0] Omega -> (\y. [0]) Omega -> Omega

hence it is sufficient to consider M = [true] [0].

- False. Following the same resoning as in (1) we get an infiite chain
of reductions also for Omega M:
Omega M -> Omega M -> Omega M -> ...

- False. Even if M has a normal form, Omega M does not have a
normal form. In fact, Omega only reduces to itself, so Omega M can never
reduce to a lambda redex. Therefore Omega and M reduce independently, and,
even if M reduces to a normal form N, the Omega in front keeps reducing to
itself
Omega M -> ... -> Omega N -> Omega N -> Omega N -> ...

## Exercise 4

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

## Exercise 5

- (B -> A) -> A is not inhabited. In fact, this type, seen as a formula, is not classically valid.
In fact for B = true and A = false the formula is false.
- A -> B -> B -> A is inhabited. One term with this type is \x y z. x.
note that it is not the principal type, though. The principal type is A ->
B -> C -> A
- (A -> B) -> B -> A is not inhabited. For A = false and B = true the
formula is false.