Forma normal beta

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Translation Latin Alphabet.svg
Este artigo ou seçã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

onde é um termo (possivelmente) contendo variáveis .

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

onde é o resultado da substituição to termo pela variável no termo .

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