Reescritura

Reemplazar un subtérmino en una fórmula por otro término

En matemáticas , informática y lógica , la reescritura abarca una amplia gama de métodos para reemplazar subtérminos de una fórmula por otros términos. Dichos métodos pueden lograrse mediante sistemas de reescritura (también conocidos como sistemas de reescritura , motores de reescritura [ ^{1] [2]} 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 maneras 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 por otro, sino un conjunto de posibles aplicaciones de la regla. Sin embargo, cuando se combinan con un algoritmo apropiado, los sistemas de reescritura pueden verse como programas de computadora , y varios demostradores de teoremas ^[3] y lenguajes de programación declarativos se basan en la reescritura de términos. ^{[4] [5]}

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. ^[6] Las reglas de un ejemplo de dicho sistema serían:

${\displaystyle \neg \neg A\to A}$( eliminación de 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 coincide con el lado izquierdo de la regla se puede reescribir en una formada por el lado derecho, y cada símbolo denota una subexpresión. En un sistema de este tipo, 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

Los sistemas de reescritura de términos se pueden emplear para calcular operaciones aritméticas con números naturales . Para ello, 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 , basada en la constante 0 (cero) y la función sucesora S. Por ejemplo, los números 0, 1, 2 y 3 se representan mediante los términos 0, S(0), S(S(0)) y S(S(S(0))), respectivamente. El siguiente sistema de reescritura de términos se puede utilizar entonces para calcular la suma y el producto de números naturales dados. ^[7]

${\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 obtener 4 se puede duplicar reescribiendo los 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 las reglas 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 estructura de frases , también llamadas reglas de reescritura , se utilizan en algunos sistemas de gramática generativa , ^[8] como un medio para generar las oraciones gramaticalmente correctas de un idioma. Dicha regla generalmente toma la forma , donde A es una etiqueta de categoría sintáctica , como frase nominal u oración , y X es una secuencia de tales etiquetas o morfemas , que expresan el hecho de que A puede reemplazarse por X para generar la estructura constituyente de una oración. Por ejemplo, la regla significa que una oración puede constar de una frase nominal (SN) seguida de una frase verbal (VV); otras reglas especificarán de qué subconstituyentes puede constar una frase nominal y una frase verbal, y así sucesivamente. ${\displaystyle {\rm {A\rightarrow X}}}$ ${\displaystyle {\rm {S\rightarrow NP\ VP}}}$

Sistemas de reescritura de resúmenes

De los ejemplos anteriores, resulta claro que podemos pensar en sistemas de reescritura 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 abstracto ^[9] o sistema de reescritura abstracto (abreviado ARS ). ^[10] Un ARS es simplemente un conjunto A de objetos, junto con una relación binaria → en A llamada relación de reducción , relación de reescritura ^[11] o simplemente reducción . ^[9]

En el contexto general de una ARS se pueden definir muchas nociones y notaciones. es la clausura transitiva reflexiva de . es la clausura simétrica de . es la clausura simétrica transitiva reflexiva de . El problema verbal para una ARS es determinar, dadas x e y , si . Un objeto x en A se llama reducible si existe alguna otra y en A tal que ; de lo contrario, se llama irreducible o una forma normal . Un objeto y se llama una "forma normal de x " si , e y es irreducible. Si la forma normal de x es única, esto generalmente se denota con . Si cada objeto tiene al menos una forma normal, la ARS se llama normalizante . o se dice que x e y son unibles si existe alguna z con la propiedad de que . Se dice que una ARS posee la propiedad de Church-Rosser si implica . Una ARS es confluente si para todo w , x e y en A , implica . Una ARS es localmente confluente si y solo si para todos los w , x e y en A , implica . Se dice que una ARS es terminal o noetheriana si no hay una cadena infinita . Una ARS confluente y terminal se llama convergente o canónica . ${\displaystyle {\overset {*}{\rightarrow }}}$ ${\displaystyle \rightarrow }$ ${\displaystyle \leftrightarrow }$ ${\displaystyle \rightarrow }$ ${\displaystyle {\overset {*}{\leftrightarrow }}}$ ${\displaystyle \rightarrow }$ ${\displaystyle x{\overset {*}{\leftrightarrow }}y}$ ${\displaystyle x\rightarrow y}$ ${\displaystyle x{\stackrel {*}{\rightarrow }}y}$ ${\displaystyle x{\downarrow }}$ ${\displaystyle x\downarrow y}$ ${\displaystyle x{\overset {*}{\rightarrow }}z{\overset {*}{\leftarrow }}y}$ ${\displaystyle x{\overset {*}{\leftrightarrow }}y}$ ${\displaystyle x\downarrow y}$ ${\displaystyle x{\overset {*}{\leftarrow }}w{\overset {*}{\rightarrow }}y}$ ${\displaystyle x\downarrow y}$ ${\displaystyle x\leftarrow w\rightarrow y}$ ${\displaystyle x{\mathbin {\downarrow }}y}$ ${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$

Los teoremas importantes para los sistemas de reescritura abstracta son que un ARS es confluente si y solo si tiene la propiedad de Church-Rosser, el lema de Newman (un ARS terminal es confluente si y solo si es localmente confluente) y que el problema verbal para un ARS es indecidible en general.

Sistemas 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 en el alfabeto que contienen lados izquierdo y derecho respectivamente de algunas reglas como subcadenas . Formalmente, un sistema semi-Thue es una tupla donde es un alfabeto (generalmente finito), y es una relación binaria entre algunas cadenas (fijas) en el alfabeto, llamadas el conjunto de reglas de reescritura . La relación de reescritura de un paso inducida por en se define como: si son cadenas cualesquiera, entonces si existen tales que , , y . Dado que es una relación en , el par se ajusta a la definición de un sistema de reescritura abstracto. Dado que la cadena vacía está en , es un subconjunto de . Si la relación es simétrica , entonces el sistema se llama un sistema Thue . ${\displaystyle R}$ ${\displaystyle (\Sigma ,R)}$ ${\displaystyle \Sigma }$ ${\displaystyle R}$ ${\displaystyle {\underset {R}{\rightarrow }}}$ ${\displaystyle R}$ ${\displaystyle \Sigma ^{*}}$ ${\displaystyle s,t\in \Sigma ^{*}}$ ${\displaystyle s{\underset {R}{\rightarrow }}t}$ ${\displaystyle x,y,u,v\in \Sigma ^{*}}$ ${\displaystyle s=xuy}$ ${\displaystyle t=xvy}$ ${\displaystyle uRv}$ ${\displaystyle {\underset {R}{\rightarrow }}}$ ${\displaystyle \Sigma ^{*}}$ ${\displaystyle (\Sigma ^{*},{\underset {R}{\rightarrow }})}$ ${\displaystyle \Sigma ^{*}}$ ${\displaystyle R}$ ${\displaystyle {\underset {R}{\rightarrow }}}$ ${\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 de Thue generada por . En un sistema de Thue, es decir, si es simétrico, la relación de reescritura coincide con la congruencia de Thue . ${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$ ${\displaystyle x{\overset {*}{\underset {R}{\rightarrow }}}y}$ ${\displaystyle uxv{\overset {*}{\underset {R}{\rightarrow }}}uyv}$ ${\displaystyle x,y,u,v\in \Sigma ^{*}}$ ${\displaystyle {\underset {R}{\rightarrow }}}$ ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$ ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$ ${\displaystyle R}$ ${\displaystyle R}$ ${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$ ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$

La noción de un sistema semi-Thue coincide esencialmente con la presentación de un monoide . Como es una congruencia, podemos definir el monoide factorial del monoide libre por la congruencia de Thue. 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 con las reglas , donde es la cadena vacía , es una presentación del grupo libre en un generador. Si en cambio las reglas son solo , 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 para 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 \{a,b\}}$ ${\displaystyle \{ab\rightarrow \varepsilon ,ba\rightarrow \varepsilon \}}$ ${\displaystyle \varepsilon }$ ${\displaystyle \{ab\rightarrow \varepsilon \}}$ ${\displaystyle (\Sigma ,R)}$

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

Sistemas de reescritura de términos

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

Imagen 2: Regla de coincidencia de términos de la izquierda en el término ${\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 el apartado Lógica anterior es un sistema de reescritura de términos. Los términos de este sistema están compuestos por 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 única variable siempre representa el mismo término a lo largo de una única regla). ${\displaystyle (\vee )}$ ${\displaystyle (\wedge )}$ ${\displaystyle (\neg )}$

A diferencia de 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, siendo el conjunto de símbolos admitidos fijado por una signatura dada . Como formalismo, los sistemas de reescritura de términos tienen todo el poder de las máquinas de Turing , es decir, cada función computable puede definirse mediante un sistema de reescritura de términos. ^[13]

Algunos lenguajes de programación se basan en la reescritura de términos. Un ejemplo de ello es Pure, un lenguaje de programación funcional para aplicaciones matemáticas. ^{[14] [15]}

Definición formal

Una regla de reescritura 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. Una regla puede aplicarse a un término s si el término izquierdo l coincide con algún subtérmino de s , es decir, si hay alguna sustitución tal que el subtérmino de enraizado en alguna posición p es el resultado de aplicar la sustitución al término l . El subtérmino que coincide con el lado izquierdo de la regla se llama redex o expresión reducible . ^[16] El término resultante t de esta aplicación de la regla es entonces el resultado de reemplazar el subtérmino en la posición p en s por el término con la sustitución aplicada, vea la imagen 1. En este caso, se dice que se reescribe en un paso , o se reescribe directamente , a por el sistema , formalmente denotado como , , o como por algunos autores. ${\displaystyle l\rightarrow r}$ ${\displaystyle l\rightarrow r}$ ${\displaystyle \sigma }$ ${\displaystyle s}$ ${\displaystyle \sigma }$ ${\displaystyle r}$ ${\displaystyle \sigma }$ ${\displaystyle s}$ ${\displaystyle t}$ ${\displaystyle R}$ ${\displaystyle s\rightarrow _{R}t}$ ${\displaystyle s{\underset {R}{\rightarrow }}t}$ ${\displaystyle s{\overset {R}{\rightarrow }}t}$

Si un término puede reescribirse en varios pasos en un término , es decir, si , se dice que el término se reescribe en , formalmente denotado como . En otras palabras, la relación es el cierre transitivo de la relación ; a menudo, también se utiliza la notación para denotar el cierre reflexivo-transitivo de , es decir, si o . ^[17] 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}{\underset {R}{\rightarrow }}t_{2}{\underset {R}{\rightarrow }}\cdots {\underset {R}{\rightarrow }}t_{n}}$ ${\displaystyle t_{1}}$ ${\displaystyle t_{n}}$ ${\displaystyle t_{1}{\overset {+}{\underset {R}{\rightarrow }}}t_{n}}$ ${\displaystyle {\overset {+}{\underset {R}{\rightarrow }}}}$ ${\displaystyle {\underset {R}{\rightarrow }}}$ ${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$ ${\displaystyle {\underset {R}{\rightarrow }}}$ ${\displaystyle s{\overset {*}{\underset {R}{\rightarrow }}}t}$ ${\displaystyle s=t}$ ${\displaystyle s{\overset {+}{\underset {R}{\rightarrow }}}t}$ ${\displaystyle R}$ ${\displaystyle {\underset {R}{\rightarrow }}}$

Por ejemplo, es una regla de reescritura, que se utiliza habitualmente 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 , véase la imagen 2. ^{[nota 2]} La aplicación de esa sustitución al lado derecho de la regla produce el término , y la sustitución del numerador por ese término produce , que es el término resultante de aplicar la regla de reescritura. En conjunto, la aplicación de la regla de reescritura ha logrado lo que se denomina "aplicar la ley de asociatividad para a " en álgebra elemental. Alternativamente, la regla podría haberse aplicado al denominador del término original, produciendo . ${\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 (a*(a+1))*(a+2)}$ ${\displaystyle {\frac {(a*(a+1))*(a+2)}{1*(2*3)}}}$ ${\displaystyle *}$ ${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$ ${\displaystyle {\frac {a*((a+1)*(a+2))}{(1*2)*3}}}$

Terminación

Los problemas de terminación de los sistemas de reescritura en general se tratan en Sistema de reescritura abstracta#Terminación y convergencia . Para los sistemas de reescritura de términos en particular, se deben considerar las siguientes sutilezas adicionales.

La terminación incluso de un sistema que consiste en una regla con un lado izquierdo lineal es indecidible. ^{[18] [19]} La terminación también es indecidible para sistemas que utilizan solo símbolos de funciones unarias; sin embargo, es decidible para sistemas básicos finitos. ^[20]

El siguiente sistema de reescritura de términos es normalizador, ^{[nota 3]} pero no terminal, ^{[nota 4]} y no confluente: ^[21] $${\displaystyle {\begin{aligned}f(x,x)&\rightarrow g(x),\\f(x,g(x))&\rightarrow b,\\h(c,x)&\rightarrow f(h(x,c),h(x,x)).\\\end{aligned}}}$$

Los dos ejemplos siguientes de sistemas de reescritura de términos de terminación se deben a Toyama: ^[22]

${\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 interminable, ya que

$${\displaystyle {\begin{aligned}&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 &\cdots \end{aligned}}}$$Este resultado refuta una conjetura de Dershowitz , ^[23] quien afirmó que la unión de dos sistemas de reescritura de términos terminales y es nuevamente terminal si todos los lados izquierdos de y los lados derechos de son lineales , y no hay " superposiciones " entre los lados izquierdos de y los lados derechos de . Todas estas propiedades se satisfacen con los ejemplos de Toyama. ${\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 orden superior

Los sistemas de reescritura de orden superior son una generalización de los sistemas de reescritura de términos de primer orden a términos lambda , lo que permite funciones de orden superior y variables ligadas. ^[24] Varios resultados sobre los TRS de primer orden también se pueden reformular para los HRS. ^[25]

Sistemas de reescritura de gráficos

Los sistemas de reescritura de gráficos son otra generalización de los sistemas de reescritura de términos, que operan sobre gráficos en lugar de términos ( de base ) o su representación de árbol correspondiente .

Sistemas de reescritura de trazas

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

Véase también

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

Notas

1. Esta variante de la regla anterior es necesaria porque la ley conmutativa A ∨ B = B ∨ A no se puede convertir en una regla de reescritura. Una regla como A ∨ B → B ∨ A haría que el sistema de reescritura no fuera terminante.
2. ya que al aplicar esa sustitución al lado izquierdo de la regla se obtiene el numerador ${\displaystyle x*(y*z)}$ ${\displaystyle a*((a+1)*(a+2))}$
3. es decir, para cada término existe alguna forma normal, p. ej., 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 )) → ... → g ( b ); ni b ni g ( b ) pueden reescribirse más, por lo tanto, el sistema no es confluente
4. 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 )) → ...

Lectura adicional

• Baader, Franz ; Nipkow, Tobias (1999). Reescritura de términos y todo eso . Cambridge University Press. ISBN 978-0-521-77920-3.316 páginas.
• Marc Bezem, Jan Willem Klop , Roel de Vrijer ("Terese"), Term Rewriting Systems ("TeReSe"), Cambridge University Press, 2003, ISBN 0-521-39115-6 . Esta es la monografía completa más reciente. Sin embargo, utiliza una buena cantidad de notaciones y definiciones que aún no son estándar. Por ejemplo, la propiedad de 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.), Handbook of Theoretical Computer Science, volumen B: Formal Models and Semantics. , 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 figuras. 
• Nachum Dershowitz y David Plaisted . "Reescritura", Capítulo 9 en 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 . "Sistemas de reescritura de términos", Capítulo 1 en Samson Abramsky , Dov M. Gabbay y Tom Maibaum (Eds.), Manual de lógica en ciencias de la computación, 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.), Manual de lógica en inteligencia artificial y programación lógica, 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: un libro de consulta , Elsevier (1990).

Reescritura de cadenas

• Ronald V. Book y Friedrich Otto, Sistemas de reescritura de cadenas , 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 – 2.ª edición , Academic Press, ISBN 0-12-206382-1 . 

Enlaces externos

• La página de inicio de Rewriting
• Grupo de trabajo 1.6 del IFIP
• Investigadores en reescritura por Aart Middeldorp, Universidad de Innsbruck
• Portal de terminación
• Sistema Maude: una implementación de software de un sistema de reescritura de términos genéricos. ^[5]

Referencias

1. Joseph Goguen "Proving and Rewriting" Conferencia internacional sobre programación algebraica y lógica, 1990 Nancy, Francia, págs. 1-24
2. Sculthorpe, Neil; Frisby, Nicolas; Gill, Andy (2014). "El motor de reescritura de la Universidad de Kansas" (PDF) . Journal of Functional Programming . 24 (4): 434–473. doi :10.1017/S0956796814000185. ISSN  0956-7968. S2CID  16807490. Archivado (PDF) desde el original el 2017-09-22 . Consultado el 2019-02-12 .
3. Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël (1992). "El enfoque de reescritura de términos para la demostración automática de teoremas". The Journal of Logic Programming . 14 (1–2): 71–99. doi : 10.1016/0743-1066(92)90047-7 .
4. Frühwirth, Thom (1998). "Teoría y práctica de reglas de manejo de restricciones". The Journal of Logic Programming . 37 (1–3): 95–138. doi : 10.1016/S0743-1066(98)10005-5 .
5. 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". Ciencias de la Computación Teórica . 285 (2): 187–243. doi : 10.1016/S0304-3975(01)00359-0 .
6. Kim Marriott; Peter J. Stuckey (1998). Programación con restricciones: una introducción. MIT Press. pp. 436–. ISBN 978-0-262-13341-8.
7. 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ág. 24.
8. Robert Freidin (1992). Fundamentos de la sintaxis generativa. Prensa del MIT. ISBN 978-0-262-06144-5.
9. Libro y Otto, pág. 10
10. Bezem y otros, pág. 7,
11. Bezem y otros, pág. 7
12. Martín Davis y otros. 1994, pág. 178
13. Dershowitz, Jouannaud (1990), sección 1, p.245
14. Albert, Gräf (2009). "Procesamiento de señales en el lenguaje de programación puro". Conferencia de audio sobre Linux .
15. Riepe, Von Michael (18 de noviembre de 2009). "Puro - eine einfache funktionale Sprache". Archivado desde el original el 19 de marzo de 2011.
16. Klop, JW "Term Rewriting Systems" (PDF) . Documentos de Nachum Dershowitz y estudiantes . Universidad de Tel Aviv. p. 12. Archivado (PDF) del original el 15 de agosto de 2021 . Consultado el 14 de agosto de 2021 .
17. N. Dershowitz, J.-P. Jouannaud (1990). Jan van Leeuwen (ed.). Rewrite Systems . Manual de informática teórica. Vol. B. Elsevier. págs. 243–320.; aquí: Sec. 2.3
18. Max Dauchet (1989). "Simulación de máquinas de Turing mediante una regla de reescritura lineal a la izquierda". Actas de la 3.ª conferencia internacional sobre técnicas y aplicaciones de reescritura . LNCS. Vol. 355. Springer. págs. 109-120.
19. Max Dauchet (septiembre de 1992). "Simulación de máquinas de Turing mediante una regla de reescritura regular". Ciencias de la Computación Teórica . 103 (2): 409–420. doi : 10.1016/0304-3975(92)90022-8 .
20. Gerard Huet, DS Lankford (marzo de 1978). On the Uniform Halting Problem for Term Rewriting Systems (PDF) (Informe técnico). IRIA. pág. 8. 283. Consultado el 16 de junio de 2013 .
21. Bernhard Gramlich (junio de 1993). "Relating Innermost, Weak, Uniform, and Modular Termination of Term Rewriting Systems". En Voronkov, Andrei (ed.). Proc. Conferencia internacional sobre programación lógica y razonamiento automatizado (LPAR) . LNAI. Vol. 624. Springer. págs. 285–296. Archivado desde el original el 4 de marzo de 2016. Consultado el 19 de junio de 2014 .Aquí: Ejemplo 3.3
22. Yoshihito Toyama (1987). "Contraejemplos de terminación para 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 . Archivado (PDF) desde el original el 2019-11-13 . Consultado el 2019-11-13 .
23. N. Dershowitz (1985). "Terminación" (PDF) . En Jean-Pierre Jouannaud (ed.). Proc. RTA . LNCS. Vol. 220. Springer. págs. 180–224. Archivado (PDF) desde el original el 12 de noviembre de 2013. Consultado el 16 de junio de 2013 .; aquí: p.210
24. Wolfram, DA (1993). La teoría de tipos de cláusulas . Cambridge University Press. pp. 47–50. doi :10.1017/CBO9780511569906. ISBN . 9780521395380. Número de identificación del sujeto  42331173.
25. Nipkow, Tobias; Prehofer, Christian (1998). "Reescritura de orden superior y razonamiento ecuacional". En Bibel, W.; Schmitt, P. (eds.). Deducción automatizada: una base para aplicaciones. Volumen I: Fundamentos . Kluwer. págs. 399–430. Archivado desde el original el 2021-08-16 . Consultado el 2021-08-16 .