Na teoria dos sistemas de reescrita, o lema de Newman enuncia que um sistema de redução abstrato noetheriano (ou fortemente normalizante, isto é, um sistena no qual não há cadeias de redução infinitas) é confluente se, e somente se, ele for localmente confluente. Esta propriedade dos sistemas de redução abstratos pode ser utilizada para mostrar a confluência de tais sistemas.
Atualmente o lema é visto como sendo um resultado puramente combinatorial baseado em uma propriedade válida para algumas relações (de serem bem-fundadas), devido a uma prova por indução noetheriana dada por Gérard Huet em 1980. A demonstração original de Newman foi consideravelmente mais complicada.Harrison, p. 260; Paterson(1990), p. 354.
Importância O problema de determinar se um sistema de reescrita de termos é confluente é indecidível, logo o lema é de grande ajuda para responder tal questão. No entanto, para podermos aplicá-lo, necessitamos garantir que o sistema seja terminante ou fortemente normalizante, o que também é um problema indecidível. Existem porém técnicas, para casos especiais, que demonstram a terminação de um sistema.
Verificando que o sistema termina, surge outro problema: como garantir que o sistema seja localmente confluente? Para isso podemos recorrer ao estudo dos pares críticos do sistema de reescrita de termos. Há um resultado segundo o qual um sistema de reescrita de termos é localmente confluente se e somente se todos os pares críticos do sistema forem ligáveis.
Como o sistema é terminante o problema de decidir se dois termos são ligáveis é decidível, logo obtemos uma importante aplicação do lema de Newman: um sistema de reescrita de termos terminante é confluente se e somente se todos os pares críticos do sistema são ligáveis.
Bibliografia M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Número 2, páginas 223—243, 1942. Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), October 1980, Volume 27, Issue 4, pp. 797 – 821. Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (book weblink) Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998 (book weblink) John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, ISBN 9780521899574, capítulo 4 "Equality". Michael S. Paterson. Automata, languages, and programming: 17th international colloquium. Warwick University, England, July 16-20, 1990: proceedings. Volume 443 de Lecture notes in computer science. Springer, 1990. ISBN 9783540528265
Ver também Sistema de reescrita de termos Forma normal
Categoria:Sistemas de reescrita de termos