# Haskell代写 | Functional Programming Graded Assignment 2

本次CS代写是Haskell函数式编程的Assignment

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

Your solutions should be submitted as a PDF ﬁle. 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 deﬁned as follows.

(Note that n and c are variables while m stands for a number or its Church encoding.)

L0

0 = n

L0

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

L0

m[times/c, 1/n] !⇤

! m!

and hence that

Lm times 1 !⇤

! m!

where m! means the factorial of m.