Haskell代写 | 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 (L ATEX, 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!

Lists Lists can be encoded in the lambda-calculus in the following way:

[N1,N2,…,Nk] , !c. !n. c N1 (cN2 (… (cNk 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 nm 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 (lcn)
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 4 (25%): The terms Lm and L0
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.)
0 = n
m = cmL0
m%1 for m> 0
Lm = !c.!n.L0
m for any m

a) What list is represented by the term Lm ?

b) Prove by induction on m that
m[times/c, 1/n] !⇤
! m!
and hence that
Lm times 1 !⇤
! m!
where m! means the factorial of m.