Forma normal beta

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Translation Latin Alphabet.svg
Este artigo ou secção está a ser traduzido. Ajude e colabore com a tradução.

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[editar | editar código-fonte]

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).

Ver também[editar | editar código-fonte]