Confluencia (reescritura abstracta)
En informática, la confluencia es una propiedad de los sistemas de reescritura , que describe qué términos de dicho sistema se pueden reescribir en más de una forma para producir el mismo resultado. Este artículo describe las propiedades en la configuración más abstracta de un sistema de reescritura abstracta .
Las reglas habituales de la aritmética elemental forman un sistema de reescritura abstracta. Por ejemplo, la expresión (11 + 9) × (2 + 4) se puede evaluar comenzando por el paréntesis izquierdo o derecho; sin embargo, en ambos casos se obtiene eventualmente el mismo resultado. Si cada expresión aritmética se evalúa con el mismo resultado independientemente de la estrategia de reducción, se dice que el sistema de reescritura aritmética es confluente en el suelo. Los sistemas de reescritura aritmética pueden ser confluentes o solo confluentes en el suelo dependiendo de los detalles del sistema de reescritura. [1]
Un segundo ejemplo, más abstracto, se obtiene de la siguiente prueba de que cada elemento del grupo es igual al inverso de su inverso: [2]
Esta prueba parte de los axiomas de grupo dados A1–A3 y establece cinco proposiciones R4, R6, R10, R11 y R12, cada una de las cuales usa algunas anteriores, y R12 es el teorema principal. Algunas de las pruebas requieren pasos no obvios, o incluso creativos, como aplicar el axioma A2 al revés, reescribiendo así "1" a " a −1 ⋅ a" en el primer paso de la prueba de R6. Una de las motivaciones históricas para desarrollar la teoría de la reescritura de términos fue evitar la necesidad de tales pasos, que son difíciles de encontrar para un ser humano sin experiencia, y mucho menos para un programa de computadora [ cita requerida ] .
Si un sistema de reescritura de términos es confluente y termina en , existe un método directo para demostrar la igualdad entre dos expresiones (también conocidas como términos ) s y t : comenzando con s , aplique igualdades [nota 1] de izquierda a derecha tanto como sea posible, eventualmente obteniendo un término s′ . Obtenga de t un término t′ de manera similar. Si ambos términos s′ y t′ concuerdan literalmente, entonces s y t se prueban (como era de esperar) como iguales. Más importante aún, si no están de acuerdo, entoncess y t no pueden ser iguales. Es decir, cualquiera de los dos términos s y t que se puede demostrar que son iguales se puede hacer mediante ese método.
El éxito de ese método no depende de un cierto orden sofisticado en el que se aplican las reglas de reescritura, ya que la confluencia garantiza que cualquier secuencia de aplicaciones de reglas eventualmente conducirá al mismo resultado (mientras que la propiedad de terminación asegura que cualquier secuencia finalmente llegará a su fin). en absoluto). Por lo tanto, si se puede proporcionar un sistema de reescritura de términos confluentes y terminales para alguna teoría ecuacional , [nota 2] no se requiere ni un poco de creatividad para realizar pruebas de igualdad de términos; esa tarea, por lo tanto, se vuelve susceptible a los programas de computadora. Los enfoques modernos manejan sistemas de reescritura abstractos más generales en lugar de términossistemas de reescritura; los segundos son un caso especial de los primeros.
