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 ni una reducción beta ni una reducción eta . Un término está en forma normal cabeza si no hay beta-reducción en la posición 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 cabeza.

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

$${\displaystyle (\mathbf {\lambda } xA)M.}$$

Un redex${\displaystyle r}$está en posición de cabeza en un término${\displaystyle t}$, si${\displaystyle t}$tiene la siguiente forma (tenga en cuenta que la aplicación tiene mayor prioridad que la abstracción, y que la fórmula que aparece a continuación está pensada para ser una abstracción lambda, no una aplicación):

$${\displaystyle \lambda x_{1}\ldots \lambda x_{n}.\underbrace {(\lambda xA)M_{1}} _{{\text{el redex }}r}M_{2}\ldots M_{m},}$$

dónde${\displaystyle n\geq 0}$y${\displaystyle m\geq 1.}$

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

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

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

Una reducción beta de cabeza es una reducción beta aplicada en posición de cabeza, es decir, de la siguiente forma:

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

dónde${\displaystyle n\geq 0}$y${\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 reducción beta, ^{[ 3 ] [ 5 ]} es decir, que no se puede reducir más. Algunos autores también pueden incluir reducciones η, de ahí los términos distintivos forma normal beta y forma normal beta-eta .

Una forma normal de cabeza es un término que no contiene una redex beta en posición de cabeza, es decir, que no puede reducirse 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, destinados a ser reducidos por reglas delta adicionales), 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},}$$

dónde${\displaystyle x}$es una variable,${\displaystyle n\geq 0}$y${\displaystyle m\geq 0}$.

Una forma normal de cabeza no siempre es una forma normal, ^{[ 5 ]} debido a los argumentos aplicados${\displaystyle M_{j}}$no tiene por qué ser normal. Sin embargo, lo contrario 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${\displaystyle M_{j}}$son en sí mismas formas normales. Esto proporciona una descripción sintáctica inductiva de las formas normales.

También existe la noción de forma normal de cabeza débil . Un término λ, M, está en forma normal de cabeza débil en caso de que sea una abstracción λ,${\displaystyle M=\mathbf {\lambda } xN}$dónde${\displaystyle N}$es cualquier expresión, incluso conteniendo un redex, o está en forma normal de cabeza (en el cálculo lambda puro, las únicas formas normales de cabeza que no son abstracciones λ son de la forma${\displaystyle xM_{1}M_{2}\ldots M_{m}}$, dónde${\displaystyle x}$es cualquier variable y${\displaystyle m\geq 0}$). ^{[ 6 ]} Las formas normales de cabeza débil fueron introducidas por Simon Peyton Jones para reflejar la forma a la que realmente se evalúan los lenguajes funcionales. ^{[ 6 ] [ 7 ]}

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