En informática teórica , la máquina Krivine es una máquina abstracta (a veces llamada máquina virtual ). Como máquina abstracta, comparte características con las máquinas de Turing y la máquina SECD . La máquina Krivine explica cómo calcular una función recursiva. Más específicamente, su objetivo es definir rigurosamente la reducción de forma normal de cabeza de un término lambda utilizando la reducción de llamada por nombre . Gracias a su formalismo, cuenta en detalle cómo funciona una especie de reducción y sienta las bases teóricas de la semántica operativa de los lenguajes de programación funcionales.. Por otro lado, la máquina Krivine implementa la llamada por nombre porque evalúa el cuerpo de un β- 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, primero evalúa la función antes de aplicarla al parámetro.
La máquina Krivine ha sido diseñada por el lógico francés Jean-Louis Krivine a principios de los años ochenta.
Llamar por nombre y cabeza reducción de forma normal
La máquina Krivine se basa en dos conceptos relacionados con el cálculo lambda , a saber, reducción de cabeza y llamada por nombre.
Reducción de forma normal de la cabeza
Un redex [1] (se dice también β-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 principal . Una forma normal de la cabeza es un término del cálculo lambda que no es un redex de la cabeza. [a] Una reducción de la cabeza es una secuencia (no vacía) de contracciones de un término que contrae la cabeza que redime. Una reducción de la cabeza de un término t (que se supone que no está en la forma normal de la cabeza) es una reducción de la cabeza que comienza con un término t y termina en una forma normal de la cabeza. Desde un punto de vista abstracto, la reducción de carga 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 Krivine es proponer un proceso para reducir un término en forma normal de cabeza y describir formalmente este proceso. Como Turing usó una máquina abstracta para describir formalmente la noción de algoritmo, Krivine usó una máquina abstracta para describir formalmente la noción de reducción de la forma normal de la cabeza.
Un ejemplo
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 la cabeza normal forma porque ( λ 0) ( λ 0) se contrae en ( λ 0) produciendo la redex de cabeza ( λ 0) ( λ 0) que se contrae en ( λ 0) y que por lo tanto es la forma normal de cabeza de (( λ 0) ( λ 0)) ( λ 0). Dicho lo contrario, la contracción de la forma normal de la cabeza es:
- (( λ 0) ( λ 0)) ( λ 0) ➝ ( λ 0) ( λ 0) ➝ λ 0,
que corresponde a:
- ( λx . x ) ( λy . y ) ( λz . z ) ➝ ( λy . y ) ( λz . z ) ➝ λz . z .
Más adelante veremos cómo la máquina Krivine reduce el término (( λ 0) ( λ 0)) ( λ 0).
Llamar por nombre
Para implementar la reducción de cabeza 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, uno lo reduce. Para reducir siempre el cuerpo de una aplicación primero se llama llamar por nombre . La máquina Krivine implementa la llamada por nombre .
Descripción
La presentación de la máquina Krivine dada aquí se basa en notaciones de términos lambda que usan índices de Bruijn y asume que los términos de los cuales calcula las formas normales principales son cerrados . [2] Modifica el estado actual hasta que no puede hacerlo más, en cuyo caso obtiene una forma normal de cabeza. Esta forma normal principal representa el resultado del cálculo o produce un error, lo que significa que el término con el que comenzó no es correcto. Sin embargo, puede entrar 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 terminante.
Se ha demostrado que la máquina Krivine implementa correctamente la reducción de la forma normal de la llamada por nombre en el cálculo lambda. Además, la máquina Krivine es determinista , ya que cada patrón del estado corresponde como máximo a una transición de máquina.
El estado
El estado tiene tres componentes [2]
- un término ,
- una pila ,
- un medio ambiente .
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
El estado inicial tiene como objetivo evaluar un término t , es el estado t , □, □, en el que el término es ty la pila y el entorno están vacíos. El estado final (en ausencia de error) es de la forma λ t , □, e, en otras palabras, los términos resultantes son una abstracción junto con su entorno y una pila vacía.
Las transiciones
La máquina Krivine [2] tiene cuatro transiciones: App , Abs , Zero , Succ .
Nombre | Antes | Después |
---|---|---|
Aplicación | tu , p, e | t , < u , e>: p, e |
Abdominales | λ t , < u , e '>: p, e | t , p, < u , e '>: e |
Cero | 0 , p, < t , e '>: e | t , p, e ' |
Succ | n + 1 , p, < t, e '>: e | n, p, e |
La aplicación de transición elimina el parámetro de una aplicación y lo coloca en la pila para una evaluación adicional. La transición Abs elimina el λ del término y abre el cierre de la parte superior de la pila y lo coloca en la parte superior del entorno. Este cierre corresponde al índice 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.
Dos ejemplos
Evaluemos el término ( λ 0 0) ( λ 0) que corresponde al término ( λ x . X x ) ( λ x . X ). Comencemos con el estado ( λ 0 0) ( λ 0), □, □.
( λ 0 0) ( λ 0), □, □ |
λ 0 0, [< λ 0, □>], □ |
0 0, □, [< λ 0, □>] |
0, [<0, < λ 0, □ >>], [< λ 0, □>] |
λ 0, [<0, < λ 0, □ >>], □ |
0, □, [<0, < λ 0, □ >>] |
0, □, [< λ 0, □>] |
λ 0 , □, □ |
La conclusión es que la forma normal principal del término ( λ 0 0) ( λ 0) es λ 0. Esto se traduce con variables en: la forma normal principal del término ( λ x . X x ) ( λ x . X ) es λ x . x .
Evaluemos el término (( λ 0) ( λ 0)) ( λ 0) como se muestra a continuación:
(( λ 0) ( λ 0)) ( λ 0), □, □ |
( λ 0) ( λ 0), [<( λ 0), □>], □ |
( λ 0), [<( λ 0), □>, <( λ 0), □>], □ |
0, [<( λ 0), □>], [<( λ 0), □>] |
λ 0, [<( λ 0), □>], □ |
0, □, [<( λ 0), □>] |
( λ 0), □, □ |
Esto confirma el hecho anterior de que la forma normal del término (( λ 0) ( λ 0)) ( λ 0) es ( λ 0).
Ver también
Notas
- ^ Si solo se trata de términos cerrados, estos términos toman la forma λ x . t .
- ^ Utilizando el concepto de cierre, se puede reemplazar el triple
, que define el estado, por un par de érmino,>,> , pero este cambio es cosmético. - ^ p es para pila , la palabra francesa para pila, que no queremos mezclar con s , para estado.
Referencias
- ^ Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics , Studies in Logic and the Foundations of Mathematics, 103 (Ed. Revisada), North Holland, Amsterdam, ISBN 0-444-87508-5, archivado desde el original el 23 de agosto de 2004 Correcciones .
- ^ a b c Curien, Pierre-Louis (1993). Combinadores categóricos, algoritmos secuenciales y funcionales (2ª ed.). Birkhaüser.
El contenido de esta edición está traducido del artículo de Wikipedia en francés existente en fr: Machine de Krivine ; consulte su historial para la atribución.
Bibliografía
- Jean-Louis Krivine: una máquina de cálculo lambda para llamar por nombre . Computación simbólica y de orden superior 20 (3): 199-207 (2007) archivo .
- Curien, Pierre-Louis (1993). Combinadores categóricos, algoritmos secuenciales y funcionales (2ª ed.). Birkhaüser.
- Frédéric Lang: Explicando la máquina Krivine perezosa usando sustituciones explícitas y direcciones . Computación simbólica y de orden superior 20 (3): 257-270 (2007) archivo .
- Olivier Danvy (Ed.): Editorial del número especial de Computación simbólica y de orden superior en la máquina Krivine, vol. 20 (3) (2007)
enlaces externos
- Medios relacionados con la máquina Krivine en Wikimedia Commons