Transformación CPS

Hace algún tiempo hablamos de las continuaciones. Además, dimos una semántica operacional para ellas. Ahora vamos a describir cómo se transforma un programa para que use continuaciones en todas sus llamadas a función. Esto es el estilo de paso de continuaciones (CPS) que permite eliminar la necesidad de usar una pila de llamadas. Es decir, la cadena dinámica.

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\ ])$]

La transformación auxiliar es bien sencilla: si no es una función no hace nada, si es una función le añade el argumento de la continuación y transforma su cuerpo.

• 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\ ] $]

Finalmente, si lo que tenemos es una aplicación, vamos calculando su operador y argumentos hasta que, al final, podamos llamar a la función.

• 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)\ ]\ ...\ ]\ ] $]

Va a ser muy habitual encontrarnos con transformaciones anidadas del tipo [$...T[\ e\mid\lambda x.T[...$] ya que representan una secuencia de operaciones. El resultado de [$e$] se pasa a la continuación que empieza por [$\lambda x...$] lo que hace guardar el resultado de [$e$] en [$x$] y proseguir con la ejecución de la secuencia. Para facilitar la comprensión de una expresión en CPS vamos a poner como subíndice de una variable la expresión cuyo valor guarda.

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.

1. Inicial: [$T[\ f(g(a)) \mid k\ ]$]
2. Regla P-TS: [$ T[\ f \mid \lambda x_f.T[\ g(a) \mid \lambda x_{g(a)}. x_f(k, x_{g(a)})\ ]\ ] $]
3. Regla P-TV: [$ (\lambda x_f.T[\ g(a) \mid \lambda x_{g(a)}. x_f(k, x_{g(a)})\ ]\ )(M[\ f\ ]) $]
4. Regla P-MV: [$ (\lambda x_f.T[\ g(a) \mid \lambda x_{g(a)}  . x_f(k, x_{g(a)})\ ]\ )(f) $]  
5. 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) $]  
6. 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) $]
7. 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) $]
8. 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) $]
9. 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) $]

 El resultado de esta expresión es sorprendentemente complejo. Además, parece que podríamos usar varias veces la regla beta para reducir un poco más la expresión.

1. 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) $]
2. Regla beta: [$ (\lambda x_g.  (\lambda x_a. x_g( \lambda x_{g(a)}. f(k, x_{g(a)}) , x_a) )(a) )(g) $]
3. Regla beta: [$ (\lambda x_a. g( \lambda x_{g(a)}. f(k, x_{g(a)}) , x_a) )(a) $]
4. Regla beta: [$ g( \lambda x_{g(a)}. f(k, x_{g(a)}) , a) $]

Esto sí se parece a lo que teníamos inicialmente, el problema es que no podemos realizar reglas beta ya que estamos transformando código y ¿cómo sabemos qué lambdas son del código y qué lambdas son las introducidas por la transformación?

¡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)\ ]\ ...\ ]\ ] $]

El problema es que las [$\bar\lambda$] no son código, son funciones sobre el código (de ahí lo de alto nivel). Si dejáramos las cosas así obtendríamos
[$$ 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\ ] $]  

El truco está en que [$\bar\lambda x_0.x x_0$] convierte el código [$x$] en una función que toma código [$x_0$] y devuelve código [$x x_0$]. Como [$x$] va a ser la continuación, el efecto es pasarle [$x_0$] a la continuación. Justo lo que teníamos antes pero, esta vez, el [$\bar\lambda$] significa que estoy trabajando con funciones sobre código y no sobre código. Podré usar la regla beta para simplificarlas. Lo que buscábamos a la hora de etiquetar.

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)\ ]\ ...\ ]\ ] $]

El truco de [$\lambda x.kx$] es que [$k$] es una función de código que tomará el código [$x$] y generará otro código que permanece dentro del cuerpo de [$\lambda x$]. El resultado es, por tanto, código. Para dejar claro qué variables son de código y qué variables son funciones sobre el código, también etiquetaremos estas últimas que incluirán ahora todas las continuaciones tambié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 $]

Mejoran mucho el resultado de la transformación a CPS. El único inconveniente es que debemos trabajar con funciones sobre código (de alto nivel). Así que, si [$k$] sin etiquetar es código, no puedo escribir
[$$ 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\ ]\ ] $]

La selección duplica el código que hay en la continuación porque lo usa en dos sitios. Esto puede dar lugar a un código final más grande de lo deseable. La solución es postergar a tiempo de ejecución el paso de la continuación de la siguiente forma:

• 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) $]  

La clásica función call/cc se implementa así.

• 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))) $]

Los let se pueden implementar como lambdas aplicados inmediatamente, pero los letrec, no. Asumimos que los letrec sólo pueden vincular valores. Entonces:

• 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\ ] $]

Referencias

Matt Might - How to compile with continuations
Mark Feeley - The 90 minute Scheme to C compiler