Forma normal beta

Na teoria do cálculo lambda, um termo se encontra na forma normal beta se não é possível nenhuma redução beta. Da mesma forma, um termo se encontra na forma normal beta-eta se uma redução beta não é possível nem tampouco uma redução eta.

No cálculo lambda, uma redex do tipo beta é um termo da forma

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

onde ${\displaystyle A(x)}$ é um termo (possivelmente) contendo variáveis ${\displaystyle x}$.

Uma redução beta é, essencialmente, uma aplicação da seguinte reescrita da redex do tipo beta

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

onde ${\displaystyle A(t)}$ é o resultado da substituição to termo ${\displaystyle t}$ pela variável ${\displaystyle x}$ no termo ${\displaystyle A(x)}$.

• Cálculo lambda
• Cálculo lambda simplesmente tipado