Reescritura

Para otros usos, consulte Reescritura (desambiguación) .

En matemáticas , ciencias de la computación y lógica , la reescritura cubre una amplia gama de métodos (potencialmente no deterministas ) para reemplazar los términos de una fórmula con otros términos. Los objetos de enfoque de este artículo incluyen sistemas de reescritura (también conocidos como sistemas de reescritura , motores de reescritura ^[1] o sistemas de reducción ). En su forma más básica, consisten en un conjunto de objetos, más relaciones sobre cómo transformar esos objetos.

La reescritura puede ser no determinista . Una regla para reescribir un término podría aplicarse de muchas formas diferentes a ese término, o podría aplicarse más de una regla. Los sistemas de reescritura no proporcionan un algoritmo para cambiar un término a otro, sino un conjunto de posibles aplicaciones de reglas. Sin embargo, cuando se combinan con un algoritmo apropiado, los sistemas de reescritura pueden verse como programas de computadora , y varios probadores de teoremas ^[2] y lenguajes de programación declarativos se basan en la reescritura de términos. ^{[3] [4]}

Casos de ejemplo

Lógica

En lógica , el procedimiento para obtener la forma normal conjuntiva (CNF) de una fórmula se puede implementar como un sistema de reescritura. ^[5] Las reglas de un ejemplo de tal sistema serían:

${\displaystyle \neg \neg A\to A}$( eliminación de la doble negación )

${\displaystyle \neg (A\land B)\to \neg A\lor \neg B}$( Leyes de De Morgan )

${\displaystyle \neg (A\lor B)\to \neg A\land \neg B}$

${\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)}$( distributividad )

${\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C),}$^{[nota 1]}

donde el símbolo ( ) indica que una expresión que coincida con el lado izquierdo de la regla se puede reescribir a una formada por el lado derecho, y cada uno de los símbolos denota una subexpresión. En tal sistema, cada regla se elige de modo que el lado izquierdo sea equivalente al lado derecho y, en consecuencia, cuando el lado izquierdo coincide con una subexpresión, realizar una reescritura de esa subexpresión de izquierda a derecha mantiene la coherencia lógica y el valor de toda la expresión. .${\displaystyle \to }$

Aritmética

Se pueden emplear sistemas de reescritura de términos para calcular operaciones aritméticas en números naturales . Con este fin, cada uno de esos números debe codificarse como un término . La codificación más simple es la utilizada en los axiomas de Peano , basado en la constante de 0 (cero) y la función sucesor S . por ejemplo, los números 0, 1, 2 y 3 están representados por los términos 0, S (0), S (S (0)) y S (S (S (0))), respectivamente. El siguiente término sistema de reescritura se puede utilizar para calcular la suma y el producto de números naturales dados. ^[6]

${\displaystyle {\begin{aligned}A+0&\to A&{\textrm {(1)}},\\A+S(B)&\to S(A+B)&{\textrm {(2)}},\\A\cdot 0&\to 0&{\textrm {(3)}},\\A\cdot S(B)&\to A+(A\cdot B)&{\textrm {(4)}}.\end{aligned}}}$

Por ejemplo, el cálculo de 2 + 2 para dar como resultado 4 se puede duplicar mediante la reescritura de términos de la siguiente manera:

${\displaystyle S(S(0))+S(S(0))}$ ${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$ ${\displaystyle S(\;S(S(0))+S(0)\;)}$ ${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$ ${\displaystyle S(S(\;S(S(0))+0\;))}$ ${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$ ${\displaystyle S(S(S(S(0)))),}$

donde los números de la regla se dan encima de la flecha de reescritura .

Como otro ejemplo, el cálculo de 2⋅2 se ve así:

${\displaystyle S(S(0))\cdot S(S(0))}$ ${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))\cdot S(0)}$ ${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))+S(S(0))\cdot 0}$ ${\displaystyle \;\;{\stackrel {(3)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))+0)}$ ${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))}$ ${\displaystyle \;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;}$ ${\displaystyle S(S(S(S(0)))),}$

donde el último paso comprende el cálculo del ejemplo anterior.

Lingüística

