Teorema de Church-Rosser
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
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
- 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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.