Fall 98, CSE 520: Solution of Assignment 1

Exercise 1

Let us define the pairing and the projection operators as follows:
Pair = \x y z. z x y
First = [True] = \x y. x
Second = [False] = \x y. y
Note that this definition is a correct encoding, since we have (Pair M N) First = M and (Pair M N) Second = N. Now define P = Predecessor as follows:
Aux = \x. Pair (Successor (x First)) (x First)
Predecessor = \n. n Aux (Pair [0] [0]) Second
Where Successor = \n x y. x(n x y) is the usual encoding of the successor function.

Exercise 2

Factorial must satisfy the equation 
Factorial = \n. [if_then_else] ([is_zero][n]) 
                               [1] 
                               (Times n (Facorial (Predecessor n)))
hence Factorial must be a fixpoint of the following function F (i.e.it must satisfy Factorial = F Factorial): 
F = \f. \n. [if_then_else] ([is_zero][n]) 
                           [1] 
                           (Times n (f (Predecessor n)))
Therefore we can define 
Factorial = Y F
where Y is the fixpoint operator.

Exercise 3

Observe that M has the required property if M satisfies
M = \x. x M
This is equivalent to saying that M is the fixpoint of the following function G:
G = \y x. x y
Hence we can define
M = Y G

Exercise 4

  1. By contradiction: If [True] = [False], then, by the Church-Rosser theorem they reduce to a common term Q, i.e. [True] ->>betaQ and [False] ->>betaQ for some Q. But [True] and [False] are both in normal form and they are not alpha-convertible, hence this is impossible.
  2. If [True] = [False] then for every M and N we have M = [True] M N = [False] M N = N.

Exercise 5

  1. The answer is no. Take for instance M1 = x and M2 = \y. x y.
(Note: The answer would be yes if we restrict M1, M2 to be closed terms, or if we add the axiom for eta-conversion.)