En lingüística , las reglas de reescritura , también llamadas reglas de estructura de frases , se utilizan en algunos sistemas de gramática generativa , ^[7] como un medio para generar las oraciones gramaticalmente correctas de un idioma. Dicha regla generalmente toma la forma A → X, donde A es una etiqueta de categoría sintáctica , como un sintagma nominal u oración , y X es una secuencia de tales etiquetas o morfemas , expresando el hecho de que A puede ser reemplazada por X al generar el estructura constituyente de una oración. Por ejemplo, la regla S → NP VP significa que una oración puede constar de un sintagma nominal seguido de un sintagma verbal.; más reglas especificarán en qué subconstituyentes pueden consistir un sintagma nominal y un sintagma verbal, y así sucesivamente.

Sistemas de reescritura abstracta

Artículo principal: Sistema de reescritura abstracta

De los ejemplos anteriores, está claro que podemos pensar en la reescritura de sistemas de una manera abstracta. Necesitamos especificar un conjunto de objetos y las reglas que se pueden aplicar para transformarlos. La configuración más general (unidimensional) de esta noción se denomina sistema de reducción abstracta (abreviado ARS ), aunque más recientemente los autores también utilizan el sistema de reescritura abstracta . ^[8] (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. Porque la palabra "reducción" no aparece en los nombres de sistemas más especializados,en los textos más antiguos sistema de reducción es sinónimo de ARS).^[9]

Un ARS es simplemente 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 ^[10] o simplemente reducción . ^[9] 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; esto se hará más evidente cuando analicemos los sistemas de reescritura de cadenas más en este artículo.

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 una y b de cualquier manera para obtener el término c . Esta propiedad es claramente importante. En cierto sentido, c es un término "más simple" en el sistema, ya que nada se puede aplicar a cpara transformarlo más. Este ejemplo nos lleva a definir algunas nociones importantes en el marco general de un ARS. Primero necesitamos algunas nociones y notaciones básicas. ^[11]

• ${\displaystyle {\stackrel {*}{\rightarrow }}}$es el cierre transitivo de , donde = es la relación de identidad , es decir, es el preorden más pequeño (relación reflexiva y transitiva ) que contiene . También se le llama cierre transitivo reflexivo de .${\displaystyle \rightarrow \cup =}$${\displaystyle {\stackrel {*}{\rightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle \rightarrow }$
• ${\displaystyle \leftrightarrow }$es decir , que es la unión de la relación → con su relación inversa , también conocida como cierre simétrico de .${\displaystyle \rightarrow \cup \ {\xrightarrow {-1}}}$${\displaystyle \rightarrow }$
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$es el cierre transitivo de , es decir, la relación de equivalencia más pequeña que contiene . También se conoce como cierre simétrico transitivo reflexivo de .${\displaystyle \leftrightarrow \cup =}$${\displaystyle {\stackrel {*}{\leftrightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle \rightarrow }$

Las formas normales, la articulación y el problema verbal

Un objeto x en A se llama reducible si existe algún otro y en A tal que ; de lo contrario, se llama irreductible o forma normal . Un objeto y se llama forma normal de x si , y y es irreducible. 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 }}$

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 es 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\downarrow y}$

Uno de los problemas importantes que se pueden formular en una ARS es la palabra problema : dado x y y , se encuentran 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, si dos objetos tienen la misma forma normal, entonces son equivalentes en . El problema verbal de un ARS es indecidible en general.${\displaystyle {\stackrel {*}{\,\leftrightarrow \,}}}$${\displaystyle {\stackrel {*}{\leftrightarrow }}}$

La propiedad y la confluencia Church-Rosser

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

Se dice que un ARS posee la propiedad Church-Rosser si lo implica . En palabras, la propiedad Church-Rosser significa que se pueden unir dos objetos equivalentes cualesquiera. Alonzo Church y J. Barkley Rosser demostraron en 1936 que el cálculo lambda tiene esta propiedad; ^{[12] de} ahí el nombre de la propiedad. ^[13] (El cálculo lambda tiene esta propiedad también se conoce como el teorema de Church-Rosser .) 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\downarrow y}$forma normal; esa es la forma normal de un objeto, es única si existe, pero puede que no exista.

Varias propiedades diferentes son equivalentes a la propiedad Church-Rosser, pero pueden ser más simples de verificar en algún entorno particular. En particular, la confluencia es equivalente a Church-Rosser. Un ARS se dice:${\displaystyle (A,\rightarrow )}$

• confluente 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\downarrow y}$
• confluentes localmente 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\downarrow y}$

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

