Graded Assignment 2 CM20256 / CM50262 Functional Programming

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
list is [ ] = λ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
the numeral 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 (10%): Define terms head and empty such that
head [N, . . . ] →∗β N empty [ ] →∗β true empty [N, . . . ] →∗β false
(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 (30%): The terms Lm and L0m 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.)
L00 = n
L0m = c m L0m−1 for m > 0
Lm = λc.λn.L0m for any m
a) What list is represented by the term Lm ?
b) Prove by induction on m that
L0m [times/c, 1/n] →∗β m!
and hence that

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.
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 :
rnd Ni .
Explain how the presence of such an effect interacts with reduction strategies (normal
order, applicative order, and lazy evaluation) and with confluence.

Graded Assignment 2 CM20256 / CM50262 Functional Programming

Uploaded by

Copyright:

Available Formats

Graded Assignment 2 CM20256 / CM50262 Functional Programming

Uploaded by

Document Information

Original Description:

Original Title

Copyright

Available Formats

Share this document

Share or Embed Document

Sharing Options

Did you find this document useful?

Is this content inappropriate?

Copyright:

Available Formats

Graded Assignment 2 CM20256 / CM50262 Functional Programming

Uploaded by

Copyright:

Available Formats

Graded Assignment 2 CM20256 / CM50262 Functional Programming

This graded assignment is about using the lambda-calculus as a programming language.

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

Part 1 (10%): Show that the following term β -reduces to 6 :

Part 3 (10%): Define terms head and empty such that

Lm = λc.λn.L0m for any m

a) What list is represented by the term Lm ?

b) Prove by induction on m that

L0m [times/c, 1/n] →∗β m!

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

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

c) Unlike Haskell, the lambda-calculus has no input-output features, or other effects. A

You might also like