Fall 99, CSE 520: Solution of MT exam

Exercise 1

A possible solution is
M =def= Y (\m n p. p m (p n m))
For explanation, and for a similar exercise, see Lecture Notes 6 and 8 (Section "The fixpoint operators in lambda calculus")

Exercise 2

One solution is to give a recursive definition and then make the usual fixpoint construction. Note in fact that is_even can be defined recursively as:
   is_even(0) = true
   is_even(n+1) = if is_even(n) then false else true
hence we can define
   [is_even] =def= Y (\f x. [if_then_else] ([is_zero] x) 
                               ([if_then_else] (f ([Predecessor] x)) [false] [true]) )

Another solution, more interesting, can be given by using the iteration capability of Church numeralas:

   [is_even] = \x. x [not][true]
where [not] is the encoding of the logical negation:
   [not] = \b. [if_then_else] b [false] [true]

Exercise 3

  1. Observe that the term in the text of the exercise is Y, the fixpoint of Curry

  2. Let M =def= (\f x. f (x x f)). The term in the text of the exercise can then be written as M M.

Exercise 4

  1. (A -> A) -> A is not inhabited. In fact, this type, seen as a formula, is not classically valid. In fact, A -> A is always true, hence (A -> A) -> A is false for A = false.
  2. A -> B -> A*B is inhabited. One term with this type is \x y (x,y)
  3. A -> (A -> B) -> B is inhabited. One term with this type is \x y. y x.

Exercise 5

All Church numerals [n] have type (A -> A) -> A -> A, which is also the principal type for n >= 2. This can be shown by induction: The base case (n=2) is immediate. For the inductive case, note that [n+1] = [succ][n] and that, if [n] has principal type (A -> A) -> A -> A, then [succ][n] has the same principal type (this can be shown easily by constructing a type proof for [succ][n]).

n = 0 and n = 1 are special cases. We have [0] : A -> B -> B, and [1] : (A -> B) -> A -> B.

Exercise 6

  1. A possible solution is
       val rec iterate = fn f => fn n => fn x => if n=0 then x else f (iterate f (n-1) x);
  2. A possible solution is
       val Church_num = swap iterate;
    where swap is the function that inverts the arguments of a function (swap g x y = g y x), see Exercise 4.3 in Assignment 3.