Forma normal beta

En el cálculo lambda , un término está en forma normal beta si no es posible ninguna reducción beta . ^[1] Un término está en forma normal beta-eta si no es posible ninguna reducción beta ni ninguna reducción eta . Un término está en forma normal de cabeza si no hay beta-redex en la posición de cabeza . La forma normal de un término, si existe, es única (como corolario del teorema de Church-Rosser ). ^[2] Sin embargo, un término puede tener más de una forma normal de cabeza.

Reducción beta

En el cálculo lambda, un beta redex es un término de la forma: ^{[3] [4]}

${\displaystyle (\mathbf {\lambda } x.A)M}$.

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): ${\displaystyle r}$ ${\displaystyle t}$ ${\displaystyle t}$

${\displaystyle \lambda x_{1}\ldots \lambda x_{n}.\underbrace {(\lambda x.A)M_{1}} _{{\text{the redex }}r}M_{2}\ldots M_{m}}$, donde y . ${\displaystyle n\geq 0}$ ${\displaystyle m\geq 1}$

Una reducción beta es una aplicación de la siguiente regla de reescritura a una redex beta contenida en un término:

${\displaystyle (\mathbf {\lambda } x.A)M\longrightarrow A[x:=M]}$

donde es el resultado de sustituir el término por la variable en el término . ${\displaystyle A[x:=M]}$ ${\displaystyle M}$ ${\displaystyle x}$ ${\displaystyle A}$

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:

${\displaystyle \lambda x_{1}\ldots \lambda x_{n}.(\lambda x.A)M_{1}M_{2}\ldots M_{m}\longrightarrow \lambda x_{1}\ldots \lambda x_{n}.A[x:=M_{1}]M_{2}\ldots M_{m}}$, donde y . ${\displaystyle n\geq 0}$ ${\displaystyle m\geq 1}$

Cualquier otra reducción es una reducción beta interna .

Una forma normal es un término que no contiene ninguna beta redex, ^{[3] [5]} es decir , que no se puede reducir más. Una forma normal de cabeza es un término que no contiene una beta redex en la posición de cabeza, es decir , que no se puede reducir más mediante una reducción de cabeza. Al considerar el cálculo lambda simple (es decir, sin la adición de símbolos de constante o función, que se pretende reducir mediante una regla delta adicional), las formas normales de cabeza son los términos de la siguiente forma:

${\displaystyle \lambda x_{1}\ldots \lambda x_{n}.xM_{1}M_{2}\ldots M_{m}}$, donde es una variable, y . ${\displaystyle x}$ ${\displaystyle n\geq 0}$ ${\displaystyle m\geq 0}$

Una forma normal de cabeza no siempre es una forma normal, ^[5] porque los argumentos aplicados no necesitan ser normales. Sin embargo, lo inverso es cierto: cualquier forma normal es también una forma normal de cabeza. ^[5] De hecho, las formas normales son exactamente las formas normales de cabeza en las que los subtérminos son en sí mismos formas normales. Esto da una descripción sintáctica inductiva de las formas normales. ${\displaystyle M_{j}}$ ${\displaystyle M_{j}}$

También existe el concepto 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. ^[6] 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 redex, 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 ya no sean posibles más reducciones de este tipo. En ese punto, el término resultante está en forma normal de la cabeza. Luego se continúa aplicando la reducción de la cabeza en los subtérminos , de izquierda a derecha. Dicho de otro modo, la reducción de orden normal es la estrategia que siempre reduce primero el redex más externo a la izquierda. ${\displaystyle M_{j}}$
• 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 carga cuando ya 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 de cabeza, la reducción de orden normal acabará por alcanzarla. Según la descripción sintáctica de las formas normales que se ha expuesto anteriormente, esto implica la misma afirmación para una forma “completamente” normal (este es el teorema de estandarización). Por el contrario, la reducción de orden aplicativo puede no terminar, incluso cuando el término tiene una forma normal. Por ejemplo, utilizando la reducción de orden aplicativo, es posible la siguiente secuencia de reducciones:

${\displaystyle {\begin{aligned}&(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\&\ldots \end{aligned}}}$

Pero utilizando la reducción de orden normal, el mismo punto de partida se reduce rápidamente a la forma normal:

${\displaystyle (\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))}$

${\displaystyle \rightarrow z}$

Las cuerdas directoras de Sinot son un método mediante el cual se puede optimizar la complejidad computacional de la reducción beta.

Véase también

• Cálculo lambda
• Forma normal (desambiguación)

Referencias

1. "Forma normal beta". Enciclopedia . TheFreeDictionary.com . Consultado el 18 de noviembre de 2013 .
2. Thompson, Simon (1991). Teoría de tipos y programación funcional. Wokingham, Inglaterra: Addison-Wesley. p. 38. ISBN 0-201-41667-0.OCLC 23287456  .
3. Barendregt, Henk P. (1984). Introducción al cálculo Lambda (PDF) (edición revisada). pag. 24.
4. Thompson, Simon (1991). Teoría de tipos y programación funcional. Wokingham, Inglaterra: Addison-Wesley. p. 35. ISBN 0-201-41667-0.OCLC 23287456  .
5. Thompson, Simon (1991). Teoría de tipos y programación funcional. Wokingham, Inglaterra: Addison-Wesley. p. 36. ISBN 0-201-41667-0.OCLC 23287456  .
6. "Forma normal de cabeza débil". Enciclopedia . TheFreeDictionary.com . Consultado el 30 de abril de 2021 .