En informática teórica , la máquina de Krivine es una máquina abstracta . Como máquina abstracta, comparte características con las máquinas de Turing y la máquina SECD . La máquina de Krivine explica cómo calcular una función recursiva. Más específicamente, pretende definir rigurosamente la reducción de la forma normal de un término lambda mediante la reducción de llamada por nombre . Gracias a su formalismo, explica en detalle cómo funciona un tipo de reducción y establece las bases teóricas de la semántica operacional de los lenguajes de programación funcional . Por otro lado, la máquina de Krivine implementa la llamada por nombre porque evalúa el cuerpo de una β -redex antes de aplicar el cuerpo a su parámetro. En otras palabras, en una expresión ( λ x . t ) u evalúa primero λ x . t antes de aplicarlo a u . En programación funcional , esto significaría que para evaluar una función aplicada a un parámetro, evalúa primero la función antes de aplicarla al parámetro.
La máquina Krivine fue diseñada por el lógico francés Jean-Louis Krivine a principios de la década de 1980.
La máquina de Krivine se basa en dos conceptos relacionados con el cálculo lambda , a saber, la reducción de carga y la llamada por nombre.
Un redex [1] (también se dice β-redex) es un término del cálculo lambda de la forma ( λ x . t ) u . Si un término tiene la forma ( λ x . t ) u 1 ... u n se dice que es un redex de cabeza . Una forma normal de cabeza es un término del cálculo lambda que no es un redex de cabeza. [a] Una reducción de cabeza es una secuencia (no vacía) de contracciones de un término que contrae redexes de cabeza. Una reducción de cabeza de un término t (que se supone que no está en forma normal de cabeza) es una reducción de cabeza que comienza a partir de un término t y termina en una forma normal de cabeza. Desde un punto de vista abstracto, la reducción de cabeza es la forma en que un programa calcula cuando evalúa un subprograma recursivo. Es importante comprender cómo se puede implementar dicha reducción. Uno de los objetivos de la máquina de Krivine es proponer un proceso para reducir un término en forma normal de cabeza y describir formalmente este proceso. Así como Turing utilizó una máquina abstracta para describir formalmente la noción de algoritmo, Krivine utilizó una máquina abstracta para describir formalmente la noción de reducción de la forma normal de la cabeza.
El término (( λ 0) ( λ 0)) ( λ 0) (que corresponde, si se utilizan variables explícitas, al término ( λx . x ) ( λy . y ) ( λz . z )) no está en forma normal de cabeza porque ( λ 0) ( λ 0) se contrae en ( λ 0) dando lugar al redex de cabeza ( λ 0) ( λ 0) que se contrae en ( λ 0) y que es, por tanto, la forma normal de cabeza de (( λ 0) ( λ 0)) ( λ 0). Dicho de otro modo, la contracción de la forma normal de cabeza es:
que corresponde a:
Veremos más adelante cómo la máquina de Krivine reduce el término (( λ 0) ( λ 0)) ( λ 0).
Para implementar la reducción de la cabecera de un término uv que es una aplicación, pero que no es un redex, se debe reducir el cuerpo u para exhibir una abstracción y, por lo tanto, crear un redex con v . Cuando aparece un redex, se lo reduce. Para reducir siempre el cuerpo de una aplicación primero se llama call by name . La máquina Krivine implementa call by name .
La presentación de la máquina de Krivine que se da aquí se basa en notaciones de términos lambda que utilizan índices de Bruijn y supone que los términos de los que calcula las formas normales de cabeza son cerrados . [2] Modifica el estado actual hasta que ya no puede hacerlo más, en cuyo caso obtiene una forma normal de cabeza. Esta forma normal de cabeza representa el resultado del cálculo o produce un error, lo que significa que el término del que partió no es correcto. Sin embargo, puede ingresar en una secuencia infinita de transiciones, lo que significa que el término que intenta reducir no tiene forma normal de cabeza y corresponde a un cálculo no terminal.
Se ha demostrado que la máquina de Krivine implementa correctamente la reducción de la forma normal de la cabeza llamada por nombre en el cálculo lambda. Además, la máquina de Krivine es determinista , ya que cada patrón del estado corresponde a lo sumo a una transición de la máquina.
El Estado tiene tres componentes [2]
El término es un término λ con índices de Bruijn. La pila y el entorno pertenecen a la misma estructura de datos recursiva. Más precisamente, el entorno y la pila son listas de pares <término, entorno> , que se llaman cierres . En lo que sigue, la inserción como cabeza de una lista ℓ (pila o entorno) de un elemento a se escribe a:ℓ , mientras que la lista vacía se escribe □. La pila es el lugar donde la máquina almacena los cierres que deben evaluarse además, mientras que el entorno es la asociación entre los índices y los cierres en un momento dado durante la evaluación. El primer elemento del entorno es el cierre asociado con el índice 0 , el segundo elemento corresponde al cierre asociado con el índice 1 etc. Si la máquina tiene que evaluar un índice, busca allí el par <término, entorno> el cierre que produce el término a evaluar y el entorno en el que este término debe evaluarse. [b] Estas explicaciones intuitivas permiten comprender las reglas de funcionamiento de la máquina. Si se escribe t para término, p para pila, [c] y e para entorno, los estados asociados a estas tres entidades se escribirán t , p, e. Las reglas explican cómo la máquina transforma un estado en otro, después de identificar los patrones entre los estados.
El estado inicial tiene como objetivo evaluar un término t , es el estado t ,□,□, en el que el término es t y la pila y el entorno están vacíos. El estado final (en ausencia de error) es de la forma λ t , □, e, es decir, el término resultante es una abstracción junto con su entorno y una pila vacía.
La máquina Krivine [2] tiene cuatro transiciones: App , Abs , Zero , Succ .
La transición App elimina el parámetro de una aplicación y lo coloca en la pila para una evaluación posterior. La transición Abs elimina el λ del término y saca el cierre de la parte superior de la pila y lo coloca en la parte superior del entorno. Este cierre corresponde al índice de De Bruijn 0 en el nuevo entorno. La transición Zero toma el primer cierre del entorno. El término de este cierre se convierte en el término actual y el entorno de este cierre se convierte en el entorno actual. La transición Succ elimina el primer cierre de la lista de entornos y disminuye el valor del índice.
Evaluamos el término ( λ 0 0) ( λ 0) que corresponde al término ( λ x . x x ) ( λ x . x ). Empecemos con el estado ( λ 0 0) ( λ 0), □, □.
La conclusión es que la forma normal de la cabeza del término ( λ 0 0) ( λ 0) es λ 0. Esto se traduce con variables en: la forma normal de la cabeza del término ( λ x . x x ) ( λ x . x ) es λ x . x .
Evaluemos el término (( λ 0) ( λ 0)) ( λ 0) como se muestra a continuación:
Esto confirma el hecho anterior de que la forma normal del término (( λ 0) ( λ 0)) ( λ 0) es ( λ 0).
La máquina de Krivine, al igual que la máquina CEK , no sólo corresponde funcionalmente a un evaluador metacircular , [3] [4] [5] sino que también corresponde sintácticamente al cálculo -una versión del cálculo de sustituciones explícitas de Pierre-Louis Curien que está cerrado bajo reducción- con una estrategia de reducción de orden normal. [6] [7] [8]
Si el cálculo incluye una reducción generalizada (es decir, el redex anidado se contrae en un paso en lugar de dos), entonces la máquina sintácticamente correspondiente coincide con la máquina original de Jean-Louis Krivine. [9] [7] (Además, si la estrategia de reducción es una llamada de derecha a izquierda por valor e incluye una reducción generalizada, entonces la máquina sintácticamente correspondiente es la máquina abstracta ZINC de Xavier Leroy , que subyace a OCaml ). [10] [7]
El contenido de esta edición se traduce del artículo existente de Wikipedia en francés en fr:Machine de Krivine; consulte su historial para ver la atribución.
Medios relacionados con la máquina Krivine en Wikimedia Commons
