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

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

$((𝝀x.A(x))t)\to A(t)$

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

Ver também

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