Máquina CEK

Una máquina CEK es una máquina abstracta inventada por Matthias Felleisen y Daniel P. Friedman que implementa la llamada por valor de izquierda a derecha . ^{[ 1 ]} Generalmente se implementa como un intérprete para lenguajes de programación funcional , pero también puede usarse para implementar lenguajes de programación imperativos simples . Un estado en una máquina CEK incluye una instrucción de control, un entorno y una continuación . La instrucción de control es el término que se está evaluando en ese momento, el entorno es (generalmente) un mapa de nombres de variables a valores, y la continuación almacena otro estado o un caso especial de parada. Es una forma simplificada de otra máquina abstracta llamada máquina SECD . ^{[ 2 ] [ 3 ] [ 4 ]}

La máquina CEK se basa en la máquina SECD reemplazando el volcado ( pila de llamadas ) con la continuación más avanzada y colocando los parámetros directamente en el entorno, en lugar de insertarlos primero en la pila de parámetros. Se pueden realizar otras modificaciones que crean toda una familia de máquinas relacionadas. Por ejemplo, la máquina CESK tiene el entorno mapeando las variables a un puntero en el almacenamiento, que es efectivamente un montón. Esto le permite modelar el estado mutable mejor que la máquina CEK ordinaria. La máquina CK no tiene entorno y puede usarse para cálculos simples sin variables. ^{[ 5 ]}

Se puede crear una máquina CEK para cualquier lenguaje de programación, por lo que el término se usa a menudo de forma vaga. Por ejemplo, se podría crear una máquina CEK para interpretar el cálculo lambda . Su entorno asigna variables a cierres y las continuaciones son una parada, una continuación para evaluar un argumento (ar) o una continuación para evaluar una aplicación después de evaluar una función (ap): ^{[ 4 ] [ 6 ]}

En el artículo original ^{[ 7 ]} , los autores describen la máquina CEK utilizando semántica operacional de pasos pequeños sobre el cálculo lambda sin tipado:

${\displaystyle {\begin{aligned}\langle x,{\text{E}},{\text{K}}\rangle &\mapsto \langle \epsilon ,\emptyset ,{\text{ret}}(E[x])\gg {\text{K}}\rangle \\\langle \lambda xM,{\text{E}},{\text{K}}\rangle &\mapsto \langle \epsilon ,\emptyset ,{\text{ret}}((\lambda xM,{\text{E}}))\gg {\text{K}}\rangle \\\langle M\,N,{\text{E}},{\text{K}}\rangle &\mapsto \langle M,{\text{E}},{\text{arg}}(N,{\text{E}})\gg {\text{K}}\rangle \\\langle \epsilon ,\emptyset ,{\text{ret}}(F)\gg {\text{arg}}(N,{\text{E}})\gg {\text{K}}\rangle &\mapsto \langle N,{\text{E}},{\text{app}}(F)\gg K\rangle \quad &F=\lambda xM\\\langle \epsilon ,\emptyset ,{\text{ret}}(V)\gg {\text{app}}(F)\gg {\text{K}}\rangle &\mapsto \langle M,{\text{E}}[x\mapsto V],K\rangle \quad &F=\lambda xM\\\end{aligned}}}$

dónde${\displaystyle \gg }$es una ligadura monádica en las continuaciones,${\displaystyle {\text{E}}[x\mapsto V]}$es un entorno ampliado con un nuevo enlace.

Por ejemplo, el término${\displaystyle (\lambda x.x+1)\,5}$Se evalúa siguiendo los siguientes pasos:

${\displaystyle {\begin{aligned}&\langle (\lambda x.x+1)\,5,{\text{E}},{\text{K}}\rangle \\\mapsto \quad &\langle (\lambda x.x+1),{\text{E}},{\text{arg}}(5,{\text{E}})\gg {\text{K}}\rangle \\\mapsto \quad &\langle \epsilon ,\emptyset ,{\text{ret}}((\lambda x.x+1,{\text{E}}))\gg {\text{arg}}(5,{\text{E}})\gg {\text{K}}\rangle \\\mapsto \quad &\langle 5,{\text{E}},{\text{app}}((\lambda x.x+1,{\text{E}}))\gg {\text{K}}\rangle \\\mapsto \quad &\langle \epsilon ,\emptyset ,{\text{ret}}(5)\gg {\text{app}}((\lambda x.x+1,{\text{E}}))\gg {\text{K}}\rangle \\\mapsto \quad &\langle x+1,{\text{E}}[x\mapsto 5],K\rangle \\\vdots \\\mapsto \quad &\langle \epsilon ,\emptyset ,{\text{ret}}(6)\gg K\rangle \\\end{aligned}}}$

donde el cálculo se extiende a los números y la suma (aunque tanto los números como la suma pueden codificarse completamente en el cálculo lambda).

Cada componente de la máquina CEK tiene diversas representaciones. La cadena de control suele ser un término que se está evaluando o, a veces, un número de línea. Por ejemplo, una máquina CEK que evalúa el cálculo lambda usaría una expresión lambda como cadena de control. El entorno es casi siempre un mapa de variables a valores o, en el caso de las máquinas CESK, de variables a direcciones en la memoria. La representación de la continuación varía. A menudo contiene otro entorno, así como un tipo de continuación, por ejemplo, argumento o aplicación . A veces es una pila de llamadas, donde cada marco es el resto del estado, es decir, una instrucción de control y un entorno.