Corolario . ^[15] 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 Bezem et al. 2003 la propiedad 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. ^[16] Debido al corolario anterior, en un ARS confluente 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 ^{[nota 2]}${\displaystyle x{\stackrel {*}{\,\leftrightarrow \,}}y}$ más en un ARS no confluente.

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. La relación es localmente confluente, pero no confluente, ya que y son equivalentes, pero no unibles. ^[17]${\displaystyle a\rightarrow b,\;b\rightarrow a,\;a\rightarrow c,\;b\rightarrow d}$${\displaystyle c}$${\displaystyle d}$

Terminación y convergencia

Se dice que un sistema de reescritura abstracto es terminante o noetheriano si no hay una cadena infinita . 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 terminal se llama convergente . En un ARS convergente, cada objeto tiene una forma normal única. ${\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 ): Un ARS terminante es confluente si y solo si es localmente confluente.

Sistemas de reescritura de cadenas

Artículo principal: Sistema de reescritura de cadenas

Un sistema de reescritura de cadenas (SRS), también conocido como sistema semi-Thue , explota la estructura monoide libre de las cadenas (palabras) sobre un alfabeto para extender una relación de reescritura , a todas las cadenas del alfabeto que contienen izquierda y derecha respectivamente. -Los lados de algunas reglas como subcadenas . Formalmente, un sistema semi-Thue es una tupla donde hay un alfabeto (generalmente finito) y es una relación binaria entre algunas cadenas (fijas) en el alfabeto, llamadas reglas de reescritura . El de un solo paso relación reescritura relación inducida por el${\displaystyle R}$ ${\displaystyle (\Sigma ,R)}$${\displaystyle \Sigma }$${\displaystyle R}$${\displaystyle {\xrightarrow[{R}]{}}}$${\displaystyle R}$${\displaystyle \Sigma ^{*}}$se define como: para cualquier cadena si y sólo si existen tales que , , y . Dado que es una relación de , el par se ajusta a la definición de un sistema de reescritura abstracta. Obviamente es un subconjunto de . Si la relación es simétrica , entonces el sistema se llama sistema Thue .${\displaystyle s,t\in \Sigma ^{*}}$ ${\displaystyle s\,{\xrightarrow[{R}]{}}\,t}$${\displaystyle x,y,u,v\in \Sigma ^{*}}$${\displaystyle s=xuy}$${\displaystyle t=xvy}$${\displaystyle uRv}$${\displaystyle {\xrightarrow[{R}]{}}}$${\displaystyle \Sigma ^{*}}$${\displaystyle (\Sigma ^{*},{\xrightarrow[{R}]{}})}$${\displaystyle R}$${\displaystyle {\xrightarrow[{R}]{}}}$${\displaystyle R}$

