Fall 2000, CSE 520: Assignment 1

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

The purpose of this assignment is to provide experience with Lambda Calculus, lambda conversion, and definability of functions in Lambda Calculus.

Note: the equality symbol in this text denotes lambda conversion, unless specified otherwise.

Please write your solutions as clearly and concisely as possible.

  1. (10 pts) Consider the following lambda terms:
    ADD = \p q x y. p x (q x y)
    MULT = \p q x. p (q x)
    Prove that they represent the addition and multiplication respectively, i.e. that for every natural number m and n,
    ADD [m][n] = [m+n]
    MULT [m][n] = [m*n]

  2. (15 pts) Prove that, if we add the axiom [1] = [2] to the theory of the lambda calculus, then the theory becomes inconsistent, in the sense that we can derive M = N for every lambda terms M and N.

    Hint: Consider the addition of the axiom [true] = [false]. Would the theory become inconsistent, in the above sense?

  3. (15 pts) Give a possible definition of the logical disjunction, i.e. define a lambda term OR such that
    OR [true] [true] = [true],
    OR [true] [false] = [true],
    OR [false] [true] = [true],
    OR [false] [false] = [false].

  4. (10 pts) For each of the following equations, define a lambda term M which satisfies the equation, for every N and P
    1. M N P = P (M P)
    2. M N P P = M P N
    Hint: Transform each equation into an equation of the form M = F M and then use the fixpoint operator.

  5. (25 pts) Give a representation in the lambda calculus of the data type list in ML, namely give an encoding for the following functions and constant:
    1. nil, the empty_list
    2. cons, the function which adds an element at the beginning of a list. For example, cons(a,cons(b,cons(c,nil))) represents the list [a,b,c]
    3. is_empty, the function that takes a list and returns true if the list is nil, false otherwise (note: here the square brackets are the ML notation for lists)
    4. head, the function which takes a list and returns its first element, if the list is not empty (otherwise it is undefined)
    5. tail, the function which takes a list L and returns the list obtained by removing the first element of L, if L is non empty (otherwise it is undefined).
    Hint: One possible way to solve this exercise is to use the Pair operator to represent cons. For instance, the list [a,b,c] would be represented as (a,(b,(c,nil))). In this way, head can be defined as the projection function First, and tail can be defined as the projection function Second. It only remains to define nil and is_empty so that they have the proper behavior.

  6. (25 pts) Define the function append in the lambda calculus. Namely, define a lambda term [append] such that, whenever applied to the lambda representations L1, L2 of two lists l1 and l2, we have that
    [append] L1 L2 = [append(l1,l2)]