En el cálculo lambda , un término está en forma beta normal si no es posible una reducción beta . [1] Un término está en forma beta-eta normal si no es posible una reducción beta ni una reducción eta . Un término está en forma normal de cabeza si no hay beta-redex en la posición de cabeza .
Reducción beta
En el cálculo lambda, un beta redex es un término de la forma:
- .
Un redex está en posición de cabeza en un término, Si tiene la siguiente forma (tenga en cuenta que la aplicación tiene mayor prioridad que la abstracción, y que la fórmula a continuación está destinada a ser una abstracción lambda, no una aplicación):
- , dónde y .
Una reducción beta es una aplicación de la siguiente regla de reescritura a un redex beta contenido en un término:
dónde es el resultado de sustituir el término para la variable en el plazo .
Una reducción beta de la cabeza es una reducción beta aplicada en la posición de la cabeza, es decir, de la siguiente forma:
- , dónde y .
Cualquier otra reducción es una reducción beta interna .
Una forma normal es un término que no contiene ninguna beta redex, es decir , que no se puede reducir más. Una forma normal de la cabeza es un término que no contiene una beta redex en la posición de la cabeza, es decir , que no puede reducirse más mediante una reducción de la cabeza. Cuando se considera el cálculo lambda simple (es decir, sin la adición de símbolos de función o constante, que se pretende reducir mediante una regla delta adicional), las formas normales de la cabeza son los términos de la siguiente forma:
- , dónde es una variable, y .
Una forma normal principal no siempre es una forma normal, porque los argumentos aplicados no tiene por qué ser normal. Sin embargo, lo contrario es cierto: cualquier forma normal es también una forma normal de cabeza. De hecho, las formas normales son exactamente las formas normales principales en las que los subtermosson en sí mismas formas normales. Esto da una descripción sintáctica inductiva de formas normales.
También existe la noción de forma normal de cabeza débil : un término en forma normal de cabeza débil es un término en forma normal de cabeza o una abstracción lambda. [2] Esto significa que un redex puede aparecer dentro de un cuerpo lambda.
Estrategias de reducción
En general, un término dado puede contener varios redexes, por lo que se podrían aplicar varias reducciones beta diferentes. Podemos especificar una estrategia para elegir qué redex reducir.
- La reducción de orden normal es la estrategia en la que se aplica continuamente la regla de reducción beta en la posición de la cabeza hasta que no sean posibles más reducciones de este tipo. En ese momento, el término resultante está en su forma normal principal. Luego se continúa aplicando reducción de cabeza en los subterráneos., de izquierda a derecha. Dicho de otra manera, la reducción de orden normal es la estrategia que siempre reduce primero el redex más externo a la izquierda.
- Por el contrario, en la reducción de orden aplicativo , se aplican primero las reducciones internas y luego solo se aplica la reducción de altura cuando no son posibles más reducciones internas.
La reducción de orden normal es completa, en el sentido de que si un término tiene una forma normal inicial, la reducción de orden normal eventualmente la alcanzará. Según la descripción sintáctica de las formas normales anterior, esto implica la misma declaración para una forma "completamente" normal (este es el teorema de estandarización ). Por el contrario, la reducción del orden de aplicación no puede terminar, incluso cuando el término tiene una forma normal. Por ejemplo, utilizando la reducción de orden aplicativa, es posible la siguiente secuencia de reducciones:
Pero usando la reducción de orden normal, el mismo punto de partida se reduce rápidamente a la forma normal:
Las cadenas de director de Sinot son un método mediante el cual se puede optimizar la complejidad computacional de la reducción beta.
Ver también
Referencias
- ^ "Forma Beta normal" . Enciclopedia . TheFreeDictionary.com . Consultado el 18 de noviembre de 2013 .
- ^ "Forma normal de la cabeza débil" . Enciclopedia . TheFreeDictionary.com . Consultado el 30 de abril de 2021 .