Denote the terms for the corresponding church numerals

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 2 (10%): The term cons appends an element to the front of a list.

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

and hence that

foldr should have the property that

foldr f u [N1, . . . , Nk] →∗βf N1 (f N2 (. . . (f Nku)))

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.

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

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 .