Forma normal beta

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