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.

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

  2. (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 = Fn X

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

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

  5. (9 points) For each of the following lambda terms, say whether it is strongly normalizing, weakly normalizing, or not normalizing. Prove your answer.

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

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

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

  6. (15 points) Assume that M is strongly normalizing. For each of the following sentences, say whether it is true or not. Justify your answer.

    1. M M   is necessarily strongly normalizing

    2. \x.M   is necessarily strongly normalizing

    3. If   M = N P   then N and P are necessarily strongly normalizing

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

    1. Y M   is strongly normalizing

    2. Y M   is weakly normalizing, but not strongly normalizing

    3. Y M   is not normalizing

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

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

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