Lema de Newman
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.[1]
Importância[editar | editar código-fonte]
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.
Notas
- ↑ Harrison, p. 260; Paterson(1990), p. 354.
Bibliografia[editar | editar código-fonte]
- 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