Confluencia (reescritura abstracta)

En informática y matemáticas, la confluencia es una propiedad de los sistemas de reescritura que describe qué términos de dicho sistema 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 .

Ejemplos motivadores

Las reglas habituales 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 el mismo resultado. Si toda expresión aritmética se evalúa al mismo resultado independientemente de la estrategia de reducción, se dice que el sistema de reescritura aritmética es confluente en la base. Los sistemas de reescritura aritmética pueden ser confluentes o solo confluentes en la base, dependiendo de los detalles del sistema. ^{[ 1 ]}

Un segundo ejemplo, más abstracto, se obtiene de la siguiente demostración 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 y establece cinco proposiciones R4, R6, R10, R11 y R12, cada una de ellas utilizando algunas anteriores, 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 ⁻¹ ⋅ 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 tales pasos, que son difíciles de encontrar para una persona inexperta, y mucho menos para un programa informático .

Si un sistema de reescritura de términos es confluente y terminante , existe un método sencillo para demostrar la igualdad entre dos expresiones (también conocidas como términos ) s y t : comenzando con s , se aplican igualdades ^{[ nota 1 ]} de izquierda a derecha hasta donde sea posible, obteniendo finalmente un término s′ . De manera similar, se obtiene un término t′ de t . Si ambos términos s′ y t′ coinciden literalmente, entonces se demuestra que s y t son iguales. Más importante aún, si no coinciden, entonces s y t no pueden ser iguales. Es decir, cualquier par de términos s y t que puedan demostrarse iguales pueden demostrarse mediante este método.

El éxito de ese método no depende de un orden sofisticado específico para aplicar las reglas de reescritura, ya que la confluencia garantiza que cualquier secuencia de aplicaciones de reglas conducirá finalmente al mismo resultado (mientras que la propiedad de terminación asegura que cualquier secuencia llegará a su fin). Por lo tanto, si se puede proporcionar un sistema de reescritura de términos confluente y terminante para alguna teoría ecuacional , ^{[ nota 2 ]} no se requiere ni una pizca de creatividad para realizar demostraciones de igualdad de términos; esa tarea, por consiguiente, se vuelve susceptible de ser realizada por programas informáticos. Los enfoques modernos manejan sistemas de reescritura abstractos más generales que sistemas de reescritura de términos ; estos últimos son un caso especial de los primeros.

Caso general y teoría

En este diagrama, $a$ se reduce a $b$ o $c$ en cero o más pasos de reescritura (indicados por el asterisco). Para que la relación de reescritura sea confluente, ambos reductos deben a su vez reducirse a algún $d$ común .

Un sistema de reescritura puede expresarse como un grafo dirigido en el que los nodos representan expresiones y las aristas representan reescrituras. Así, por ejemplo, si la expresión a puede reescribirse como b , decimos que b es una reducción de a (o, alternativamente, a se reduce a b , o a es una expansión de b ). Esto se representa mediante 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 del grafo 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 el cierre reflexivo-transitivo de →. Usando el ejemplo del párrafo anterior, tenemos (11+9)×(2+4) → 20×(2+4) y 20×(2+4) → 20×6, por lo que (11+9)×(2+4) ∗ → 20×6.

Una vez establecido esto, la confluencia se puede definir de la siguiente manera. Se considera que a ∈ S es 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 $b\mathbin {\downarrow } c$ Si todo 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.

Confluencia del terreno

Un sistema de reescritura de términos es confluente en su base si cada término base es confluente, es decir, cada término sin variables. ^{[ 3 ]}

Confluencia local

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 todo a ∈ S es localmente confluente, entonces → se llama localmente confluente, o posee la propiedad débil de Church-Rosser . Esto es diferente de la confluencia en que b y c deben reducirse de a en un paso. En analogía con esto, a la confluencia a veces se la denomina confluencia global .

La relación ∗ → , introducida como notación para secuencias de reducción, puede considerarse un sistema de reescritura en sí mismo, cuya relación es el cierre reflexivo-transitivo de → . Dado que una secuencia de secuencias de reducción es también una secuencia de reducción (o, equivalentemente, dado que la formación del cierre reflexivo-transitivo es idempotente ), ∗ ∗ → = ∗ → . De ello se deduce que → es confluente si y solo si ∗ → es localmente confluente.

Un sistema de reescritura puede ser localmente confluente sin ser globalmente confluente. En las figuras 1 y 2 se muestran ejemplos. 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 terminante o fuertemente normalizador ), entonces es globalmente confluente.

Propiedad Church-Rosser

Se dice que un sistema de reescritura posee la propiedad Church-Rosser si y solo si $x{\stackrel {*}{\leftrightarrow }}y$ implica $x{\mathbin {\downarrow }}y$ 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 la palabra 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 podría 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 solo si es confluente. ^{[ 9 ]} Debido a esta equivalencia, se encuentra una considerable variación en las definiciones en la literatura. Por ejemplo, en "Terese", la propiedad de Church-Rosser y la confluencia se definen como sinónimas e idénticas 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 diferencia con otros textos es deliberada. ^{[ 10 ]}

Semiconfluencia

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 solo paso de reescritura. Al considerar un elemento alcanzado en un solo 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 tiene por qué ser confluente, pero un sistema de reescritura semiconfluente es necesariamente confluente, y un sistema confluente es trivialmente semiconfluente.

