Sistema de reescritura abstracta

En lógica matemática e informática teórica , un sistema de reescritura abstracta (también sistema de reducción (abstracto) o sistema de reescritura abstracta ; ARS abreviado ) es un formalismo que captura la noción y propiedades por excelencia de los sistemas de reescritura . En su forma más simple, un ARS es simplemente un conjunto (de "objetos") junto con una relación binaria , tradicionalmente denotada con ; esta definición se puede refinar aún más si indexamos (etiquetamos) subconjuntos de la relación binaria. A pesar de su simplicidad, un ARS es suficiente para describir propiedades importantes de sistemas de reescritura como${\displaystyle \rightarrow }$formas normales , terminación y diversas nociones de confluencia .

Históricamente, ha habido varias formalizaciones de reescritura en un entorno abstracto, cada una con sus idiosincrasias. Esto se debe en parte al hecho de que algunas nociones son equivalentes, ver más abajo en este artículo. La formalización que se encuentra más comúnmente en monografías y libros de texto, y que generalmente se sigue aquí, se debe a Gérard Huet (1980). ^[1]

Definición

Un sistema de reducción abstracto ( ARS ) es la noción más general (unidimensional) sobre la especificación de un conjunto de objetos y reglas que se pueden aplicar para transformarlos. Más recientemente, los autores también utilizan el término sistema de reescritura de resúmenes . ^[2] (La preferencia por la palabra "reducción" en lugar de "reescritura" constituye una desviación del uso uniforme de "reescritura" en los nombres de sistemas que son particularizaciones de ARS. Porque la palabra "reducción" no aparece en los nombres de los sistemas más especializados, en los textos más antiguos sistema de reducción es sinónimo de ARS). ^[3]

Un ARS es un conjunto A , cuyos elementos generalmente se denominan objetos, junto con una relación binaria en A , tradicionalmente denotada por →, y llamada relación de reducción , relación de reescritura ^[2] o simplemente reducción . ^[3] Esta terminología (arraigada) que usa "reducción" es un poco engañosa, porque la relación no necesariamente reduce alguna medida de los objetos.

En algunos contextos, puede ser beneficioso distinguir entre algunos subconjuntos de las reglas, es decir, algunos subconjuntos de la relación de reducción →, por ejemplo, la relación de reducción completa puede consistir en reglas de asociatividad y conmutatividad . En consecuencia, algunos autores definen la relación de reducción → como la unión indexada de algunas relaciones; por ejemplo si , la notación utilizada es (A, → ₁ , → ₂ ).${\displaystyle {\rightarrow _{1}\cup \rightarrow _{2}}={\rightarrow }}$

Como objeto matemático, un ARS es exactamente lo mismo que un sistema de transición de estado sin etiquetar , y si la relación se considera como una unión indexada, entonces un ARS es lo mismo que un sistema de transición de estado etiquetado con los índices como etiquetas. Sin embargo, el enfoque del estudio y la terminología son diferentes. En un sistema de transición de estado, uno está interesado en interpretar las etiquetas como acciones, mientras que en un ARS el enfoque está en cómo los objetos pueden transformarse (reescribirse) en otros. ^[4]

Ejemplo 1

Supongamos que el conjunto de objetos es T = { a , b , c } y la relación binaria está dada por las reglas un → b , b → una , un → c , y b → c . Observe que estas reglas se pueden aplicar tanto a a como a b para obtener c . Además, no se puede aplicar nada a c para transformarlo más. Esta propiedad es claramente importante.

Nociones basicas

Primero defina algunas nociones y notaciones básicas. ^[5]

• ${\displaystyle {\stackrel {+}{\rightarrow }}}$es el cierre transitivo de .${\displaystyle \rightarrow }$
• ${\displaystyle {\stackrel {*}{\rightarrow }}}$es el cierre transitivo reflexivo de , es decir, el cierre transitivo de , donde = es la relación de identidad . De manera equivalente, es el preorden más pequeño que contiene .${\displaystyle \rightarrow }$${\displaystyle (\rightarrow )\cup (=)}$${\displaystyle {\stackrel {*}{\rightarrow }}}$${\displaystyle \rightarrow }$
• ${\displaystyle \leftrightarrow }$es el cierre simétrico de , es decir , la unión de la relación → con su relación inversa .${\displaystyle \rightarrow }$${\displaystyle (\rightarrow )\cup (\rightarrow )^{-1}}$
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$es el cierre simétrico transitivo reflexivo de , es decir, el cierre transitivo de . De manera equivalente, es la relación de equivalencia más pequeña que contiene .${\displaystyle \rightarrow }$${\displaystyle (\leftrightarrow )\cup (=)}$${\displaystyle {\stackrel {*}{\leftrightarrow }}}$${\displaystyle \rightarrow }$

Formas normales y el problema verbal

