Forma normal beta

En càlcul lambda, un terme està en forma normal beta si no és possible fer cap reducció beta. Un terme està en forma normal beta-eta si no són possibles ni una reducció beta ni una reducció eta. Un terme està en forma normal de capçalera si no hi ha cap beta-redex en posició de capçalera.

Reducció beta

En càlcul lambda, una beta redex és un terme de la forma

$((\mathbf {\lambda } x.A(x))t)$

on $A(x)$ és un terme depenent, possiblement, de la variable $x$.

Una reducció beta és una aplicació de la següent regla de reescriptura a una beta redex:

$((\mathbf {\lambda } x.A(x))t)\rightarrow A(t)$

on $A(t)$ és el resultat de substituir la variable $x$ pel terme $t$ al terme $A(x)$.

Una reducció beta està en posició de capçalera si està en la forma següent:

$\lambda x_{0}\ldots \lambda x_{i-1}.(\lambda x_{i}.A(x_{i}))M_{1}M_{2}\ldots M_{n}\rightarrow \lambda x_{0}\ldots \lambda x_{i-1}.A(M_{1})M_{2}\ldots M_{n}$, on $i\geq 0,n\geq 1$.

Qualsevol reducció que no estigui en aquesta forma és una reducció beta interna.

Estratègies de reducció

En general, pot haver-hi diferents reduccions beta possibles per a un terme donat. La reducció en ordre normal és l'estratègia d'avaluació en la qual hom continua aplicant la regla de reducció beta en posició inicial fins que no es pugui reduir més. Un cop arribat a aquest punt, el terme resultant està en forma normal.

En canvi, en una reducció en ordre aplicatiu hom aplica primer les reduccions internes i, quan ja no s'hi poden aplicar més, després s'aplica la reducció a la capçalera.

La reducció en ordre normal és completa, en el sentit que, si un terme té a la capçalera una forma normal, la reducció en ordre normal arribarà algun cop a aquesta capçalera. En canvi, pot ser que la reducció en ordre aplicatiu no acabi mai, fins i tot quan el terme té una forma normal. Per exemple, si hom usa una reducció en ordre aplicatiu, podem tenir aquesta successió de reduccions:

$(\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$

Però si hom usa les reduccions en ordre normal, l'expressió inicial es redueix ràpidament a una forma normal:

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

$\rightarrow z$

Les cadenes directrius de Sinot proporcionen un mètode per optimitzar la complexitat computacional de la reducció beta.

Vegeu també

• Càlcul lambda
• Forma normal