En matemáticas , en la teoría de los sistemas de reescritura , el lema de Newman , también llamado comúnmente lema del diamante , establece que un sistema de reescritura abstracta (ARS) terminante (o fuertemente normalizador ), es decir, uno en el que no hay secuencias de reducción infinitas, es confluente si es localmente confluente . De hecho, un ARS de terminación es confluente precisamente cuando es localmente confluente. [1]
De manera equivalente, para cada relación binaria sin cadenas infinitas decrecientes y que satisfaga una versión débil de la propiedad del diamante, existe un elemento mínimo único en cada componente conectado de la relación considerada como un gráfico .
Hoy, esto se ve como un resultado puramente combinatorio basado en fundamento debido a una prueba de Gérard Huet en 1980. [2] La prueba original de Newman era considerablemente más complicada. [3]
Lema de diamante
En general, el lema de Newman puede verse como un resultado combinatorio sobre relaciones binarias → en un conjunto A (escrito al revés, de modo que a → b significa que b está por debajo de a ) con las siguientes dos propiedades:
- → es una relación bien fundada : todo subconjunto no vacío X de A tiene un elemento mínimo (un elemento a de X tal que a → b para no b en X ). De manera equivalente, no hay una cadena infinita un 0 → un 1 → un 2 → un 3 → ... . En la terminología de los sistemas de reescritura, → está terminando.
- Cada cubierta está delimitada por debajo. Es decir, si un elemento de una en A cubre elementos b y c en A en el sentido de que un → b y un → c , entonces no es un elemento d en A tal que b d y c d , dondedenota el cierre transitivo reflexivo de →. En la terminología de los sistemas de reescritura, → confluye localmente.
Si las dos condiciones anteriores se cumplen, entonces el lema establece que → es confluente: siempre que un b y una c , hay un elemento d tal que b d y c d . En vista de la terminación de →, esto implica que cada componente conectado de → como gráfico contiene un elemento mínimo único a , además b a para cada elemento b del componente. [4]
Notas
- ^ Franz Baader , Tobias Nipkow , (1998) Reescritura de términos y todo eso , Cambridge University Press ISBN 0-521-77920-0
- ^ Gérard Huet , "Reducciones confluentes: propiedades abstractas y aplicaciones a sistemas de reescritura de términos", Journal of the ACM ( JACM ), octubre de 1980, volumen 27 , número 4, págs. 797 - 821.
- ^ Harrison, pág. 260, Paterson (1990), pág. 354.
- ^ Paul M. Cohn , (1980) Álgebra universal , D. Reidel Publishing, ISBN 90-277-1254-9 ( Véanse las págs. 25-26 )
Referencias
- MHA Newman . Sobre teorías con una definición combinatoria de "equivalencia" . Annals of Mathematics, 43, Número 2, páginas 223–243, 1942.
- Paterson, Michael S. (1990). Autómatas, lenguajes y programación: XVII coloquio internacional . Apuntes de conferencias en informática. 443 . Universidad de Warwick, Inglaterra: Springer. ISBN 978-3-540-52826-5.
Libros de texto
- Term Rewriting Systems , Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (enlace web del libro)
- Reescritura de términos y todo eso , Franz Baader y Tobias Nipkow, Cambridge University Press, 1998 (enlace web del libro)
- John Harrison, Manual de lógica práctica y razonamiento automatizado , Cambridge University Press, 2009, ISBN 978-0-521-89957-4 , capítulo 4 "Igualdad".
enlaces externos
- Lema del diamante en PlanetMath .
- "Prueba de Newman del lema de Newman", un PDF sobre la prueba original , archivado el 6 de julio de 2017 en Wayback Machine.