Fall 99, CSE 520: Solution of MT

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) 
                               [true]
                               ([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

Observe that the term in the text of the exercise is Y, the fixpoint of Curry
- (a) The answer is yes. See Lecture Notes 3, 4 and 5 for the proof that Y F = F (Y F) for any F.
- (b) The answer is no. In fact the only possible reduction chains from Y F are of the form:
```
   Y F ->> (\f. f...f (\x. f (x x))(\x. f (x x))) F 
       ->  F...F (\x. F (x x))(\x. F (x x)))
       ->> F...F...F (\x. F (x x))(\x. F (x x)))
       ...   
```
  and none of these terms are alpha equivalent to F(Y F)
Let M =def= (\f x. f (x x f)). The term in the text of the exercise can then be written as M M.
- (a) The answer is no: there exists an F such that M M F is not lambda convertible to F (M M F). In fact, we have:
```
   M M F -> (\x. M (x x M)) F
         -> M (F F M)
         -> \x. (F F M) (x x (F F M)) 
```
  In order to reduce it to a normal form, define F =def= [true] = \x y. x. We have:
```
   M M [true] ->> \x. ([true] [true] M) (x x ([true] [true] M))
              ->> \x. [true] (x x [true])
              ->  \x y. x x [true]     (normal form)
   
```
  On the other hand, we have
```
   [true] (M M [true]) ->  \z. M M [true]
                       ->> \z x y. x x [true]     (normal form)
   
```
  Since the normal forms are different, by the Church-Rosser theorem, the two terms are not lambda convertible.
- (b) The answer is no, and it is an immediate consequence of previous answer (if two terms are not lambda convertible then they are not beta reducible either).

Exercise 4

(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.
A -> B -> A*B is inhabited. One term with this type is \x y (x,y)
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

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);

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.