En informática y matemáticas, la confluencia es una propiedad de los sistemas de reescritura que describe qué términos de un sistema de este tipo pueden reescribirse de más de una manera para obtener el mismo resultado. Este artículo describe las propiedades en el contexto más abstracto de un sistema de reescritura abstracto .
Las reglas usuales de la aritmética elemental forman un sistema de reescritura abstracto. Por ejemplo, la expresión (11 + 9) × (2 + 4) puede evaluarse comenzando por el paréntesis izquierdo o derecho; sin embargo, en ambos casos se obtiene finalmente el mismo resultado. Si cada expresión aritmética evalúa el mismo resultado independientemente de la estrategia de reducción, se dice que el sistema de reescritura aritmética es confluente en el terreno. Los sistemas de reescritura aritmética pueden ser confluentes o solo confluentes en el terreno según 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 demostración parte de los axiomas de grupo A1–A3 dados y establece cinco proposiciones R4, R6, R10, R11 y R12, cada una de las cuales utiliza algunos de los anteriores y siendo R12 el teorema principal. Algunas de las demostraciones requieren pasos no obvios, o incluso creativos, como aplicar el axioma A2 a la inversa, reescribiendo así "1" como " a −1 ⋅ a" en el primer paso de la demostración de R6. Una de las motivaciones históricas para desarrollar la teoría de la reescritura de términos fue evitar la necesidad de dichos pasos, que son difíciles de encontrar para un humano inexperto, y mucho menos para un programa informático [ cita requerida ] .
Si un sistema de reescritura de términos es confluente y termina en , existe un método sencillo 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, obteniendo finalmente 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 iguales. Más importante aún, si no están de acuerdo, entonces s y t no pueden ser iguales. Es decir, dos términos s y t cualesquiera que se puedan probar iguales se pueden probar con ese método.
El éxito de ese método no depende de un cierto orden sofisticado en el que aplicar las reglas de reescritura, ya que la confluencia asegura que cualquier secuencia de aplicaciones de reglas eventualmente conducirá al mismo resultado (mientras que la propiedad de terminación asegura que cualquier secuencia eventualmente llegará a un final). Por lo tanto, si se puede proporcionar un sistema de reescritura de términos confluente y terminal para alguna teoría de ecuaciones , [nota 2] no se requiere ni una pizca de creatividad para realizar pruebas de igualdad de términos; esa tarea, por lo tanto, se vuelve susceptible a programas de computadora. Los enfoques modernos manejan sistemas de reescritura abstracta más generales en lugar de sistemas de reescritura de términos ; estos últimos son un caso especial de los primeros.
Un sistema de reescritura se puede expresar como un grafo dirigido en el que los nodos representan expresiones y las aristas representan reescrituras. Así, por ejemplo, si la expresión a se puede reescribir en b , entonces decimos que b es una reducción de a (alternativamente, a se reduce a b , o a es una expansión de b ). Esto se representa utilizando la notación de flechas; a → b indica que a se reduce a b . Intuitivamente, esto significa que el grafo correspondiente tiene una arista dirigida de a a b .
Si existe un camino entre dos nodos de grafos c y d , entonces se forma una secuencia de reducción . Por ejemplo, si c → c′ → c′′ → ... → d′ → d , entonces podemos escribir c d , lo que indica la existencia de una secuencia de reducción de c a d . Formalmente,es la clausura reflexiva-transitiva de →. Usando el ejemplo del párrafo anterior, tenemos (11+9)×(2+4) → 20×(2+4) y 20×(2+4) → 20×6, entonces (11+9)×(2+4)20×6.
Una vez establecido esto, la confluencia se puede definir de la siguiente manera. a ∈ S se considera confluente si para todos los pares b , c ∈ S tales que a B y a c , existe un d ∈ S con b d y c d (denotado ). Si cada a ∈ S es confluente, decimos que → es confluente. Esta propiedad también se denomina a veces propiedad del diamante , por la forma del diagrama que se muestra a la derecha. Algunos autores reservan el término propiedad del diamante para una variante del diagrama con reducciones simples en todas partes; es decir, siempre que a → b y a → c , debe existir un d tal que b → d y c → d . La variante de reducción simple es estrictamente más fuerte que la de reducción múltiple.
Un sistema de reescritura de términos es confluente en el terreno si cada término fundamental es confluente, es decir, cada término sin variables. [3]
Se dice que un elemento a ∈ S es localmente confluente (o débilmente confluente [5] ) si para todo b , c ∈ S con a → b y a → c existe d ∈ S con b d y c d . Si cada a ∈ S es localmente confluente, entonces → se llama localmente confluente, o tiene la propiedad débil de Church-Rosser . Esto es diferente de la confluencia en que b y c deben reducirse a partir de a en un solo paso. En analogía con esto, la confluencia a veces se denomina confluencia global .
La relación, introducido como una notación para secuencias de reducción, puede ser visto como un sistema de reescritura por derecho propio, cuya relación es el cierre reflexivo-transitivo de → . Dado que una secuencia de secuencias de reducción es nuevamente una secuencia de reducción (o, equivalentemente, dado que formar el cierre reflexivo-transitivo es idempotente ),=. De ello se deduce que → es confluente si y sólo siEs localmente confluente.
Un sistema de reescritura puede ser localmente confluente sin ser (globalmente) confluente. Se muestran ejemplos en las figuras 1 y 2. Sin embargo, el lema de Newman establece que si un sistema de reescritura localmente confluente no tiene secuencias de reducción infinitas (en cuyo caso se dice que es terminal o fuertemente normalizante ), entonces es globalmente confluente.
Se dice que un sistema de reescritura posee la propiedad de Church-Rosser si y solo si implica para todos los objetos x , y . Alonzo Church y J. Barkley Rosser demostraron en 1936 que el cálculo lambda tiene esta propiedad; [6] de ahí el nombre de la propiedad. [7] (El hecho de que el cálculo lambda tenga esta propiedad también se conoce como el teorema de Church-Rosser .) En un sistema de reescritura con la propiedad de Church-Rosser, el problema de palabras puede reducirse a la búsqueda de un sucesor común. En un sistema de Church-Rosser, un objeto tiene como máximo una forma normal ; es decir, la forma normal de un objeto es única si existe, pero bien puede no existir. En el cálculo lambda, por ejemplo, la expresión (λx.xx)(λx.xx) no tiene una forma normal porque existe una secuencia infinita de β-reducciones (λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ... [8]
Un sistema de reescritura posee la propiedad de Church-Rosser si y sólo si es confluente. [9] Debido a esta equivalencia, en la literatura se encuentran bastantes variaciones en las definiciones. Por ejemplo, en "Terese" la propiedad de Church-Rosser y la confluencia se definen como sinónimos e idénticos a la definición de confluencia presentada aquí; Church-Rosser tal como se define aquí permanece sin nombre, pero se da como una propiedad equivalente; esta desviación de otros textos es deliberada. [10]
La definición de confluencia local difiere de la de confluencia global en que solo se consideran los elementos alcanzados desde un elemento dado en un único paso de reescritura. Al considerar un elemento alcanzado en un único paso y otro elemento alcanzado por una secuencia arbitraria, llegamos al concepto intermedio de semiconfluencia: se dice que a ∈ S es semiconfluente si para todo b , c ∈ S con a → b y a c existe d ∈ S con b d y c d ; si todo a ∈ S es semiconfluente, decimos que → es semiconfluente.
Un elemento semiconfluente no necesita ser confluente, pero un sistema de reescritura semiconfluente es necesariamente confluente, y un sistema confluente es trivialmente semiconfluente.
La confluencia fuerte es otra variación de la confluencia local que nos permite concluir que un sistema de reescritura es globalmente confluente. Se dice que un elemento a ∈ S es fuertemente confluente si para todo b , c ∈ S con a → b y a → c existe d ∈ S con b d y c → d o c = d ; si cada a ∈ S es fuertemente confluente, decimos que → es fuertemente confluente.
Un elemento confluente no necesita ser fuertemente confluente, pero un sistema de reescritura fuertemente confluente es necesariamente confluente.
