Sistema de reescritura abstracta

En lógica matemática y ciencias de la computación teórica , 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${\displaystyle \rightarrow }$Esta definición puede refinarse 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 las formas normales , la terminación y diversas nociones de confluencia .

Históricamente, ha habido varias formalizaciones de la reescritura en un contexto abstracto, cada una con sus particularidades. Esto se debe en parte a que algunas nociones son equivalentes (véase más adelante en este artículo). La formalización más común en monografías y libros de texto, y que generalmente se sigue aquí, es la de Gérard Huet (1980). ^{[ 1 ]}

Un sistema de reducción abstracto ( SAR ) es la noción más general (unidimensional) para especificar un conjunto de objetos y reglas que se pueden aplicar para transformarlos. Más recientemente, algunos autores también utilizan el término sistema de reescritura abstracto . ^{[ 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 los sistemas que son particularizaciones de SAR. Dado que la palabra "reducción" no aparece en los nombres de sistemas más especializados, en textos antiguos " sistema de reducción" es sinónimo de SAR). ^{[ 3 ]}

Un ARS es un conjunto A , cuyos elementos suelen llamarse 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 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${\displaystyle {\rightarrow _{1}\cup \rightarrow _{2}}={\rightarrow }}$, la notación utilizada es (A, → ₁ , → ₂ ).

Como objeto matemático , un ARS es exactamente igual a un sistema de transición de estados sin etiquetar , y si la relación se considera como una unión indexada, entonces un ARS es igual a 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, el interés radica 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 ]}

Supongamos que el conjunto de objetos es T = { a , b , c } y que la relación binaria viene 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 aún más. Esta propiedad es claramente importante.

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${\displaystyle \rightarrow }$, es decir, el cierre transitivo de${\displaystyle (\rightarrow )\cup (=)}$, donde = es la relación de identidad . Equivalentemente,${\displaystyle {\stackrel {*}{\rightarrow }}}$es el pedido anticipado más pequeño que contiene${\displaystyle \rightarrow }$.
• Similarmente,${\displaystyle {\stackrel {+}{\leftarrow }}}$, y${\displaystyle {\stackrel {*}{\leftarrow }}}$son cierres de${\displaystyle {\leftarrow }}$, la relación inversa de${\displaystyle {\rightarrow }}$.
• ${\displaystyle \leftrightarrow }$es el cierre simétrico de${\displaystyle \rightarrow }$, es decir, la unión de${\displaystyle \rightarrow }$con${\displaystyle {\leftarrow }}$.
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$es el cierre simétrico transitivo reflexivo de${\displaystyle \rightarrow }$, es decir, el cierre transitivo de${\displaystyle (\leftrightarrow )\cup (=)}$. De forma equivalente,${\displaystyle {\stackrel {*}{\leftrightarrow }}}$es la relación de equivalencia más pequeña que contiene${\displaystyle \rightarrow }$.

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

Una noción relacionada, pero más débil que la existencia de formas normales, es la de dos objetos que se pueden unir : se dice que x e y se pueden unir si existe algún z con la propiedad de que${\displaystyle x{\stackrel {*}{\rightarrow }}z{\stackrel {*}{\leftarrow }}y}$. A partir de esta definición, resulta evidente que se puede definir la relación de unión como${\displaystyle {\stackrel {*}{\rightarrow }}\circ {\stackrel {*}{\leftarrow }}}$, dónde${\displaystyle \circ }$es la composición de relaciones . La capacidad de unión se suele denotar, de forma algo confusa, también con${\displaystyle \downarrow }$, pero en esta notación la flecha hacia abajo es una relación binaria, es decir escribimos${\displaystyle x\mathrel {\downarrow } y}$si x e y se pueden unir.

Se dice que un ARS posee la propiedad Church-Rosser si y solo si${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$implica${\displaystyle x\mathrel {\downarrow } y}$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 unibilidad. 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 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 puede no existir.

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

• confluente si y solo si para todo w , x , e y en A , ${\displaystyle x{\stackrel {*}{\leftarrow }}w{\stackrel {*}{\rightarrow }}y}$implica${\displaystyle x\mathrel {\downarrow } y}$En términos generales, la confluencia implica que, independientemente de cómo se separen dos caminos de un ancestro común ( w ), ambos convergen en algún sucesor común. Esta noción puede refinarse como una propiedad de un objeto particular w , y el sistema se denomina confluente si todos sus elementos lo son.
• semiconfluente si y solo si para todo w , x , e y en A , ${\displaystyle x\leftarrow w{\stackrel {*}{\rightarrow }}y}$implica${\displaystyle x\mathrel {\downarrow } y}$. Esto difiere de la confluencia por la reducción en un solo paso de w a x .
• localmente confluente si y solo si para todo w , x , e y en A , ${\displaystyle x\leftarrow w\rightarrow y}$implica${\displaystyle x\mathrel {\downarrow } y}$Esta propiedad a veces se denomina confluencia débil .

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

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

• 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, 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 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${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$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.

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

Se dice que un sistema de reescritura abstracto es terminante o noetheriano si no hay una cadena infinita.${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$(Esto simplemente significa que la relación de reescritura es una relación noetheriana ). En una ARS terminante, cada objeto tiene al menos una forma normal, por lo tanto, es normalizadora. Lo contrario no es cierto. En el ejemplo 1, por ejemplo, hay una cadena de reescritura infinita, a saber:${\displaystyle a\rightarrow b\rightarrow a\rightarrow b\rightarrow \cdots }$, aunque el sistema se esté normalizando. Un ARS confluente y terminante se denomina canónico , ^{[ 11 ]} o convergente . En un ARS convergente, cada objeto tiene una forma normal única. Pero basta con que el sistema sea confluente y se esté normalizando para que exista una forma 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 demostración original de este resultado realizada por Newman en 1942 fue bastante complicada. No fue hasta 1980 que Huet publicó una demostración mucho más simple que explotaba el hecho de que cuando${\displaystyle \rightarrow }$es terminante podemos aplicar inducción bien fundamentada . ^{[ 12 ]}

• Problema verbal (matemáticas) — en particular la sección sobre sistemas de reescritura abstractos

• Baader, Franz ; Nipkow, Tobias (1998). Term Rewriting and All That . Cambridge University Press. ISBN 9780521779203.Un libro de texto adecuado para estudiantes de pregrado.
• Nachum Dershowitz y Jean-Pierre Jouannaud, Sistemas de reescritura , Capítulo 6 en Jan van Leeuwen (Ed.), Manual de informática teórica, Volumen B: Modelos formales y semántica , Elsevier y MIT Press, 1990, ISBN 0-444-88074-7, págs.  243 – 320. La versión preliminar de este capítulo está disponible gratuitamente a través de los autores, pero no incluye las figuras.
• Book, 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. Sin embargo, utiliza una cantidad considerable de notaciones y definiciones que no se encuentran habitualmente en otras fuentes. 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 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 un sistema de reescritura de cadenas" , Revista Internacional de Matemáticas y Ciencias Matemáticas , Volumen 2010 (2010), Artículo ID 458563, 6 páginas.
• Duffy, David A. (1991). Principios de la demostración automatizada de teoremas . Wiley.
• Church, Alonzo; Rosser, JB (1936). "Algunas propiedades de la conversión" . Transactions of the American Mathematical Society . 39 (3): 472– 482. doi : 10.2307/1989762 . ISSN 0002-9947 . JSTOR 1989762 .