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] [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 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 ^[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 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. ^[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 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 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 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 ^[9] o sistema de reescritura abstracta (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]

Se pueden definir muchas nociones y notaciones en el marco general de un ARS. es el cierre transitivo reflexivo de . es el cierre simétrico de . es el cierre simétrico transitivo reflexivo de . El problema de palabras para una ARS es determinar, dadas x y y , si . 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${\displaystyle {\stackrel {*}{\rightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle \leftrightarrow }$${\displaystyle \rightarrow }$${\displaystyle {\stackrel {*}{\,\leftrightarrow \,}}}$${\displaystyle \rightarrow }$${\displaystyle x{\stackrel {*}{\,\leftrightarrow \,}}y}$${\displaystyle x\rightarrow y}$. Un objeto y se denomina "forma normal de x " si , y y son irreductibles. Si la forma normal de x es única, generalmente se denota con . Si cada objeto tiene al menos una forma normal, el ARS se denomina normalizador . o x y y se dice que son unibles si existe algún z con la propiedad de que . Se dice que un ARS posee la propiedad Church-Rosser si lo implica . Un ARS es confluente si para todo w , x , y y${\displaystyle x{\stackrel {*}{\,\rightarrow \,}}y}$${\displaystyle x{\downarrow }}$${\displaystyle x\downarrow y}$${\displaystyle x{\stackrel {*}{\,\rightarrow \,}}z{\stackrel {*}{\,\leftarrow \,}}y}$${\displaystyle x{\stackrel {*}{\,\leftrightarrow \,}}y}$${\displaystyle x\downarrow y}$en A , implica . Un ARS está confluente localmente si y sólo si para todo w , x , y y en A , implica . Se dice que una ARS es terminante o noetheriana si no hay una cadena infinita . Un ARS confluente y terminal se llama convergente o canónico .${\displaystyle x{\stackrel {*}{\,\leftarrow \,}}w{\stackrel {*}{\,\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 tiene la propiedad de Church-Rosser, el lema de Newman que establece que un ARS terminante es confluente si y solo si es localmente confluente, y que el problema de palabras para un ARS es indecidible. en general.

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, llamado el conjunto de reglas de reescritura . La relación de reescritura de una etapa 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. 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 . ^[12]

Sistemas de reescritura de términos

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 }$

Imagen 2: Concordancia de términos de la regla lhs en términos${\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 .

Definicion formal

"Redex" vuelve a dirigir aquí. Para el medicamento, consulte Tadalafil .

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. 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 hay alguna sustitución tal que el subtermo de arraigado en alguna posición p es el resultado de aplicar la sustitución al término l${\displaystyle l\rightarrow r}$${\displaystyle l\rightarrow r}$ ${\displaystyle \sigma }$${\displaystyle s}$ ${\displaystyle \sigma }$. El subtermo que coincide con el lado izquierdo de la regla se llama redex o expresión reducible . ^[13] El término de resultado t de esta aplicación de regla es entonces el resultado de reemplazar el subtermo en la posición p en s por el término con la sustitución aplicada, ver imagen 1. En este caso, se dice que se reescribe en un paso , o reescrito directamente , a por el sistema , denominado formalmente como , o como por algunos autores.${\displaystyle r}$${\displaystyle \sigma }$${\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 . ^[14] 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 2]} 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 conjunto, 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. ^{[15] 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 .^[dieciséis]

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

${\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: ^[18]

${\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 , ^[19] 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 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. También se pueden reformular varios resultados sobre los TRS de primer orden para los HRS. ^[20]

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 en gráficos en lugar de términos ( básicos ) / su representación de árbol correspondiente .

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)
• Compilador
• 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. 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))}$
3. 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 ); ningunob ni g ( b ) se pueden reescribir 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 )) → ...

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) . Revista de programación funcional . 24 (4): 434–473. doi : 10.1017 / S0956796814000185 . ISSN  0956-7968 .
3. Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël (1992). "El enfoque de reescritura de término para la demostración automatizada de teoremas" . El diario de la programación lógica . 14 (1–2): 71–99. doi : 10.1016 / 0743-1066 (92) 90047-7 .
4. 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 .
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" . Informática 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 . Prensa del MIT. págs. 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.24.
8. Robert Freidin (1992). Fundamentos de la sintaxis generativa . Prensa del MIT. ISBN 978-0-262-06144-5.
9. Book y Otto, p. 10
10. Bezem y col., P. 7,
11. Bezem y col., P. 7
12. Martin Davis y col. 1994, pág. 178
13. Klop, JW "Sistemas de reescritura de términos" (PDF) . Artículos de Nachum Dershowitz y estudiantes . Universidad de Tel Aviv. pag. 12 . Consultado el 14 de agosto de 2021 .
14. 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
15. 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.
16. 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 .
17. 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
18. 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 .
19. N. Dershowitz (1985). "Terminación" (PDF) . En Jean-Pierre Jouannaud (ed.). Proc. RTA . LNCS. 220 . Saltador. págs. 180–224. ; aquí: p.210
20. Nipkow, Tobías; Prehofer, Christian (1998). "Reescritura de orden superior y razonamiento ecuacional" . En Bibel, W .; Schmitt, P. (eds.). Deducción automatizada: una base para las solicitudes. Volumen I: Fundaciones . Kluwer. págs. 399–430.

Otras lecturas

• 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 notaciones 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