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.
Ver também Sistema de reescrita de termos Sistema de redução abstrato Confluência
Categoria:Sistemas de reescrita de termos