Fall 99, CSE 520: Assignment 2


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

The purpose of this assignment is to provide experience with the notion of reduction in lambda calculus, and with the higher order core of ML.

  1. (10 points) Define in ML the function "composition" which takes two arguments (one after the other, i.e. "composition" should be in curried style) and gives as result their functional composition, in the same order of application (i.e. on a generic input, the first argument is applied first, then the second is applied to the result). Example: if "plus2" is the function that adds 2 to its argument, and "mult3" is the function that multiplies its argument by 3, then (composition plus2 mult3) is the function that, on input n, gives as result (n+2)*3, and (composition mult3 plus2) is the function that, on input n, gives as result (n*3)+2.

  2. (10 points) Define in ML the function "twice" which takes one argument and gives as result its functional composition with itself. Example: if "plus2" and "mult3" are the functions defined as in Exercise 1, then (twice plus2) is the function that, on input n, gives as result n+4, and (twice mult3) is the function that, on input n, gives as result n*9.

  3. (5 points) Given the function twice defined as in Exercise 2, and a generic function f, is (twice twice f) equivalent to (twice (twice f)) ? Justify your answer.

    Note: by "equivalent" here we mean the same functional behaviour, i.e. same output for every input.

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

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

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

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