Sistema de reescritura de resúmenes

Sistema formal para transcribir expresiones en términos equivalentes

En lógica matemática y ciencias de la computación teóricas , un sistema de reescritura abstracto (también sistema de reducción (abstracto) o sistema de reescritura abstracto ; abreviado ARS ) es un formalismo que captura la noción y las propiedades esenciales 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 los sistemas de reescritura como formas normales , terminación y varias nociones de confluencia . ${\displaystyle \rightarrow }$

Históricamente, ha habido varias formalizaciones de la reescritura en un contexto abstracto, cada una con sus idiosincrasias. Esto se debe en parte al hecho de que algunas nociones son equivalentes (véase más adelante en este artículo). La formalización que se encuentra con más frecuencia 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 abstracto . ^[2] (La preferencia por la palabra "reducción" aquí en lugar de "reescritura" constituye una desviación del uso uniforme de "reescritura" en los nombres de sistemas que son particularizaciones de ARS. Debido a que la palabra "reducción" no aparece en los nombres de sistemas más especializados, en textos más antiguos sistema de reducción es un sinónimo de ARS.) ^[3]

Un ARS es un conjunto A , cuyos elementos se denominan habitualmente 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 utiliza "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 constar de 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 estados sin etiquetas , 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 estados etiquetado, donde los índices son las etiquetas. Sin embargo, el enfoque del estudio y la terminología son diferentes. En un sistema de transición de estados , 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 que la relación binaria está dada por las reglas a → b , b → a , a → c y b → c . Observemos 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 básicas

Primero definamos 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 a . ${\displaystyle \rightarrow }$ ${\displaystyle (\rightarrow )\cup (=)}$ ${\displaystyle {\stackrel {*}{\rightarrow }}}$ ${\displaystyle \rightarrow }$
• De manera similar, , y son cierres de , la relación inversa de . ${\displaystyle {\stackrel {+}{\leftarrow }}}$ ${\displaystyle {\stackrel {*}{\leftarrow }}}$ ${\displaystyle {\leftarrow }}$ ${\displaystyle {\rightarrow }}$
• ${\displaystyle \leftrightarrow }$es el cierre simétrico de , es decir, la unión de con . ${\displaystyle \rightarrow }$ ${\displaystyle \rightarrow }$ ${\displaystyle {\leftarrow }}$
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$es la clausura simétrica transitiva reflexiva de , es decir, la clausura transitiva 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

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

Capacidad de unirse

Una noción relacionada, pero más débil que la existencia de formas normales, es la de que dos objetos son unibles : se dice que x e y 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 unibilidad como , donde es la composición de relaciones . La unibilidad suele denotarse, de forma algo confusa, 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 unibles. ${\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 de Church-Rosser y las nociones de confluencia

Se dice que un ARS posee la propiedad de Church-Rosser si y solo si implica para todos los objetos x , y . Equivalentemente, la propiedad de 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 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. ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$ ${\displaystyle x{\mathbin {\downarrow }}y}$

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

• confluente si y solo si para todos w , x e y en A , implica . En términos generales, la confluencia dice que no importa cómo diverjan dos caminos 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}$
• semiconfluente si y solo si para todos w , x e y en A , implica . Esto difiere 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}$
• localmente confluente si y solo si para todos w , x e 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 con confluencia local que no tiene la propiedad de Church-Rosser

Teorema. Para un ARS las tres condiciones siguientes son equivalentes: (i) tiene la propiedad de 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 encuentra una variación considerable en las definiciones. 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í; la propiedad de 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] Debido al corolario anterior, se puede definir una forma normal y de x como una y irreducible con la propiedad de que . Esta definición, que se encuentra en Book y Otto, es equivalente a la común que se da aquí en un sistema confluente, pero es más inclusiva en un ARS no confluente. ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$

Por otra parte, la confluencia local no es equivalente a las otras nociones de confluencia que se dan 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 (véase la 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 terminal o noetheriano si no hay una cadena infinita . (Esto simplemente dice que la relación de reescritura es una relación noetheriana ). En un SRA terminal, cada objeto tiene al menos una forma normal, por lo tanto, es normalizante. Lo inverso no es cierto. En el ejemplo 1, por ejemplo, hay una cadena de reescritura infinita, a saber , aunque el sistema se esté normalizando. Un SRA confluente y terminal se llama canónico , ^[11] o convergente . En un SRA convergente, cada objeto tiene una forma normal única. Pero es suficiente que el sistema sea confluente y normalizante para que exista una normal única para cada elemento, como se ve en el ejemplo 1. ${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$ ${\displaystyle a\rightarrow b\rightarrow a\rightarrow b\rightarrow \cdots }$

Teorema ( Lema de Newman ): Una ARS terminal es confluente si y sólo si es localmente confluente.

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

Véase también

• Problema de palabras (matemáticas) , en particular la sección sobre sistemas de reescritura abstracta

Notas

1. Libro y Otto 1993, pág. 9
2. Terese 2003, pág. 7
3. Book & Otto 1993, pág. 10
4. Terese 2003, págs. 7-8
5. Baader y Nipkow 1998, págs. 8-9
6. Iglesia y Rosser 1936
7. Baader y Nipkow 1998, pág. 9
8. Baader y Nipkow 1998, pág. 11
9. Baader y Nipkow 1998, pág. 12
10. Terese 2003, pág. 11
11. Duffy 1991, pág. 153, sección 7.2.1
12. Harrison 2009, pág. 260

Referencias

• Baader, Franz ; Nipkow, Tobias (1998). Reescritura de términos y todo eso. Cambridge University Press. 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, Volume B: Formal Models and Semantics , Elsevier y MIT Press, 1990, ISBN 0-444-88074-7 , pp. 243–320. La preimpresión de este capítulo está disponible gratuitamente a través de los autores, pero faltan las figuras. 
• Libro, Ronald V. ; Otto, Friedrich (1993). "1, "Sistemas de reducción abstracta"". Sistemas de reescritura de cadenas . Springer. ISBN 0-387-97965-4.
• Marc Bézem; Jan Willem Klop ; Roel de Vrijer; Terese (2003). "1". Sistemas de reescritura de términos . Prensa de la Universidad de Cambridge. ISBN 0-521-39115-6.Se trata de una monografía exhaustiva, pero utiliza una buena cantidad de notaciones y definiciones que no se encuentran comúnmente en otros lugares. Por ejemplo, la propiedad de Church-Rosser se define como idéntica a la confluencia.
• Harrison, John (2009). "4 "Igualdad"". Manual de lógica práctica y razonamiento automatizado Cambridge University Press . ISBN 978-0-521-89957-4.Reescritura abstracta desde la perspectiva práctica de la solución de problemas en lógica ecuacional .
• Gérard Huet , Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems , 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 un sistema de reescritura de cadenas", Revista Internacional de Matemáticas y Ciencias Matemáticas , Volumen 2010 (2010), ID de artículo 458563, 6 páginas.
• Duffy, David A. (1991). Principios de demostración automática de teoremas . Wiley.
• Church, Alonzo; Rosser, JB (1936). "Algunas propiedades de la conversión". Transacciones de la American Mathematical Society . 39 (3): 472–482. doi : 10.2307/1989762 . ISSN  0002-9947. JSTOR  1989762.