Fall 2000, CSE 520: Assignment 2

Distributed: Published on the web on Sep 22.
Due: Oct 5 (in class).
Total maximum score: 100 points.

The purpose of this assignment is to provide experience with coding in lambda calculus, and with the notion of reduction in lambda calculus.

  1. (25 points) Encode in the lambda calculus the function "integer division", defined as follows:
    div(n,k) = p     if n = k*p + r   where   r is non negative and r < k
    Examples: div(7,3) = 2, div(9,3) = 3.

    Hint: you can use either minimalization or recursion.

  2. (20 points) For each of the following properties, say whether it holds or not on lambda terms. Justify your answers. P, M, N, and Q represent generic lambda terms, and -> and ->> are the relations defined in Lecture 6.
    1. (Confluence of ->) If P -> M and P -> N, then there exist Q such that M -> Q and N -> Q.
    2. (Weak confluence of ->) If P -> M and P -> N, then there exist Q such that M ->> Q and N ->> Q.

  3. (25 points) Consider an arbitrary binary relation -> on an arbitrary set A, and let ->> be the reflexive and transitive closure of -> as defined in Lecture 6. (For example, -> could be the relation of beta-reduction on lambda terms, or the standard ordering relation on natural numbers, or...)
    1. Does the confluence of -> imply the confluence of ->> ?
    2. Does the weak conluence of -> imply the confluence of ->> ?
    Justify your answers.

    Note: "Confluence of ->>" means of course that, if a ->> b and a ->> c, then there exists d such that b ->> d and c ->> d. The symbols a, b, c, and d here are arbitrary elements of the set A where -> and ->> are defined.

  4. (20 points) For each of the following lambda terms, say whether it is strongly normalizing, weakly normalizing, or not normalizing. Justify your answers. In case a term is normalizing (weakly or strongly), give its normal form.
    1. (5 points) [if_then_else]([is_zero] [0]) [1] Omega
    2. (5 points) [if_then_else]([is_zero] Omega) [0] [1]
    3. (10 points) Y F [3], where F is the lambda term which represents the functional used in the fixpoint equation of the factorial function, i.e.
      F =def= \u.\x. [if_then_else] ([is_zero] x) [1] ([times] x (u ([predecessor] x)))

    Note: Omega is the lambda term defined in Lecture 7.

  5. (10 points) Suppose that a lambda term M0 gives rise to an infinite chain of reductions
    M0 -> M1 -> M2 -> ... -> Mn -> ...
    Is it the case that the "size" of the terms is monotonically increasing, i.e. that for every n, the size of Mn+1 is bigger than, or equal to, the size of Mn ? Justify your answer.

    Note: by "size" of a lambda term M, here we mean its structural complexity, i.e. the height of a parse tree (or derivation tree) for M in the grammar generating M. If you don't know the definition of parse tree, please refer to the book

    Ravi Sethi. Programming Languages Concepts and Constructs. 2nd edition, Addison-Wesley, 1996.
    or to any other book on programming languages.