Fall 99, CSE 520: Solution of Assignment 1

Exercise 1

ADD [m][n] = (\p q x y. p x (q x y)) [m] [n]
= \x y. [m] x ([n] x y)
= \x y. xm (xn y)
= \x y. xm+n y
= [m+n]
MULT [m][n] = (\p q x. p (q x)) [m] [n]
= \x. [m] ([n] x)
= \x. [m] ([n] x)
= \x y. ([n] x)m y
= \x y. ([n] x ([n] x (...([n] x y)...)))    m times
= \x y. (xn (xn (...(xn y)...)))    m times
= [m*n]

Exercise 2

A possible proof is the following. Consider the encoding of the test is_zero seen in class:
[is_zero] = \z. z ([true][false])[true]
We have that [is_zero] [0] = [true] and [is_zero] [1] = [false]. If [0] = [1], then by the congruence rule we have [true] = [false], from which we derive, for every term M and N:
M = [true] M N = [false] M N = N.

Exercise 3

A possible definition is
AND = \a b. [if_then_else] a b [false]
where [if_then_else] is the encoding of the conditional operator seen in class:
[if_then_else] = \x y z. x y z

Another (simpler, but equivalent) definition is

AND = \a b. a b [false]
Note that in both cases AND is short-circuit, i.e. if the first argument is [false], then the second does not need to be evaluated.

Exercise 4

  1. The answer is yes: if M and N are such that, for every lambda term P, we have P M = P N, then it does follow that M = N. Let in fact P to be the identity function, i.e. P = \x. x. We have:
    M = (\x. x) M = (\x. x) N = N.
  2. The answer is no: even if M and N are such that, for every lambda term P, we have M P = N P, still it does not follow that M = N. Consider in fact M = y and N = \x. y x. We have that, for every P,
    M P = y P = (\x. y x) P = N P
    However M and N are both in normal form and they are not alpha-convertible. Note: The answer would be yes if we restricted M and N to be closed terms, or if we added the axiom eta.

Exercise 5

The function exp(n) = 2n can be defined by (primitive) recursion as follows:
exp(0) = 1
exp(n+1) = 2 * exp(n)
We can then define EXP = [exp] by using the fixpoint operator Y seen in class:
EXP = Y M
where M is defined as follows:
M = \f x. [if_then_else] ([is_zero] x) [1] (MULT [2] (f ([pred] x)))
where pred(n) = n - 1; its encoding in the lambda calculus has been defined in class.

Another possible definition is the following:

EXP = \z x. z [2] x
The proof that this alternative definition is correct too is similar to the proof of corrcetness of MULT (Exercise 1).

Exercise 6

The function log(n) = k iff n = 2k can be defined by minimalization as follows:
log(n) = mu k. | 2k - n | = 0
where | m - n | represents the absolute value of m - n, i.e. the distance between m and n. Such function can be defined by general recursion as follows:
distance(0,n) = n
distance(m,0) = m
distance(m+1,n+1) = distance(m,n)
Hence we can define
[distance] = Y M
where
M = \f x y. [if_then_else] ([is_zero] x) y ([if_then_else] ([is_zero] y) x (f ([pred] x) ([pred] y)))
Finally, by applying the technique for encoding minimalization seen in class, we can define LOG = [log] as follows:
LOG = (Y N) [0]
where
N = \f x y. [if_then_else] ([is_zero] ([distance] (EXP x) y) ) x (f ([S] x) y)
where S is the successor function.