La máquina SECD es una máquina abstracta , un intérprete de expresiones del cálculo λ . Utiliza cuatro pilas: S ( ing. pila ) - una pila de objetos para calcular expresiones recursivas, E ( ing. entorno ) - contexto (asignación de identificadores a objetos), C ( ing. lista de control ) - línea de control (lista de control), D ( dump ) es un volcado, un almacenamiento de estados anteriores que se usa para regresar de una llamada de función.
Intérprete propuesto en 1964 por Peter Landinen el artículo "The Mechanical Evaluation of Expressions" (evaluación mecánica de expresiones) [1] . La máquina SECD ha formado la base de muchas implementaciones prácticas de lenguajes de programación funcionales (tanto evaluación ansiosa como perezosa ), aunque aún necesita ser optimizada. [2]
En cualquier momento, la máquina SECD tiene un estado representado como una tupla de cuatro pilas, y su funcionamiento puede describirse mediante una función de transición de un estado a otro.
Inicialmente, el contexto E, la pila S y el volcado D están vacíos y la expresión que se va a evaluar se carga como un solo elemento de C, que se convierte a la notación polaca inversa durante la evaluación. La única operación utilizada en este caso es application , denotada por el símbolo ap (del inglés apply - apply). Por ejemplo, la expresión f (gx) (el único elemento de la lista) se reemplaza por la lista [x, g, ap, F, ap].
El cálculo de C se realiza según la lógica polaca inversa. Si el primer elemento en C es un valor, se coloca en la pila S. Más precisamente, si el elemento es un identificador, el valor será el enlace para ese identificador en el contexto actual E. Si el elemento es una abstracción λ , para preservar sus enlaces de variables libres(que están en E) se forma un cierre y se empuja sobre la pila S.
Si el elemento de C es ap (aplicación), se extraen dos valores de la pila y el primero se aplica al segundo. Si el resultado de la aplicación es un valor, se coloca en la pila S.
Sin embargo, si la aplicación es una abstracción λ de un valor, esto dará como resultado una expresión de cálculo lambda que puede ser en sí misma una aplicación (en lugar de un valor) y, por lo tanto, no se puede colocar en la pila. En este caso, los contenidos actuales de S, E y C se vuelcan en D (que es una pila de estos triples), S se vacía y C se reinicializa para el resultado de la aplicación, y E recibe un contexto para las variables libres de esta expresión, complete con los enlaces resultantes de las aplicaciones. Los cálculos continúan como arriba.
El signo de finalización de los cálculos intermedios es la pila vacía C. En este caso, el resultado estará en la pila S. En este caso, el último estado guardado de los cálculos se recupera de la pila D y se coloca en las pilas correspondientes. . El cálculo continúa como arriba.
Si C y D están vacíos, la evaluación termina con el resultado en la pila S.