El estilo de paso de continuaciones (CPS)
Para empezar, veamos cómo es eso del CPS. Supongamos la siguiente expresión.
[$$ f(g(a)) $$]
Lo primero que calculamos es el valor de [$a$]. Luego, el valor de [$g(a)$] y, finalmente, el valor de [$f(g(a))$]. El estilo CPS añade un argumento adicional a cada función que es la continuación, a la que le pasaremos el resultado cuando la función termine.
¿A dónde pasábamos el resultado de [$g(a)$]? A [$f$]. Así que, al hacer [$g$] CPS, la expresión de arriba queda
[$$ g(f, a) $$]
y se leería algo así como "calcula [$g(a)$] y pásale el resultado a [$f$]. El problema es que también tenemos que hacer CPS a [$f$] por lo que ahora [$f$] no toma un argumento, toma dos: la continuación y su argumento propiamente dicho. La solución es añadir una función anónima. La expresión de arriba con tanto [$g$] como [$f$] puestas en CPS sería así:
[$$g(\lambda x.f(k,x), a)$$]
El detalle es que [$k$] es la continuación de la expresión, que no sabemos cuál es porque no he dicho qué vamos a hacer después de calcular [$f(g(a))$]. Para destacar claramente que [$k$] es la continuación, que [$f(g(a))$] es la expresión original y que [$g(\lambda x.f(k,x), a)$] es la expresión transformada a CPS, vamos a usar la siguiente notación:
[$$ T\ [\ f(g(a))\mid k\ ]\ = g(\lambda x.f(k,x), a) $$]
La transformación de Plotkin
Bastará conocer las reglas de la transformación [$ T\ [\ ]$] para poder realizarla. Esto es a lo que se dedicó Plotkin en 1975 en el artículo "Call-by-name, call-by-value and the [$\lambda$]-calculus", aunque ha llovido mucho y la versión que presento aquí es bastante distinta a la original.
Lo primero que necesitamos es definir el lenguaje que vamos a transformar. Vamos a usar una variante del lambda cálculo sin currificar. Es muy sencilla: un valor es o bien una variable o bien una función anónima.
[$$ v::= x \mid \lambda (x_1,...,x_n).e $$]
Una expresión es o bien un valor o bien una aplicación (llamo [$s$] a las aplicaciones).
[$$ e::= v \mid s $$]
También llamaremos, [$k$] a una expresión. Una aplicación no es más que una llamada a función.
[$$ s::= e_0 (e_1,...,e_n) $$]
Para transformar un programa escrito con esta sintaxis hemos de dar la transformación para cada una de estas construcciones sintácticas. Si lo que tengo un valor, ya está calculado, sólo he de pasarlo a la continuación. ¡Pero ojo! Si es una función he de transformarla antes en CPS. De esto se va a encargar la transformación auxiliar [$ M[\ ]$].
- Regla P-TV: [$ T\ [\ v\mid k\ ]= k(M[\ v\ ])$]
- Regla P-MX: [$ M\ [\ x\ ]=x $]
- Regla P-ML: [$ M\ [\ \lambda(x_1,...,x_n).e\ ]=\lambda(x,x_1,...,x_n).T[\ e\mid x\ ] $]
- Regla P-TS: [$ T\ [\ e_0(e_1,...,e_n) \mid k\ ]=T[\ e_0 \mid \lambda x_0.T[\ e_1 \mid \lambda x_1.\ ...T[\ e_n \mid \lambda x_n. x_0(k, x_1,...,x_n)\ ]\ ...\ ]\ ] $]
Bien, ahora que tenemos las cuatro reglas de Plotkin vamos a probar a ver cómo transforma a [$f(g(a))$]. Vamos a hacerlo paso a paso.
- Inicial: [$T[\ f(g(a)) \mid k\ ]$]
- Regla P-TS: [$ T[\ f \mid \lambda x_f.T[\ g(a) \mid \lambda x_{g(a)}. x_f(k, x_{g(a)})\ ]\ ] $]
- Regla P-TV: [$ (\lambda x_f.T[\ g(a) \mid \lambda x_{g(a)}. x_f(k, x_{g(a)})\ ]\ )(M[\ f\ ]) $]
- Regla P-MV: [$ (\lambda x_f.T[\ g(a) \mid \lambda x_{g(a)} . x_f(k, x_{g(a)})\ ]\ )(f) $]
- Regla P-TS: [$ (\lambda x_f.T[g \mid \lambda x_g.T[\ a \mid \lambda x_a. x_g( \lambda x_1. x_f(k, x_{g(a)}) , x_a)\ ]\ ]\ )(f) $]
- Regla P-TV: [$ (\lambda x_f. (\lambda x_g.T[\ a \mid \lambda x_a. x_g( \lambda x_{g(a)}. x_f(k, x_{g(a)}) , x_a)\ ]\ )(M[\ g\ ]) )(f) $]
- Regla P-MV: [$ (\lambda x_f. (\lambda x_g.T[\ a \mid \lambda x_a. x_g( \lambda x_{g(a)}. x_f(k, x_{g(a)}) , x_a)\ ]\ )(g) )(f) $]
- Regla P-TV: [$ (\lambda x_f. (\lambda x_g. (\lambda x_a. x_g( \lambda x_{g(a)}. x_f(k, x_{g(a)}) , x_a) )(M[\ a\ ]\ ) )(g) )(f) $]
- Regla P-MV: [$ (\lambda x_f. (\lambda x_g. (\lambda x_a. x_g( \lambda x_{g(a)}. x_f(k, x_{g(a)}) , x_a) )(a) )(g) )(f) $]
- Del anterior: [$ (\lambda x_f. (\lambda x_g. (\lambda x_a. x_g( \lambda x_{g(a)}. x_f(k, x_{g(a)}) , x_a) )(a) )(g) )(f) $]
- Regla beta: [$ (\lambda x_g. (\lambda x_a. x_g( \lambda x_{g(a)}. f(k, x_{g(a)}) , x_a) )(a) )(g) $]
- Regla beta: [$ (\lambda x_a. g( \lambda x_{g(a)}. f(k, x_{g(a)}) , x_a) )(a) $]
- Regla beta: [$ g( \lambda x_{g(a)}. f(k, x_{g(a)}) , a) $]
¡Ah!... Se me ocurre una idea. Podríamos etiquetarlas...
Nota: ¿Por qué no podemos realizar reglas beta en el código? Imaginemos la siguiente expresión [$(\lambda x.3)(f(x))$]. Si [$f(x)$] tiene efectos secundarios, al realizar la regla beta obtendríamos [$3$] y habríamos perdido los efectos secundarios.
La tranformación de alto nivel de Appel
Esta fue la idea que se le ocurrió a Appel en 1992 para su libro "Compiling with Continuations", pero no es tan sencilla. En primer lugar estaríamos tentados a etiquetar (con una rayita encima) las lambda que fueran introducidas por la transformación a CPS. Empecemos por la regla que las introduce: la P-TS que renombraremos a A-TS.
- Regla A-TS: [$ T\ [\ e_0(e_1,...,e_n) \mid k\ ]=$][$T[\ e_0 \mid \bar\lambda x_0.T[\ e_1 \mid \bar\lambda x_1.\ ...T[\ e_n \mid \bar\lambda x_n. x_0(k, x_1,...,x_n)\ ]\ ...\ ]\ ] $]
[$$ T[\ f(a)(b)\ ]=f(\bar\lambda x_{f(a)}.x_{f(a)}(k,b), a) $$]
Y eso no es código. No es código porque contiene un [$\bar\lambda$] que es una función sobre el código. No está en la sintaxis que pusimos al inicio.
La solución se obtiene forzando que las continuaciones se especifiquen siempre de forma indirecta, como una función sobre el código. En ese aspecto, cambiamos la regla P-ML de la siguiente forma (la nueva regla es la A-ML):
- Regla P-ML: [$ M\ [\ \lambda(x_1,...,x_n).e\ ]=\lambda(x,x_1,...,x_n).T[\ e\mid x\ ] $]
- Regla A-ML: [$ M\ [\ \lambda(x_1,...,x_n).e\ ]=\lambda(x,x_1,...,x_n).T[\ e\mid \bar\lambda x_0.x x_0\ ] $]
También hay que trastear la regla A-TS porque [$k$] no es código.
- Regla P-TS: [$ T\ [\ e_0(e_1,...,e_n) \mid k\ ]= $][$ T[\ e_0 \mid \lambda x_0.T[\ e_1 \mid \lambda x_1.\ ...T[\ e_n \mid \lambda x_n. x_0(k, x_1,...,x_n)\ ]\ ...\ ]\ ] $]
- Regla A-TS antigua (etiqueto lambdas): [$ T\ [\ e_0(e_1,...,e_n) \mid k\ ]= $][$ T[\ e_0 \mid \bar\lambda x_0.T[\ e_1 \mid \bar\lambda x_1.\ ...T[\ e_n \mid \bar \lambda x_n. x_0(k, x_1,...,x_n)\ ]\ ...\ ]\ ] $]
- Regla A-TS nueva (arreglo [$k$]): [$ T\ [\ e_0(e_1,...,e_n) \mid k\ ]= $][$ T[\ e_0 \mid \bar\lambda x_0.T[\ e_1 \mid \bar\lambda x_1.\ ...T[\ e_n \mid \bar \lambda x_n. x_0(\lambda x.k x, x_1,...,x_n)\ ]\ ...\ ]\ ] $]
Entonces, las reglas de transformación de alto nivel definitivas son las siguientes:
- Regla A-MX: [$ M\ [\ x\ ]=x $]
- Regla A-ML: [$ M\ [\ \lambda(x_1,...,x_n).e\ ]=\lambda(x,x_1,...,x_n).T[\ e\mid \bar\lambda x_0.x x_0 \ ] $]
- Regla A-TV: [$ T\ [\ v\mid \bar k\ ]= k(M[\ v\ ])$]
- Regla A-TS: [$ T\ [\ e_0(e_1,...,e_n) \mid \bar k\ ]=$][$T[\ e_0 \mid \bar\lambda x_0.T[\ e_1 \mid \bar\lambda x_1.\ ...T[\ e_n \mid \bar\lambda x_n. x_0(\lambda x.\bar k x, x_1,...,x_n)\ ]\ ...\ ]\ ] $]
- Regla beta: [$ (\bar\lambda (x_1,...x_n). e) (v_1,...,v_n) = [x_1 \rightarrow v_1,..., x_n \rightarrow v_n ]e $]
[$$ T[\ f(a)\mid k\ ]$$]
Tengo que escribir
[$$ T[\ f(a)\mid \bar\lambda x.k x\ ]$$]
y el resultado de esto no es todo lo perfecto que quisiéramos:
[$$ f( \lambda x.k x, a) $$]
Se me ocurre otra idea... ¿Y no podemos mezclar las reglas de Plotkin y de Appel para usar código o funciones sobre código cuando queramos?
La tranformación CPS híbrida
Separemos entonces [$T\ [\ ]$] en dos: una sin etiqueta y otra con etiqueta [$\bar T\ [\ ]$]. La versión sin etiqueta requiere que la continuación sea código [$T\ [\ e\mid k\ ]$] y la etiquetada requiere que sea una función sobre código [$\bar T\ [\ e\mid \bar k\ ]$]. La mezcla es sencilla.
- Regla H-MX: [$ M\ [\ x\ ]=x $]
- Regla H-ML: [$ M\ [\ \lambda(x_1,...,x_n).e\ ]=\lambda(x,x_1,...,x_n).T[\ e\mid x \ ] $]
- Regla H-TV: [$ T\ [\ v\mid k\ ]= k(M[\ v\ ])$]
- Regla H-TS: [$ T\ [\ e_0(e_1,...,e_n) \mid k\ ]=$][$\bar T[\ e_0 \mid \bar\lambda x_0. \bar T[\ e_1 \mid \bar\lambda x_1.\ ... \bar T[\ e_n \mid \bar\lambda x_n. x_0(k, x_1,...,x_n)\ ]\ ...\ ]\ ] $]
- Regla H-FV: [$ \bar T\ [\ v\mid \bar k\ ]= \bar k(M[\ v\ ])$]
- Regla H-FS: [$ \bar T\ [\ e_0(e_1,...,e_n) \mid \bar k\ ]=$] [$\bar T[\ e_0 \mid \bar\lambda x_0. \bar T[\ e_1 \mid \bar\lambda x_1.\ ... \bar T[\ e_n \mid \bar\lambda x_n. x_0(\lambda x.\bar k x, x_1,...,x_n)\ ]\ ...\ ]\ ] $]
- Regla beta: [$ (\bar\lambda (x_1,...x_n). e) (v_1,...,v_n) = [x_1 \rightarrow v_1,..., x_n \rightarrow v_n ]e $]
Con estas reglas sí que conseguimos el objetivo deseado.
[$$ T\ [\ f(a)\mid k\ ]\ = f(k,a)$$]
[$$ T\ [\ f(g(a))\mid k\ ]\ = g(\lambda x.f(k,x), a) $$]
El único problemilla que tenemos es que trabajamos como en dos fases. En la primera fase quitamos las [$T$] (y [$\bar T$]) de en medio y en la segunda fase quitamos las [$\bar \lambda$] con la regla beta. Es posible hacerlo todo a la vez, pero aumenta lo suficiente la complejidad como para no explicarlo aquí (se basa en separar las [$e$] en [$v$] y en [$s$] y tratar cada caso con una regla distinta, específica).
Transformación CPS para lenguajes reales
Para finalizar vamos a apuntar brevemente cómo son las reglas de transformación CPS para un lenguaje de programación real, con asignación, selección, secuencia y demás primitivas.
- AsignaciónT: [$ T\ [\ \mathrm{set}\ x\ e \mid k\ ]=\bar T[ e \mid \bar\lambda x_0. k ( \mathrm{set}\ x\ e)\ ] $]
- AsignaciónF: [$ \bar T\ [\ \mathrm{set}\ x\ e \mid \bar k\ ]=\bar T[ e \mid \bar\lambda x_0. \bar k ( \mathrm{set}\ x\ e)\ ] $]
- SelecciónT: [$ T\ [\ \mathrm{if}\ e_1\ e_2\ e_3 \mid k\ ]=\bar T[\ e_1 \mid \bar\lambda x_1. ( \mathrm{if}\ x_1\ T[\ e_2 \mid k\ ]\ T[\ e_3 \mid k\ ]\ ] $]
- SelecciónF: [$ \bar T\ [\ \mathrm{if}\ e_1\ e_2\ e_3 \mid \bar k\ ]=\bar T[\ e_1 \mid \bar\lambda x_1. ( \mathrm{if}\ x_1\ \bar T[\ e_2 \mid \bar k\ ]\ \bar T[\ e_3 \mid \bar k\ ]\ ] $]
- SecuenciaT: [$ T\ [\ e_1 ; e_2 \mid k \ ]= \bar T[\ e_1 \mid \bar\lambda x.T[\ e_2 \mid k\ ]\ ] $]
- SecuenciaF: [$ \bar T\ [\ e_1 ; e_2 \mid \bar k \ ]= \bar T[\ e_1 \mid \bar\lambda x. \bar T[\ e_2 \mid \bar k\ ]\ ] $]
- SelecciónT2: [$ T\ [\ \mathrm{if}\ e_1\ e_2\ e_3 \mid k\ ]=(\lambda x. \bar T[\ e_1 \mid \bar\lambda x_1. ( \mathrm{if}\ x_1\ T[\ e_2 \mid k\ ]\ T[\ e_3 \mid x\ ]\ ])(k) $]
- SelecciónF2: [$ \bar T\ [\ \mathrm{if}\ e_1\ e_2\ e_3 \mid \bar k\ ]=(\lambda x. \bar T[\ e_1 \mid \bar\lambda x_1. ( \mathrm{if}\ x_1\ \bar T[\ e_2 \mid \bar x\ ]\ \bar T[\ e_3 \mid \bar k\ ]\ ])(\lambda x_0.\bar k x_0) $]
- CallCCT: [$ T\ [\ \mathrm{calcc}\ | k\ ] = k (\lambda(x_0,x_1).x_1(x_0,\lambda(x_2,x_3).x_0(x_3))) $]
- CallCCF: [$ \bar T\ [\ \mathrm{calcc} \ | \bar k\ ] = \bar k (\lambda(x_0,x_1).x_1(x_0,\lambda(x_2,x_3).x_0(x_3))) $]
- LetRecT: [$ T\ [\ \mathrm{letrec}\ x_1=v_1,...,x_n=v_n\ \mathrm{in}\ e \mid k\ ]=$][$\mathrm{letrec}\ x_1=M[\ v_1\ ],...,x_n=M[\ v_n\ ]\ \mathrm{in}\ T[\ e \mid k\ ] $]
- LetRecF: [$ \bar T\ [\ \mathrm{letrec}\ x_1=v_1,...,x_n=v_n\ \mathrm{in}\ e \mid \bar k\ ]=$][$\mathrm{letrec}\ x_1=M[\ v_1\ ],...,x_n=M[\ v_n\ ]\ \mathrm{in}\ \bar T[\ e \mid \bar k\ ] $]
Matt Might - How to compile with continuations
Mark Feeley - The 90 minute Scheme to C compiler