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