###
*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.

- (10 pts)
Consider the following lambda terms:
ADD = \p q x y. p x (q x y)

and
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]

and
MULT [m][n] = [m*n]

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

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

- (10 pts)
For each of the following equations, define a lambda term M which
satisfies the equation, for every N and P
- M N P = P (M P)
- 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.
- (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:
- nil, the empty_list
- 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]
- 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)
- head, the function which takes a list and returns its first element,
if the list is not empty (otherwise it is undefined)
- 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.
- (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)]