Give Lambda Calculus Term for Haskell Function

Question

I am working on a larger project translating Haskell to Lambda calculus. I would like to give a lambda term to specific Haskell functions. I am not quite sure how to approach two of them. I went ahead and created the property each term should have, just to give you an idea of what I am trying to do.

What would the $\lambda$-terms for these Haskell functions be? If you could give a brief explanation that would be super helpful.

Function 1: $\mathsf{foldr}$: It should have the property

$$\mathsf{foldr} \, f \, u \, [N_1, \dots ,N_k] \to_\beta^* f N_1 (f N_2 (\dots (f N_k u)))$$

Function 2: $\mathsf{map}$: It should have the property

$$\mathsf{map} \, f \, [N_1, \dots,N_k] \to_\beta^* [f N_1,f N_2, \dots,f N_k]$$

Answer 1

Given that a list $[N_1, \dots, N_k]$ of $\lambda$-terms is represented by the $\lambda$-term $$\lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots ))$$ it is easy to define the $\lambda$-terms $\mathsf{foldr}$ and $\mathsf{map}$.

1. $\mathsf{foldr} \, f \, u \, [N_1, \dots, N_k] \to_\beta^* f N_1 (f N_2( \dots (f N_k u) \dots ))$. Here, the intuition is to bring $\lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots ))$ (i.e. the list $[N_1, \dots, N_k]$) in "head position" and apply it to $f$ and then to $u$, so that, when the $\beta$-steps destroy $\lambda c$ and $\lambda n$, $f$ substitutes for $c$, and $u$ substitutes for $n$. Which $\lambda$-term $\mathsf{foldr}$ allows us to do that?

! Let $\mathsf{foldr} = \lambda f'. \lambda u'. \lambda l. lf'u'$. Then, \begin{align} \mathsf{foldr} \, f \, u \, [N_1, \dots, N_k] &= (\lambda f'. \lambda u'. \lambda l. lf'u') f \, u \, [N_1, \dots, N_k] \\ &\to_\beta (\lambda u'. \lambda l. l f u') \, u \, [N_1, \dots, N_k] \\ &\to_\beta (\lambda l. l f u) [N_1, \dots, N_k] \\ &\to_\beta [N_1, \dots, N_k] \, f \, u \\ &= \big( \lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots )) \big) f u \\ &\to_\beta \big( \lambda n. f N_1 (f N_2( \dots(f N_k n) \dots )) \big) u \\ &\to_\beta f N_1 (f N_2( \dots(f N_k u) \dots )) \end{align}

2. $\mathsf{map} \, f \, [N_1, \dots, N_k] \to_\beta^* [f N_1, \dots, f N_k]$. Here the idea is a variant of the previous point: bring $\lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots ))$ (i.e. the list $[N_1, \dots, N_k]$) in "head position" and then replace each $N_i$ with $f N_i$, so as to obtain $\lambda c. \lambda n. c (fN_1) (c (fN_2) ( \dots(c (f N_k) n) \dots ))$, i.e. the list $[f N_1, \dots, f N_k]$. How can each $N_i$ be replaced by $f N_i$? The $\lambda$-term $\lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots ))$ (i.e. the list $[N_1, \dots, N_k]$) should be applied to the $\lambda$-term $\lambda x . c (fx)$, so that, when the $\beta$-step destroys $\lambda c$ in the list, $\lambda x. c (f x)$ substitutes for $c$ and then $(\lambda x. c (f x))N_i \to_\beta c (f N_i)$. Summing up, which $\lambda$-term $\mathsf{map}$ allows us to do all that?

! Let $\mathsf{map} = \lambda f'. \lambda l. \lambda c. l \, \lambda x. c (f'x)$. Then, \begin{align} \mathsf{map} \, f \, [N_1, \dots, N_k] &= \big( \lambda f'. \lambda l. \lambda c. l \, \lambda x. c (f'x) \big) f \, [N_1, \dots, N_k] \\ &\to_\beta \big( \lambda l. \lambda c. l \, \lambda x. c (f x) \big) [N_1, \dots, N_k] \\ &\to_\beta \lambda c. [N_1, \dots, N_k] \lambda x. c (f x) \\ &= \lambda c. \big( \lambda c'. \lambda n. c' N_1 (c' N_2( \dots(c' N_k n) \dots )) \big) \lambda x.c (f x) \\ &\to_\beta \lambda c. \lambda n. (\lambda x.c (f x)) N_1 ((\lambda x.c (f x)) N_2( \dots( (\lambda x.c (f x)) N_k n) \dots )) \\ &\to_\beta \lambda c. \lambda n. c (f N_1) ((\lambda x.c (f x)) N_2( \dots( (\lambda x.c (f x)) N_k n) \dots )) \\ &\to_\beta \lambda c. \lambda n. c (f N_1) (c (f N_2) ( \dots( (\lambda x.c (f x)) N_k n) \dots )) \\ &\to_\beta^* \lambda c. \lambda n. c (f N_1) (c (f N_2) ( \dots( c (f N_k) n) \dots )) \\ &= [f N_1, \dots, f N_k] \end{align}