Fall 2001, CSE 520: Assignment 2
Distributed: Published on the web on Sep 18.
Due: Oct 2 (in class).
Total maximum score: 100 points.
The purpose of this assignment is to provide experience
with coding in lambda calculus, the fixpoint operator, and with the notion of reduction in
lambda calculus.
Please write your solutions as clearly and concisely as possible.
 (10 points)
Define a lambda term M which
satisfies the following equation, for every N and P:
M N P = (N M) (M P)
Hint: Transform the equation into an equation of the form M = F M and then use
the fixpoint operator.
 (10 points)
Define a lambda term Iterate which
satisfies the following equation, for every lambda terms F and X, and every natural number n:
Iterate F [n] X = F^{n} X
 (10 points)
Use the term Iterate of previous exercise to lambda define the function
minus on natural numbers, namely define a lambda term [minus] such that for every
natural numbers m and n we have
[minus][m][n] = [m  n] if m >= n
[minus][m][n] = [0] if m < n
 (25 points)
Define a lambda term corresponding to the function smallest_prime_factor.
Namely, define a lambda term Spf such that
for every natural number n we have
Spf [n] = [m] iff m is the smallest prime factor of n
Remember that the smallest prime factor of n is the smallest natural number m greater than 1 such that n is divisible by m.
 (9 points)
For each of the following lambda terms, say whether it is
strongly normalizing, weakly normalizing, or not normalizing. Prove your answer.

((\x.xxx)(\x.xx))(\yz.z)

(\yz.z)((\x.xxx)(\x.xx))

(\yz.z)(\x.xxx)(\x.xx)
 (15 points)
Assume that M is strongly normalizing. For each of the following sentences,
say whether it is true or not. Justify your answer.

M M is necessarily strongly normalizing

\x.M is necessarily strongly normalizing

If M = N P then N and P are necessarily strongly normalizing
 (15 points)
Let Y be the Church's fixpoint operator.
For each of the following properties, say whether or not it is possible to find
a M which satisfies it. Justify your answer.

Y M is strongly normalizing

Y M is weakly normalizing, but not strongly normalizing

Y M is not normalizing
 (6 points)
Let Dvg = (\x.xxx)(\y.yy).
For each of the following pairs of terms, say whether they are lambda convertible or not.
Justify your answer.

M = [true] [1] Dvg and N = [false] Dvg [1].

M = [true] [1] Dvg and N = [false] Dvg [0].