Semántica operacional de continuaciones

He encontrado una semántica operacional para las continuaciones que es muy simple de entender.

Sintaxis

Su sintaxis es la siguiente:


[$$ t::= x \mid \lambda x.t \mid tt \mid callcc \mid \#e $$]

Esto quiere decir que un término será o bien una variable, o bien una abstracción lambda, o bien una aplicación de un término sobre otro, o bien una llamada a call/cc o bien una continuación (con el [$ \# $] delante).

Como se observa, las continuaciones hacen uso de una nueva categoría sintáctica [$ e $]. Esta es la categoría de los términos con hueco. Debido a que vamos a evaluar primero el operador y luego el operando, en la última aplicación de esta categoría requerimos un valor a la izquierda.


[$$ e::= [] \mid et \mid ve $$]

Los valores son los ya conocidos más una continuación.

[$$ v::= \lambda x.t \mid x v_1 ... v_n \mid \#e $$]

Así que, en el fondo, una continuación no es más que una expresión con un hueco. Ese hueco hay que rellenarlo cuando utilicemos la continuación. Para eso hemos de definir primero la semántica.

Semántica

Esta semántica hace uso de los propios términos con hueco. Cuando escribimos [$ e[t] $] lo que queremos decir es un término con hueco [$ e $] rellenado el hueco con el término [$ t $]. En este caso, la regla β queda así:

[$$ e[(\lambda x.t)v] \rightarrow e[ [x \mapsto v] t] $$]

Que no es más que decir: allá donde haya una aplicación de una abstracción sobre un valor, sustitúyela por el término de la aplicación cambiando la variable ligada por el valor. Esta regla es usual en el lambda cálculo, aunque dentro de un término con hueco hecho explícito, así que no comentaré nada más.

El meollo del asunto está en modificar ese término con hueco y para eso usamos call/cc y la continuación.

[$$ e[callcc\ t] \rightarrow e[t (\#e)] $$]
[$$ e[(\#e') v] \rightarrow e'[v] $$]

Lo que hace call/cc es recordar el término con hueco, guardándolo en la continuación. Lo que hace la continuación es volver a ese término con hueco.

Ejemplo

De esta manera, usando las continuaciones, se pueden implementar las sentencias de control que queramos. Por ejemplo, un bucle, si suponemos que tenemos secuencia, variables y condicionales.

[$$ n=0;\ k=callcc\ (\lambda x. x)\ ;\ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \} $$]

Evalúo [$ n=0 $]. Ahora [$ n $] vale [$ 0 $].

[$$ k=callcc\ (\lambda x. x)\ ;\ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \} $$]

Evalúo [$ callcc $]. Es un paso importante porque todo lo que hay alrededor del call/cc pasa a ser la continuación.

[$$ k\ =\ (\lambda x. x)\ (\#\ []\ ;\ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \} )\ ;\ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \} $$]

Evalúo la aplicación de la abstracción lambda con la continuación. Es muy fácil porque es la función identidad por lo que el resultado es la propia continuación.

[$$ k\ =\ (\#\ []\ ;\ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \}\ )\ ;\ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \} $$]

Ahora [$ k $] vale la continuación  [$ \#\ []\ ;\ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \} $].

[$$ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \} $$]

Evalúo el [$ if $] que, al ser cierto, es igual a evaluar su cuerpo.

[$$ print\ n\ ;\ n=n+1\ ;\ k\ 0 $$]

Como [$ n $] valía [$ 0 $], imprimimos un cero.


[$$ n=n+1\ ;\ k\ 0 $$]

Y [$ n $] vale [$ 1 $]

[$$ k\ 0 $$]

Ahora empieza el baile. Debido a que [$ k $] vale la continuación  [$ \#\ []\ ;\ if\ n<5\ \{\ print\ n\ ;\ n=n+1\ ;\ k\ 0\ \} $], evaluamos a:

[$$ (\#\ []\ ;\ if\ n<5\ \{\ print\ n\ ;\ k\ 0\ \})\ 0 $$]

Aplicar la continuación es sustituir toda la expresión por la continuación sustituyendo el hueco por el operando evaluado (ya lo está, es el cero).

[$$ 0\ ;\ if\ n<5\ \{\ print\ n\ ;\ k\ 0\ \} $$]

El cero se ignora en la secuencia y repetimos el bucle con [$ n $] igual a [$ 1 $]. Obviamente, cuando sea [$ 5 $], el cuerpo del [$ if $] no se ejecutará y terminaremos el programa.