En un SRS, la relación de reducción es compatible con la operación monoide, lo que significa que implica para todas las cadenas . De manera similar, el cierre simétrico transitivo reflexivo de , denotado , es una congruencia , lo que significa que es una relación de equivalencia (por definición) y también es compatible con la concatenación de cadenas. La relación se llama congruencia Thue generada por . En un sistema Thue, es decir, si es simétrico, la relación de reescritura coincide con la congruencia Thue .${\displaystyle {\xrightarrow[{R}]{*}}}$${\displaystyle x\,{\xrightarrow[{R}]{*}}\,y}$${\displaystyle uxv\,{\xrightarrow[{R}]{*}}\,uyv}$${\displaystyle x,y,u,v\in \Sigma ^{*}}$${\displaystyle {\xrightarrow[{R}]{}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle R}$${\displaystyle R}$${\displaystyle {\xrightarrow[{R}]{*}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$

La noción de un sistema semi-Thue coincide esencialmente con la presentación de un monoide . Dado que es una congruencia, podemos definir el factor monoide del monoide libre por la congruencia de Thue de la manera habitual . Si un monoide es isomorfo con , entonces el sistema semi-Thue se denomina presentación monoide de .${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$ ${\displaystyle {\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle \Sigma ^{*}}$${\displaystyle {\mathcal {M}}}$${\displaystyle {\mathcal {M}}_{R}}$${\displaystyle (\Sigma ,R)}$${\displaystyle {\mathcal {M}}}$

Inmediatamente obtenemos algunas conexiones muy útiles con otras áreas del álgebra. Por ejemplo, el alfabeto { a , b } con las reglas { ab → ε, ba → ε}, donde ε es la cadena vacía , es una presentación del grupo libre en un generador. Si en cambio las reglas son solo { ab → ε}, entonces obtenemos una presentación del monoide bicíclico . Por lo tanto, los sistemas semi-Thue constituyen un marco natural para resolver el problema verbal de monoides y grupos. De hecho, cada monoide tiene una presentación de la forma , es decir, siempre puede presentarse mediante un sistema semi-Thue, posiblemente sobre un alfabeto infinito.${\displaystyle (\Sigma ,R)}$

El problema verbal para un sistema semi-Thue es indecidible en general; este resultado se conoce a veces como el teorema de Post-Markov . ^[18]

Sistemas de reescritura de términos

Esta sección necesita expansión . Puede ayudar agregando más . ( Octubre de 2009 )

Imagen 1: Diagrama de triángulo esquemático de la aplicación de una regla de reescritura en la posición de un término, con sustitución correspondiente${\displaystyle l\longrightarrow r}$${\displaystyle p}$${\displaystyle \sigma }$

Fig.2: Regla LHS término coincidente en plazo${\displaystyle x*(y*z)}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$

Un sistema de reescritura de términos ( TRS ) es un sistema de reescritura cuyos objetos son términos , que son expresiones con subexpresiones anidadas. Por ejemplo, el sistema que se muestra en § Lógica anterior es un sistema de reescritura de términos. Los términos de este sistema se componen de operadores binarios y y el operador unario . También están presentes en las reglas las variables, que representan cualquier término posible (aunque una sola variable siempre representa el mismo término en una sola regla).${\displaystyle (\vee )}$${\displaystyle (\wedge )}$${\displaystyle (\neg )}$

En contraste con los sistemas de reescritura de cadenas, cuyos objetos son secuencias de símbolos, los objetos de un sistema de reescritura de términos forman un álgebra de términos . Un término puede visualizarse como un árbol de símbolos, el conjunto de símbolos admitidos queda fijado por una firma determinada .

Definición formal

Una regla de reescritura de términos es un par de términos , comúnmente escritos como , para indicar que el lado izquierdo l puede ser reemplazado por el lado derecho r . Un sistema de reescritura de términos es un conjunto R de tales reglas. Se puede aplicar una regla a un término s si el término izquierdo l coincide con algún subtermo de s , es decir, si para alguna posición p en s y alguna sustitución . ^{[nota 3]} El término de resultado t${\displaystyle l\rightarrow r}$${\displaystyle l\rightarrow r}$ ${\displaystyle s|_{p}=l\sigma }$ ${\displaystyle \sigma }$de esta regla la aplicación se obtiene como ; ^{[nota 4]} ver imagen 1. En este caso, se dice que es reescrito en un solo paso , o reescrito directamente , a por el sistema , denotado formalmente como , o como por algunos autores.${\displaystyle t=s[r\sigma ]_{p}}$${\displaystyle s}$${\displaystyle t}$${\displaystyle R}$${\displaystyle s\rightarrow _{R}t}$${\displaystyle s\,{\xrightarrow[{R}]{}}\,t}$${\displaystyle s\,{\xrightarrow {R}}\,t}$

Si un término puede ser reescrita en varios pasos en un término , es decir, si el término se dice que está reescrito a , denotado formalmente como . En otras palabras, la relación es el cierre transitivo de la relación ; a menudo, también la notación se usa para denotar el cierre reflexivo-transitivo de , es decir, si s = t o . ^[19] Una reescritura de términos dada por un conjunto de reglas puede verse como un sistema de reescritura abstracto como se definió anteriormente , con términos como sus objetos y como su relación de reescritura.${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\displaystyle t_{1}\,{\xrightarrow[{R}]{}}\,t_{2}\,{\xrightarrow[{R}]{}}\,\ldots \,{\xrightarrow[{R}]{}}\,t_{n}}$${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\displaystyle t_{1}\,{\xrightarrow[{R}]{+}}\,t_{n}}$${\displaystyle {\xrightarrow[{R}]{+}}}$${\displaystyle {\xrightarrow[{R}]{}}}$${\displaystyle {\xrightarrow[{R}]{*}}}$${\displaystyle {\xrightarrow[{R}]{}}}$${\displaystyle s\,{\xrightarrow[{R}]{*}}\,t}$${\displaystyle s\,{\xrightarrow[{R}]{+}}\,t}$${\displaystyle R}$${\displaystyle {\xrightarrow[{R}]{}}}$

Por ejemplo, es una regla de reescritura, comúnmente utilizada para establecer una forma normal con respecto a la asociatividad de . Esa regla se puede aplicar en el numerador del término con la sustitución correspondiente , ver imagen 2. ^{[nota 5]} Al aplicar esa sustitución al lado derecho de la regla se obtiene el término ( a * ( a + 1)) * ( a + 2) , y reemplazar el numerador por ese término produce , que es el término resultante de aplicar la regla de reescritura. En total, la aplicación de la regla de reescritura ha logrado lo que se llama "la aplicación de la ley para la asociatividad de${\displaystyle x*(y*z)\rightarrow (x*y)*z}$${\displaystyle *}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$${\displaystyle \{x\mapsto a,\;y\mapsto a+1,\;z\mapsto a+2\}}$${\displaystyle {\frac {(a*(a+1))*(a+2)}{1*(2*3)}}}$${\displaystyle *}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$"en álgebra elemental. Alternativamente, la regla podría haberse aplicado al denominador del término original, ceder .${\displaystyle {\frac {a*((a+1)*(a+2))}{(1*2)*3}}}$

Terminación

Más allá de la sección Terminación y convergencia , se deben considerar sutilezas adicionales para los sistemas de reescritura de términos.

Incluso la terminación de un sistema que consta de una regla con un lado izquierdo lineal es indecidible. ^{[20] La} terminación también es indecidible para sistemas que utilizan únicamente símbolos de función unaria; sin embargo, es decidible para sistemas terrestres finitos .^[21]

El siguiente término sistema de reescritura se está normalizando, ^{[nota 6]} pero no termina, ^{[nota 7]} y no confluye: ^[22]

${\displaystyle f(x,x)\rightarrow g(x),}$

${\displaystyle f(x,g(x))\rightarrow b,}$

${\displaystyle h(c,x)\rightarrow f(h(x,c),h(x,x)).}$

Los siguientes dos ejemplos de sistemas de reescritura de términos terminados se deben a Toyama: ^[23]

${\displaystyle f(0,1,x)\rightarrow f(x,x,x)}$

y

${\displaystyle g(x,y)\rightarrow x,}$

${\displaystyle g(x,y)\rightarrow y.}$

Su unión es un sistema indeterminado, ya que . Este resultado refuta una conjetura de Dershowitz , ^[24] quien afirmó que la unión de dos sistemas de reescritura de términos terminantes y está nuevamente terminando si todos los lados izquierdo y derecho de son lineales , y no hay " superposiciones " entre lados izquierdos y lados derechos de . Todas estas propiedades quedan satisfechas con los ejemplos de Toyama.${\displaystyle f(g(0,1),g(0,1),g(0,1))\rightarrow f(0,g(0,1),g(0,1))\rightarrow f(0,1,g(0,1))\rightarrow f(g(0,1),g(0,1),g(0,1))\rightarrow \ldots }$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$

Consulte Orden de reescritura y Orden de ruta (reescritura de términos) para ordenar las relaciones utilizadas en las pruebas de terminación para los sistemas de reescritura de términos.

Sistemas de reescritura de gráficos

Una generalización de los sistemas de reescritura de términos son los sistemas de reescritura de gráficos , que operan en gráficos en lugar de términos ( básicos ) / su correspondiente representación de árbol .

Sistemas de reescritura de seguimiento

La teoría de trazas proporciona un medio para discutir el multiprocesamiento en términos más formales, como a través del monoide de trazas y el monoide de historia . La reescritura también se puede realizar en sistemas de seguimiento.

Filosofía

Los sistemas de reescritura pueden verse como programas que infieren efectos finales a partir de una lista de relaciones causa-efecto. De esta manera, los sistemas de reescritura pueden considerarse como probadores de causalidad automatizados . ^{[ cita requerida ]}

Ver también

• Par crítico (lógica)
• Algoritmo de finalización de Knuth-Bendix
• Los sistemas L especifican la reescritura que se realiza en paralelo.
• Transparencia referencial en informática
• Reescritura regulada
• Cálculo de Rho

Notas

1. Esta variante de la regla anterior es necesaria ya que la ley conmutativa A ∨ B = B ∨ A no se puede convertir en una regla de reescritura. Una regla como A ∨ B → B ∨ A causaría que el sistema de reescritura no sea final.
2. es decir, considera más objetos como una forma normal de x que nuestra definición
3. aquí,denota el subtermo dearraigado en la posición p , mientras quedenota el resultado de aplicar la sustitución al término 1${\displaystyle s\mid _{p}}$${\displaystyle s}$${\displaystyle l\sigma }$ ${\displaystyle \sigma }$
4. aquí,denota el resultado de reemplazar el subtermo en la posición p en s por el término ${\displaystyle s[r\sigma ]_{p}}$${\displaystyle r\sigma }$
5. ya que al aplicar esa sustitución al lado izquierdo de la regla seobtiene el numerador${\displaystyle x*(y*z)}$${\displaystyle a*((a+1)*(a+2))}$
6. Es decir, para cada término, existe alguna forma normal, por ejemplo, h ( c , c ) tiene las formas normales b y g ( b ), ya que h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( h ( c , c ), f ( h ( c , c ), h ( c ,c ))) → f ( h ( c , c ), g ( h ( c , c ))) → b y h ( c , c ) → f ( h ( c , c ), h ( c , c ) ) → g ( h ( c , c ), h ( c , c )) → ... → g ( b ); ninguno de los dosb ni g ( b ) se pueden reescribir más, por lo tanto, el sistema no es confluente
7. es decir, hay infinitas derivaciones, p. ej. h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( f ( h ( c , c ), h ( c , c ) ), h ( c , c )) → f ( f ( f ( h ( c , c ), h( c , c )), h ( c , c )), h ( c , c )) → ...

Referencias

1. Sculthorpe, Neil; Frisby, Nicolas; Gill, Andy (2014). "El motor de reescritura de la Universidad de Kansas" (PDF) . Revista de programación funcional . 24 (4): 434–473. doi : 10.1017 / S0956796814000185 . ISSN  0956-7968 .
2. Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël (1992). "El enfoque de reescritura de término para demostrar teoremas automatizados". El diario de la programación lógica . 14 (1–2): 71–99. doi : 10.1016 / 0743-1066 (92) 90047-7 .
3. Frühwirth, Thom (1998). "Teoría y práctica de las reglas de manejo de restricciones". El diario de la programación lógica . 37 (1-3): 95-138. doi : 10.1016 / S0743-1066 (98) 10005-5 .
4. Clavel, M .; Durán, F .; Eker, S .; Lincoln, P .; Martí-Oliet, N .; Meseguer, J .; Quesada, JF (2002). "Maude: Especificación y programación en la reescritura de la lógica". Informática Teórica . 285 (2): 187–243. doi : 10.1016 / S0304-3975 (01) 00359-0 .
5. Kim Marriott; Peter J. Stuckey (1998). Programación con restricciones: una introducción . MIT Press. págs. 436–. ISBN 978-0-262-13341-8.
6. Jürgen Avenhaus; Klaus Madlener (1990). "Reescritura de términos y razonamiento ecuacional". En RB Banerji (ed.). Técnicas formales en inteligencia artificial . Libro de consulta. Elsevier. págs. 1-43. Aquí: Ejemplo en la sección 4.1, p.24.
7. Robert Freidin (1992). Fundamentos de la sintaxis generativa . MIT Press. ISBN 978-0-262-06144-5.
8. Bezem y col., P. 7,
9. Book y Otto, p. 10
10. Bezem y col., P. 7
11. Baader y Nipkow, págs. 8–9
12. Iglesia de Alonzo y J. Barkley Rosser. "Algunas propiedades de conversión". Trans. AMS , 39: 472–482, 1936
13. Baader y Nipkow, p. 9
14. Baader y Nipkow, p. 11
15. Baader y Nipkow, p. 12
16. Bezem et al., P.11
17. MHA Neumann (1942). "Sobre teorías con una definición combinatoria de equivalencia ". Annals of Mathematics . 42 (2): 223–243. doi : 10.2307 / 1968867 . JSTOR 1968867 . 
18. Martin Davis y col. 1994, pág. 178
19. N. Dershowitz, J.-P. Jouannaud (1990). Jan van Leeuwen (ed.). Reescribir sistemas . Manual de Informática Teórica. B . Elsevier. págs. 243–320.; aquí: Sect. 2.3
20. M. Dauchet (1989). "Simulación de máquinas de Turing por una regla de reescritura lineal a la izquierda". Proc. 3er RTA . LNCS. 355 . Springer LNCS. págs. 109-120.
21. Gerard Huet, DS Lankford (marzo de 1978). Sobre el problema de detención uniforme para los sistemas de reescritura de términos (PDF) (Informe técnico). IRIA. pag. 8. 283 . Consultado el 16 de junio de 2013 .
22. Bernhard Gramlich (junio de 1993). "Relacionando la terminación más interna, débil, uniforme y modular de los sistemas de reescritura de términos" . En Voronkov, Andrei (ed.). Proc. Congreso Internacional de Programación Lógica y Razonamiento Automatizado (LPAR) . LNAI. 624 . Saltador. págs. 285-296. Aquí: Ejemplo 3.3
23. Yoshihito Toyama (1987). "Contraejemplos a la rescisión por la suma directa de sistemas de reescritura de términos" (PDF) . Inf. Proceso. Lett . 25 (3): 141-143. doi : 10.1016 / 0020-0190 (87) 90122-0 . hdl : 2433/99946 .
24. N. Dershowitz (1985). "Terminación" (PDF) . En Jean-Pierre Jouannaud (ed.). Proc. RTA . LNCS. 220 . Saltador. págs. 180–224. ; aquí: p.210

Lectura adicional

• Baader, Franz ; Nipkow, Tobias (1999). Término reescrito y todo eso . Prensa de la Universidad de Cambridge. ISBN 978-0-521-77920-3.316 páginas. Un libro de texto adecuado para estudiantes universitarios.
• Marc Bezem , Jan Willem Klop , Roel de Vrijer ("Terese"), Term Rewriting Systems ("TeReSe"), Cambridge University Press, 2003, ISBN 0-521-39115-6 . Ésta es la monografía completa más reciente. Sin embargo, utiliza una buena cantidad de anotaciones y definiciones que aún no son estándar. Por ejemplo, la propiedad Church-Rosser se define como idéntica a la confluencia. 
• Nachum Dershowitz y Jean-Pierre Jouannaud "Rewrite Systems" , 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 preimpresión de este capítulo está disponible gratuitamente para los autores, pero faltan las figuras. 
• Nachum Dershowitz y David Plaisted . "Reescritura" , Capítulo 9 de John Alan Robinson y Andrei Voronkov (Eds.), Manual de razonamiento automatizado , Volumen 1 .
• Gérard Huet et Derek Oppen, Equations and Rewrite Rules, A Survey (1980) Stanford Verification Group, Informe N ° 15 Informe del Departamento de Ciencias de la Computación N ° STAN-CS-80-785
• Jan Willem Klop . "Term Rewriting Systems", Capítulo 1 en Samson Abramsky , Dov M. Gabbay y Tom Maibaum (Eds.), Handbook of Logic in Computer Science , Volumen 2: Antecedentes: Estructuras computacionales .
• David Plaisted. "Sistemas de razonamiento ecuacional y reescritura de términos" , en Dov M. Gabbay , CJ Hogger y John Alan Robinson (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming , Volumen 1 .
• Jürgen Avenhaus y Klaus Madlener. "Reescritura de términos y razonamiento ecuacional". En Ranan B. Banerji (Ed.), Técnicas formales en inteligencia artificial: Libro de consulta , Elsevier (1990).

Reescritura de cadenas

• Ronald V. Book y Friedrich Otto, String-Rewriting Systems , Springer (1993).
• Benjamin Benninghofen, Susanne Kemmerich y Michael M. Richter , Sistemas de reducciones . LNCS 277 , Springer-Verlag (1987).

Otro

• Martin Davis , Ron Sigal , Elaine J. Weyuker , (1994) Computabilidad, complejidad y lenguajes: Fundamentos de la informática teórica - 2da edición , Academic Press, ISBN 0-12-206382-1 . 

Enlaces externos

Busque reescritura en Wiktionary, el diccionario gratuito.

• La página de inicio de reescritura
• Grupo de trabajo IFIP 1.6
• Investigadores en reescritura por Aart Middeldorp , Universidad de Innsbruck
• Portal de terminación