Graded Assignment 2 CM20256 / CM50262 Functional Programming
Graded Assignment 2
This graded assignment is about using the lambda-calculus as a programming language. Your solutions should be submitted as a PDF file. You may write the solutions using appro- priate software (LATEX, Word, etc.) or as a clearly legible handwritten document that you scan to PDF. Throughout this assignment, you could of course write your solutions as pure lambda-terms, but that would be very hard to read. Make use of abbreviations to ensure that your solutions to these exercises are readable!
Note that this graded assignment is an individual assignment. Collaboration on this as- signment is not permitted: you should not discuss your work with others, and the work you submit should be your own. Failure to observe this constitutes plagiarism: see http://www.bath.ac.uk/quality/documents/QA53.pdf.
Lists Lists can be encoded in the lambda-calculus in the following way: [N1,N2,…,Nk] λc.λn.c N1 (c N2 (…(c Nk n)…))
Intuitively, the variable c represents the cons operation (which adds an item to the head of the list) and the variable n represents the empty list, nil: note that the term for the empty listis []=λc.λn.n.
Part 1 (10%): Show that the following term β -reduces to 6 : [3,2,1] times 1
Here the numerals 1 , 2 , 3 , . . . denote the λ -terms for the corresponding Church numerals, and times is the term for multiplication. You may use the fact that times n m reduces to thenumeral n×m.
Part 2 (10%): The term cons appends an element to the front of a list. cons λx.λl.λc.λn. c x (l c n)
Show that it works by reducing cons 3 [2, 1] to [3, 2, 1] . Make sure to include every β -step, and try to use abbreviations for readability.
Part 3 (15%): Define terms head and empty such that
head [N,…] →∗β N empty [] →∗β true empty [N,…] →∗β false
Graded Assignment 2 CM20256 / CM50262 Functional Programming
(where →∗β means reduction by any number of β -steps). The term head [ ] is an error in most programming languages; in this lambda-calculus version, it may reduce to whatever you like.
Part 4 (25%): The terms Lm and L′m for each natural number m are defined as follows. (Note that n and c are variables while m stands for a number or its Church encoding.)
L′0 = n
L′m = cmL′m−1 form>0
Lm = λc.λn.L′m for any m
a) What list is represented by the term Lm ?
b) Prove by induction on m that
and hence that
L′m[times/c, 1/n] →∗β m! Lm times 1 →∗β m!
where m! means the factorial of m . Part 5 (20%):
a) Give a λ -term that corresponds to the foldr function in Haskell. That is, your term foldr should have the property that
foldr f u [N1,…,Nk] →∗β f N1 (f N2 (… (f Nk u)))
b) Give a λ -term that corresponds to the map function. That is,
map f [N1,…,Nk] →∗β [f N1,f N2,…,f Nk]
c) Write a λ -term that corresponds to the infinite list
[0,1,2,…]
You should explain why your functions work as they are supposed to. You need not give a
complete formal proof: a convincing explanation is all that is required.
Part 6 (20%): This last part consists of three technical but more open-ended questions. Please take care to give a full answer that demonstrates your understanding of the concepts involved.
Graded Assignment 2 CM20256 / CM50262 Functional Programming
a) For your three solutions for Part 5, (a) foldr, (b) map, and (c) the infinite list [0, 1, 2, …] , explain if they can be typed, and why (not). For each, is it possible that there is a solution in the typed lambda-calculus?
b) Suppose we have a lambda-term take corresponding to Haskell’s take :: Int -> [a] -> [a]
and we use it in the following lambda-term ten. ten=take 10 [0,1,2,…]
Use the concepts of confluence, weak normalization, and strong normalization to ex- plain how many normal forms the term ten has, and if it might diverge (i.e. if it has an infinite beta-reduction).
c) Unlike Haskell, the lambda-calculus has no input-output features, or other effects. A naive way of adding effects is via constants: primitive functions that (notionally) carry out a side-effect. For instance, we could add a function rnd which represents a random Church numeral, with for every i ∈ N the following reduction rule, where Ni is the church numeral corresponding to i :
rndNi .
Explain how the presence of such an effect interacts with reduction strategies (normal order, applicative order, and lazy evaluation) and with confluence.