Resolver el problema verbal: decidir si normalmente requiere una búsqueda heurística ( rojo , verde ), mientras que decidir es sencillo ( gris ). Para los sistemas de reescritura de términos, el algoritmo de terminación de Knuth-Bendix se amplía para establecer formas normales únicas, si es posible.${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$${\displaystyle x\downarrow =y\downarrow }$${\displaystyle \rightarrow }$

Artículo principal: forma normal (reescritura de resúmenes)

Un objeto x en A se llama reducible si existe algún otro y en A y ; de lo contrario, se denomina forma normal o irreductible . Un objeto y se denomina forma normal de x si e y son irreductibles. Si x tiene una forma normal única , generalmente se denota con . En el ejemplo 1 anterior, c es una forma normal y . Si cada objeto tiene al menos una forma normal, el ARS se denomina normalizador .${\displaystyle x\rightarrow y}$${\displaystyle x{\stackrel {*}{\rightarrow }}y}$${\displaystyle x\downarrow }$${\displaystyle c=a\downarrow =b\downarrow }$

Uno de los problemas importantes que se pueden formular en una ARS es la palabra problema : dado x y y son ellos bajo equivalente ? Este es un escenario muy general para formular el problema verbal para la presentación de una estructura algebraica . Por ejemplo, el problema verbal para grupos es un caso particular de un problema verbal ARS. Para una solución "fácil" del problema verbal es fundamental la existencia de formas normales únicas: en este caso, dos objetos son equivalentes si y sólo si tienen la misma forma normal. El problema verbal de un ARS es indecidible en general.${\displaystyle {\stackrel {*}{\leftrightarrow }}}$${\displaystyle {\stackrel {*}{\leftrightarrow }}}$

Unión

Una noción relacionada, pero más débil que la existencia de formas normales es la de dos objetos siendo acoplable : x y y se dice que son unibles si existe algún z con la propiedad de que . A partir de esta definición, es evidente que se puede definir la relación de unión como , donde está la composición de las relaciones . Joinability se denota generalmente, un tanto confusamente, también con , pero en esta notación la flecha hacia abajo es una relación binaria, es decir, escribimos si x e y son acoplables.${\displaystyle x{\stackrel {*}{\rightarrow }}z{\stackrel {*}{\leftarrow }}y}$${\displaystyle {\stackrel {*}{\rightarrow }}\circ {\stackrel {*}{\leftarrow }}}$${\displaystyle \circ }$${\displaystyle \downarrow }$${\displaystyle x{\mathbin {\downarrow }}y}$

La propiedad Church-Rosser y las nociones de confluencia

Artículo principal: Confluencia (reescritura de resúmenes)

Se dice que un ARS posee la propiedad Church-Rosser si y solo si implica para todos los objetos x , y . De manera equivalente, la propiedad Church-Rosser significa que el cierre simétrico transitivo reflexivo está contenido en la relación de unión. 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] En un ARS con la propiedad Church-Rosser, el problema verbal puede reducirse a la búsqueda de un sucesor común. En un sistema Church-Rosser, un objeto tiene como máximo una${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$${\displaystyle x{\mathbin {\downarrow }}y}$forma normal; esa es la forma normal de un objeto, es única si existe, pero puede que no exista.

Varias propiedades, más simples que Church-Rosser, le son equivalentes. La existencia de estas propiedades equivalentes permite probar que un sistema es Church-Rosser con menos trabajo. Además, las nociones de confluencia se pueden definir como propiedades de un objeto en particular, algo que no es posible para Church-Rosser. Se dice que un ARS es,${\displaystyle (A,\rightarrow )}$

• confluente si y sólo si para todo w , x , y y en A , implica . En términos generales, la confluencia dice que no importa cómo dos caminos diverjan de un ancestro común ( w ), los caminos se unen en algún sucesor común. Esta noción puede refinarse como propiedad de un objeto particular w , y el sistema puede llamarse confluente si todos sus elementos son confluentes.${\displaystyle x{\stackrel {*}{\leftarrow }}w{\stackrel {*}{\rightarrow }}y}$${\displaystyle x{\mathbin {\downarrow }}y}$
• semi-confluentes si y sólo si para todo w , x , y y en A , implica . Esto se diferencia de la confluencia por la reducción de un solo paso de w a x .${\displaystyle x\leftarrow w{\stackrel {*}{\rightarrow }}y}$${\displaystyle x{\mathbin {\downarrow }}y}$
• confluentes localmente si y sólo si para todo w , x , y y en A , implica . Esta propiedad a veces se denomina confluencia débil .${\displaystyle x\leftarrow w\rightarrow y}$${\displaystyle x{\mathbin {\downarrow }}y}$

Ejemplo de un sistema de reescritura localmente confluente que no tiene la propiedad Church-Rosser

Teorema. Para un ARS, las siguientes tres condiciones son equivalentes: (i) tiene la propiedad Church-Rosser, (ii) es confluente, (iii) es semiconfluente. ^[8]

Corolario . ^[9] En un ARS confluente si entonces${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$

• Si tanto x como y son formas normales, entonces x = y .
• Si y es una forma normal, entonces${\displaystyle x{\stackrel {*}{\rightarrow }}y}$

Debido a estas equivalencias, en la literatura se encuentran algunas variaciones en las definiciones. Por ejemplo, en Terese la propiedad Church-Rosser y la confluencia se definen como sinónimos e idénticas a la definición de confluencia presentada aquí; Church-Rosser como se define aquí permanece sin nombre, pero se da como una propiedad equivalente; esta desviación de otros textos es deliberada. ^[10] Debido al corolario anterior, se puede definir una forma normal y de x como una y irreducible con la propiedad que . Esta definición, que se encuentra en Book y Otto, es equivalente a la común dada aquí en un sistema confluente, pero es más inclusiva en un ARS no confluente.${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$

La confluencia local, por otro lado, no es equivalente a las otras nociones de confluencia dadas en esta sección, pero es estrictamente más débil que la confluencia. El contraejemplo típico es , que es localmente confluente pero no confluente (ver imagen).${\displaystyle \{b\rightarrow c,c\rightarrow b,b\rightarrow a,c\rightarrow d\}}$

Terminación y convergencia

Se dice que un sistema de reescritura abstracto es terminante o noetheriano si no hay una cadena infinita . (Esto significa simplemente que la relación de reescritura es una relación noetheriana ). En un ARS de terminación, cada objeto tiene al menos una forma normal, por lo que se está normalizando. Lo contrario no es cierto. En el ejemplo 1, por ejemplo, hay una cadena de reescritura infinita, es decir , aunque el sistema se esté normalizando. Un ARS confluente y terminante se llama canónico , ^[11] o convergente${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$${\displaystyle a\rightarrow b\rightarrow a\rightarrow b\rightarrow \cdots }$. En un ARS convergente, cada objeto tiene una forma normal única. Pero es suficiente que el sistema confluya y se normalice para que exista una normal única para cada elemento, como se ve en el ejemplo 1.

Teorema ( Lema de Newman ): Un ARS terminante es confluente si y solo si es localmente confluente.

La prueba original de 1942 de este resultado por Newman fue bastante complicada. No fue hasta 1980 que Huet publicó una prueba mucho más simple explotando el hecho de que cuando está terminando podemos aplicar una inducción bien fundada . ^[12]${\displaystyle \rightarrow }$

Notas

1. Libro y Otto, p. 9
2. Terese, pág. 7,
3. Book y Otto, p. 10
4. Terese, p. 7-8
5. Baader y Nipkow, págs. 8-9
6. Iglesia de Alonzo y J. Barkley Rosser. Algunas propiedades de conversión. Trans. AMS, 39: 472-482, 1936
7. Baader y Nipkow, p. 9
8. Baader y Nipkow, p. 11
9. Baader y Nipkow, p. 12
10. Terese p.11
11. David A. Duffy (1991). Principios de la demostración automatizada de teoremas . Wiley. Aquí: sección 7.2.1, p.153
12. Harrison, pág. 260

Otras lecturas

• Baader, Franz ; Nipkow, Tobias (1998). Reescritura de términos y todo eso . Prensa de la Universidad de Cambridge. ISBN 9780521779203. Un libro de texto adecuado para estudiantes universitarios.
• Nachum Dershowitz y Jean-Pierre Jouannaud Rewrite Systems , Capítulo 6 en Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volumen B: Modelos formales y semántica. , Elsevier y MIT Press, 1990, ISBN 0-444-88074-7 , págs. 243-320. La preimpresión de este capítulo está disponible gratuitamente a través de los autores, pero faltan las cifras. 
• Ronald V. Book y Friedrich Otto, String-rewriting Systems , Springer (1993). Capítulo 1, "Sistemas de reducción abstracta"
• Marc Bezem , Jan Willem Klop , Roel de Vrijer ("Terese"), Sistemas de reescritura de términos , Cambridge University Press, 2003, ISBN 0-521-39115-6 , Capítulo 1. Ésta es una monografía completa. Sin embargo, utiliza una gran cantidad de notaciones y definiciones que no se encuentran comúnmente en otros lugares. Por ejemplo, la propiedad Church-Rosser se define como idéntica a la confluencia. 
• 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". Reescritura abstracta desde la perspectiva práctica de la resolución de problemas en lógica ecuacional . 
• 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. El artículo de Huet estableció muchos de los conceptos, resultados y notaciones modernos.
• Sinyor, J .; "El problema 3x + 1 como sistema de reescritura de cadenas" , Revista Internacional de Matemáticas y Ciencias Matemáticas , Volumen 2010 (2010), Artículo ID 458563, 6 páginas.