Teorema de Church-Rosser
Aspeto
Este artigo ou secção contém uma lista de referências no fim do texto, mas as suas fontes não são claras porque não são citadas no corpo do artigo, o que compromete a confiabilidade das informações. (Agosto de 2021) |
O Teorema de Church-Rosser é um resultado de confluência para o cálculo lambda e também uma propriedade sobre sistemas de redução abstratos equivalente à confluência e a semi-confluência.
(Se busca pela propriedade de Church-Rosser consulte confluência em sistemas de reescrita de termos.)
Teorema de Church-Rosser e o Cálculo Lambda
[editar | editar código-fonte]O teorema de Church-Rosser enuncia que se existem duas conversões/reduções distintas iniciadas de um mesmo termo no cálculo lambda, então existe um termo que é alcançado através de uma cadeia de redução (possivelmente vazia) de ambas reduções. Olhando para o cálculo lambda como um sistema de reescrita de termos, o teorema de Church-Rosser é uma demonstração de confluência. O teorema foi demonstrado em 1936 por Alonzo Church e J. Barkley Rosser.
Bibliografia
[editar | editar código-fonte]- Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003.
- Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998.