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

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

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

  3. True: all typeable terms are strongly normalizing.

Exercise 4

    The correct answer is the second: T1 and T2 must be instances of a common type. In fact, by the Church-Rosser theorem, there must be a term M such that M1 ->> M and M2 ->> M. By the subject reduction theorem, we have that M : T1 and M : T2. Thus, if T is the principal type of M, T1 and T2 must be instances of T.

    Note that T1 and T2 in general are not identical, because in the Curry system the same term can have different types.

Exercise 5

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

Exercise 6

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