Existen otras máquinas estrechamente vinculadas a la máquina CEK.

En la página 196 de "Operadores de control, la máquina SECD y la${\displaystyle \lambda }$-Cálculo", ^{[ 10 ]} y en la página 4 del informe técnico del mismo nombre, ^{[ 7 ]} Matthias Felleisen y Daniel P. Friedman escribieron "La máquina [CEK] se deriva del intérprete extendido IV de Reynolds.", refiriéndose al intérprete III de John Reynolds en "Intérpretes definicionales para lenguajes de programación de orden superior". ^{[ 11 ] [ 12 ]}

A saber, aquí hay una implementación de la máquina CEK en OCaml , que representa términos lambda con índices de De Bruijn:

término de tipo = IND de int (* índice de Bruijn *) | ABS de plazo | APP de término * término

Los valores son cierres , tal como los inventó Peter Landin :

tipo valor = CLO del término * lista de valorestipo cont = C2 de término * lista de valores * cont | C1 de valor * cont | C0let rec continue ( c : cont ) ( v : value ) : value = match c , v with C2 ( t1 , e , k ), v0 -> eval t1 e ( C1 ( v0 , k )) | C1 ( v0 , k ), v1 -> apply v0 v1 k | C0 , v -> v and eval ( t : term ) ( e : value list ) ( k : cont ) : value = match t with IND n -> continue k ( List . nth e n ) | ABS t' -> continue k ( CLO ( t' , e )) | APP ( t0 , t1 ) -> eval t0 e ( C2 ( t1 , e , k )) y apply ( v0 : valor ) ( v1 : valor ) ( k : cont ) = let ( CLO ( t , e )) = v0 en eval t ( v1 :: e ) klet main ( t : term ) : value = eval t [] C0

Esta implementación está en forma desfuncionalizada , con conty continue como la representación de primer orden de una continuación. Aquí está su contraparte refuncionalizada:

let rec eval ( t : term ) ( e : value list ) ( k : value -> ' a ) : ' a = match t with IND n -> k ( List . nth e n ) | ABS t' -> k ( CLO ( t' , e )) | APP ( t0 , t1 ) -> eval t0 e ( fun v0 -> eval t1 e ( fun v1 -> apply v0 v1 k )) and apply ( v0 : value ) ( v1 : value ) ( k : value -> ' a ) : ' a = let ( CLO ( t , e )) = v0 in eval t ( v1 :: e ) klet main ( t : term ) : value = eval t [] ( fun v -> v )

Esta implementación sigue un estilo de paso de continuaciones de izquierda a derecha , donde el dominio de las respuestas es polimórfico, es decir, se implementa con una variable de tipo . ^{[ 13 ]} Esta implementación de paso de continuaciones se mapea de nuevo al estilo directo de la siguiente manera:

let rec eval ( t : term ) ( e : value list ) : value = match t with IND n -> List . nth e n | ABS t' -> CLO ( t' , e ) | APP ( t0 , t1 ) -> let v0 = eval t0 e and v1 = eval t1 e in apply v0 v1 and apply ( v0 : value ) ( v1 : value ) : value = let ( CLO ( t , e )) = v0 in eval t ( v1 :: e )let main ( t : term ) : value = eval t []

Esta implementación de estilo directo también se encuentra en forma desfuncionalizada, o más precisamente en forma convertida a cierre. Este es el resultado de desconvertirla a cierre:

tipo valor = FUN de ( valor -> valor )let rec eval ( t : term ) ( e : value list ) : value = match t with IND n -> List . nth e n | ABS t' -> FUN ( fun v -> eval t' ( v :: e )) | APP ( t0 , t1 ) -> let v0 = eval t0 e and v1 = eval t1 e in apply v0 v1 and apply ( v0 : value ) ( v1 : value ) : value = let ( FUN f ) = v0 in f v1let main ( t : term ) : value = eval t []

La implementación resultante es compositiva . Es el auto-intérprete definicional habitual de Scott-Tarski , donde el dominio de valores es reflexivo ( Scott ) y donde las funciones sintácticas se definen como funciones semánticas y las aplicaciones sintácticas se definen como aplicaciones semánticas ( Tarski ).

Esta derivación imita la deconstrucción racional de Danvy de la máquina SECD de Landin . ^{[ 14 ]} La derivación inversa (conversión de cierre, transformación CPS y desfuncionalización) está documentada en el artículo de John Reynolds «Intérpretes definicionales para lenguajes de programación de orden superior», que es el origen de la máquina CEK y posteriormente se identificó como un modelo para transformar evaluadores compositivos en máquinas abstractas y viceversa. ^{[ 11 ] [ 15 ]}

La máquina CEK, al igual que la máquina Krivine , no solo se corresponde funcionalmente con un evaluador metacircular (a través de una transformación CPS de llamada por valor de izquierda a derecha), ^{[ 15 ]} también se corresponde sintácticamente con el${\displaystyle \lambda {\widehat {\rho }}}$cálculo — un cálculo que utiliza sustitución explícita — con una estrategia de reducción de orden aplicativo de izquierda a derecha, ^{[ 16 ] [ 17 ]} y de igual manera para la máquina SECD (a través de una transformación CPS de llamada por valor de derecha a izquierda). ^{[ 18 ]}