Session 1, 2004
Exercises: Lambda Calculus
The following exercises should help you develop a better understanding
of how the lambda calculus works.
A note on notation: In the following, I use the Haskell syntax
\x > e to denote lambda expressions .
Translation of let Bindings into the Plain Lambda
Calculus
In the lecture, we discussed that we can translate nonrecusive and
recursive let bindings into the plain lambda calculus as follows:
Nonrecursive binding: 

let x = e_{1} in e_{2}



=> 
(\x > e_{2}) e_{1}


Recursive binding: 

let x = e_{1} in e_{2}



=> 
let x = fix (\x > e_{1}) in e_{2}

where the fixed point
combinator fix is defined to be the function
fix :: (a > a) > a
fix f = f (fix f)
Your task is to find a translation rule for mutually recursive bindings
of the form
let {x_{1} = e_{1}; ...;
x_{n} = e_{n}}
in e
where the x_{i} may occur in the
e_{i} as well as in e . (Hint: It is
sufficient if you turn the set of mutuallyrecursive bindings into a
single recursive binding to which the previous rules can, then, be
applied.)
Translation of Data Constructors and case into the Plain
Lambda Calculus
In the lecture, we discussed that
pair = \a1 > \a2 > \sel > sel a1 a2
fst = \p > p (\a1 > \a2 > a1)
snd = \p > p (\a1 > \a2 > a2)
encodes pair construction (pair ) and decomposition
(fst and snd ). In particular, the following
rules are satisfied:
fst (pair e1 e2) = e1
snd (pair e1 e2) = e2
Your tasks is to find an implementation of the constructors
nil and cons , the destructors
head and tail , and the conditional
ifNull , which encode lists and have to satisfy the
following rules:
head (cons e1 e2) = e1
tail (cons e1 e2) = e2
ifNull nil e3 e4 = e3
ifNull (cons e1 e2) e3 e4 = e4
Afterwards, implement the function
map f [] = []
map f (x:xs) = x : map f xs
in terms of nil , cons , head ,
tail , and ifNull (without using
case , [] , (:) , or
patternmatching).
