Dar un término de cálculo Lambda para una función Haskell

Question

Estoy trabajando en un proyecto más grande traduciendo Haskell a Lambda calculus. Me gustaría dar un término lambda a funciones específicas de Haskell . No estoy muy seguro de cómo abordar dos de ellos. Me adelanté y creé la propiedad que debe tener cada término, sólo para dar una idea de lo que estoy tratando de hacer.

¿Qué haría el $\lambda$ -para estas funciones Haskell? Si pudieras dar una breve explicación sería muy útil.

Función 1: $\mathsf{foldr}$ : Debe tener la propiedad

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

Función 2: $\mathsf{map}$ : Debe tener la propiedad

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

Answer 1

Dado que una lista $[N_1, \dots, N_k]$ de $\lambda$ -está representado por el $\lambda$ -término $$\lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots ))$$ es fácil definir el $\lambda$ -términos $\mathsf{foldr}$ y $\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 ))$ . En este caso, la intuición es llevar $\lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots ))$ (es decir, la lista $[N_1, \dots, N_k]$ ) en "posición de cabeza" y aplicarlo a $f$ y luego a $u$ para que, cuando el $\beta$ -pasa a destruir $\lambda c$ y $\lambda n$ , $f$ sustitutos de $c$ y $u$ sustitutos de $n$ . Que $\lambda$ -término $\mathsf{foldr}$ nos permite hacer eso?

¡! Dejemos que $\mathsf{foldr} = \lambda f'. \lambda u'. \lambda l. lf'u'$ . Entonces, \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]$ . Aquí la idea es una variante del punto anterior: llevar $\lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots ))$ (es decir, la lista $[N_1, \dots, N_k]$ ) en "posición de cabeza" y luego reemplazar cada $N_i$ con $f N_i$ con el fin de obtener $\lambda c. \lambda n. c (fN_1) (c (fN_2) ( \dots(c (f N_k) n) \dots ))$ es decir, la lista $[f N_1, \dots, f N_k]$ . ¿Cómo puede cada $N_i$ ser sustituido por $f N_i$ ? El $\lambda$ -término $\lambda c. \lambda n. c N_1 (c N_2( \dots(c N_k n) \dots ))$ (es decir, la lista $[N_1, \dots, N_k]$ ) debe aplicarse al $\lambda$ -término $\lambda x . c (fx)$ para que, cuando el $\beta$ -paso destruye $\lambda c$ en la lista, $\lambda x. c (f x)$ sustitutos de $c$ y luego $(\lambda x. c (f x))N_i \to_\beta c (f N_i)$ . Resumiendo, que $\lambda$ -término $\mathsf{map}$ nos permite hacer todo eso?

¡! Dejemos que $\mathsf{map} = \lambda f'. \lambda l. \lambda c. l \, \lambda x. c (f'x)$ . Entonces, \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}