Give Lambda Calculus Term for Haskell Function 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]$$
 A: 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}$.

*

*$\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}



*$\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}

