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.

Ver também

• Sistema de reescrita de termos
• Sistema de redução abstrato
• Confluência