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

  1. 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 -> ...

  2. True. For instance,
    [true] [0] Omega -> (\y. [0]) Omega -> Omega
    hence it is sufficient to consider M = [true] [0].

  3. 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 -> ...

  4. 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

  1. Not typeable
  2. (A -> (A -> B)) -> A -> B
  3. ((A -> B) -> (B -> C)) -> (A -> B) -> A -> C

Exercise 5

  1. (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.
  2. 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
  3. (A -> B) -> B -> A is not inhabited. For A = false and B = true the formula is false.