Fuerte confluencia

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 o bien c → d o bien c = d ; si todo a ∈ S es fuertemente confluente, decimos que → es fuertemente confluente.

Un elemento confluente no tiene por qué ser fuertemente confluente, pero un sistema de reescritura fuertemente confluente es necesariamente confluente.

Ejemplos de sistemas confluentes

La reducción de polinomios módulo un ideal es un sistema de reescritura confluente siempre que se trabaje con una base de Gröbner .
El teorema de Matsumoto se deduce de la confluencia de las relaciones de trenzado.
La β-reducción de los términos λ es confluente según el teorema de Church-Rosser .

Véase también

Notas

↑ Luego se denominaron reglas de reescritura para enfatizar su orientación de izquierda a derecha.
↑ El algoritmo de completación de Knuth-Bendix puede utilizarse para calcular dicho sistema a partir de un conjunto dado de ecuaciones. Un ejemplo de este sistema para grupos se muestra aquí , con sus proposiciones numeradas de forma consistente. Utilizándolo, una demostración de R6 consiste en aplicar R11 y R12 en cualquier orden al término ( a ⁻¹ )⁻¹ ⋅1 para obtener el término a ; no se aplican otras reglas.

Referencias

↑ Walters, HR; Zantema, H. (octubre de 1994). "Sistemas de reescritura para aritmética de enteros" (PDF) . Universidad de Utrecht.
↑ Bläsius y Bürckert 1992 , pág. 134 : los nombres de los axiomas y las proposiciones siguen el texto original.
↑ Robinson, Alan JA; Voronkov, Andrei (5 de julio de 2001). Manual de razonamiento automatizado . Gulf Professional Publishing. pág. 560. ISBN 978-0-444-82949-8.
1 2 N. Dershowitz y J.-P. Jouannaud (1990). «Sistemas de reescritura». En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. Vol. B. Elsevier. págs. 243–320 . ISBN 0-444-88074-7.Aquí: pág. 268, Fig. 2a+b.
^ Terese 2003 , págs. 10-11.
↑ Alonzo Church y J. Barkley Rosser. Algunas propiedades de la conversión. Trans. AMS, 39:472-482, 1936
↑ Baader y Nipkow 1998 , pág. 9.
↑ Cooper, SB (2004). Teoría de la computabilidad . Boca Raton: Chapman & Hall/CRC. p. 184. ISBN 1584882379.
↑ Baader y Nipkow 1998 , pág. 11.
↑ Terese 2003 , pág. 11.

"Teresa"; Bezem, Marc; Klop, Jan Willem ; de Vrijer, Roel (2003). Sistemas de reescritura de términos . Tratados de Cambridge sobre informática teórica. Prensa de la Universidad de Cambridge. ISBN 0-521-39115-6.
Baader, Franz ; Nipkow, Tobias (1998). Term Rewriting and All That . Cambridge University Press. ISBN 978-0-521-77920-3.
Blasius, KH; Bürckert, H.-J., eds. (1992). Sistema de deducción . Oldenburgo. pag. 291.

Enlaces externos

Weisstein, Eric W. "Confluente" . MundoMatemático .

[3] Luego se denominaron reglas de reescritura para enfatizar su orientación de izquierda a derecha.

[4] El algoritmo de completación de Knuth-Bendix puede utilizarse para calcular dicho sistema a partir de un conjunto dado de ecuaciones. Un ejemplo de este sistema para grupos se muestra aquí , con sus proposiciones numeradas de forma consistente. Utilizándolo, una demostración de R6 consiste en aplicar R11 y R12 en cualquier orden al término ( a ⁻¹ )⁻¹ ⋅1 para obtener el término a ; no se aplican otras reglas.

[1] Walters, HR; Zantema, H. (octubre de 1994). "Sistemas de reescritura para aritmética de enteros" (PDF) . Universidad de Utrecht.

[2] Bläsius y Bürckert 1992 , pág. 134 : los nombres de los axiomas y las proposiciones siguen el texto original.

[5] Robinson, Alan JA; Voronkov, Andrei (5 de julio de 2001). Manual de razonamiento automatizado . Gulf Professional Publishing. pág. 560. ISBN 978-0-444-82949-8.

[Dershowitz.Jouannaud.1990.Fig2-6] 1 2 N. Dershowitz y J.-P. Jouannaud (1990). «Sistemas de reescritura». En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. Vol. B. Elsevier. págs. 243–320 . ISBN 0-444-88074-7.Aquí: pág. 268, Fig. 2a+b.

[FOOTNOTETerese200310–11-7] Terese 2003 , págs. 10-11.

[8] Alonzo Church y J. Barkley Rosser. Algunas propiedades de la conversión. Trans. AMS, 39:472-482, 1936

[FOOTNOTEBaaderNipkow19989-9] Baader y Nipkow 1998 , pág. 9.

[10] Cooper, SB (2004). Teoría de la computabilidad . Boca Raton: Chapman & Hall/CRC. p. 184. ISBN 1584882379.

[FOOTNOTEBaaderNipkow199811-11] Baader y Nipkow 1998 , pág. 11.

[FOOTNOTETerese200311-12] Terese 2003 , pág. 11.

[ 1 ]

[ 2 ]

[ nota 1 ]

[ nota 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]