Forma normal beta
# 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.

## Redução Beta

No cálculo lambda, uma redex do tipo beta é um termo da forma
    $((\mathbf {\lambda } x.A(x))t)$
onde $A(x)$ é um termo (possivelmente) contendo variáveis $x$.
Uma redução beta é, essencialmente, uma aplicação da seguinte reescrita da redex do tipo beta
    $((\mathbf {\lambda } x.A(x))t)\rightarrow A(t)$
onde $A(t)$ é o resultado da substituição to termo $t$ pela variável $x$ no termo $A(x)$.