Hispanopedia Wiki
Articulo de referencia

Reescritura

En matemáticas , lingüística , informática y lógica , la reescritura abarca una amplia gama de métodos para reemplazar subtérminos de una fórmula con otros términos. Estos métod...

Hispanopedia WikiContenido en espanolLectura gratuita

En matemáticas , lingüística , informática y lógica , la reescritura abarca una amplia gama de métodos para reemplazar subtérminos de una fórmula con otros términos. Estos métodos pueden implementarse 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, además de relaciones sobre cómo transformar dichos 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ían aplicarse varias reglas. Por lo tanto, los sistemas de reescritura no proporcionan un algoritmo para cambiar un término por otro, sino un conjunto de posibles aplicaciones de reglas. Sin embargo, cuando se combinan con un algoritmo apropiado, los sistemas de reescritura pueden considerarse programas informáticos , y varios demostradores de teoremas [ 3 ] y lenguajes de programación declarativos se basan en la reescritura de términos. [ 4 ] [ 5 ]

Ejemplos de casos

Lógica

En lógica , el procedimiento para obtener la forma normal conjuntiva (FNC) de una fórmula puede implementarse como un sistema de reescritura. [ 6 ] Por ejemplo, las reglas de dicho sistema serían:

¬¬A→A{\displaystyle \neg \neg A\to A}( eliminación de la doble negación )
¬(A∧B)→¬A∨¬B{\displaystyle \neg (A\land B)\to \neg A\lor \neg B}( Leyes de De Morgan )
¬(A∨B)→¬A∧¬B{\displaystyle \neg (A\lor B)\to \neg A\land \neg B}
(A∧B)∨do→(A∨do)∧(B∨do){\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)}( distributividad )
A∨(B∧do)→(A∨B)∧(A∨do),{\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C),}[ nota 1 ]

Para cada regla, cada variable denota una subexpresión y el símbolo (→{\displaystyle \to }) indica que una expresión que coincide con su lado izquierdo puede reescribirse como una que coincide con su lado derecho. En este sistema, cada regla es una equivalencia lógica , por lo que reescribir una expresión mediante estas reglas no cambia su valor de verdad. Otros sistemas de reescritura útiles en lógica pueden no preservar los valores de verdad; véase, por ejemplo, la equisatisfacibilidad .

Aritmética

Los sistemas de reescritura de términos pueden emplearse para calcular operaciones aritméticas con números naturales . Para ello, cada número debe codificarse como un término . La codificación más sencilla 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 puede utilizarse para calcular la suma y el producto de números naturales dados. [ 7 ]

A+0→A(1),A+S(B)→S(A+B)(2),A⋅0→0(3),A⋅S(B)→A+(A⋅B)(4).{\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 mediante la reescritura de términos de la siguiente manera:

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

donde la notación sobre cada flecha indica la regla utilizada para cada reescritura.

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

S(S(0))⋅S(S(0)){\displaystyle S(S(0))\cdot S(S(0))}→(4){\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}S(S(0))+S(S(0))⋅S(0){\displaystyle S(S(0))+S(S(0))\cdot S(0)}→(4){\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}S(S(0))+S(S(0))+S(S(0))⋅0{\displaystyle S(S(0))+S(S(0))+S(S(0))\cdot 0}→(3){\displaystyle \;\;{\stackrel {(3)}{\to }}\;\;}S(S(0))+S(S(0))+0{\displaystyle S(S(0))+S(S(0))+0}→(1){\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}S(S(0))+S(S(0)){\displaystyle S(S(0))+S(S(0))}→sa{\displaystyle \;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;}S(S(S(S(0)))),{\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 sintagmática , 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 suele tomar la formaA→incógnita{\displaystyle {\rm {A\rightarrow X}}}donde A es una etiqueta de categoría sintáctica , como frase nominal u oración , y X es una secuencia de dichas etiquetas o morfemas , que expresa el hecho de que A puede ser reemplazada por X al generar la estructura constituyente de una oración. Por ejemplo, la reglaS→nortePAG VPAG{\displaystyle {\rm {S\rightarrow NP\ VP}}}significa que una oración puede constar de un sintagma nominal (SN) seguido de un sintagma verbal (SV); otras reglas especificarán de qué subconstituyentes pueden constar un sintagma nominal y un sintagma verbal, y así sucesivamente.

Sistemas de reescritura abstracta

A partir de los ejemplos anteriores, queda claro que podemos concebir los sistemas de reescritura de forma 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 SRA ). [ 10 ] Un SRA 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 un ARS, se pueden definir muchos conceptos y notaciones.→∗{\displaystyle {\overset {*}{\rightarrow }}}es el cierre transitivo reflexivo de→{\displaystyle \rightarrow }.↔{\displaystyle \leftrightarrow }es el cierre simétrico de→{\displaystyle \rightarrow }.↔∗{\displaystyle {\overset {*}{\leftrightarrow }}}es el cierre simétrico transitivo reflexivo de→{\displaystyle \rightarrow }El problema verbal para un ARS es determinar, dados x e y , siincógnita↔∗y{\displaystyle x{\overset {*}{\leftrightarrow }}y}. Un objeto x en A se llama reducible si existe algún otro y en A tal queincógnita→y{\displaystyle x\rightarrow y}; de lo contrario se denomina irreducible o forma normal . Un objeto y se denomina "forma normal de x " siincógnita→∗y{\displaystyle x{\stackrel {*}{\rightarrow }}y}y es irreducible. Si la forma normal de x es única, entonces esto se suele denotar conincógnita↓{\displaystyle x{\downarrow }}. Si cada objeto tiene al menos una forma normal, el ARS se denomina normalizador .incógnita↓y{\displaystyle x\downarrow y}o se dice que x e y son combinables si existe algún z con la propiedad de queincógnita→∗z←∗y{\displaystyle x{\overset {*}{\rightarrow }}z{\overset {*}{\leftarrow }}y}Se dice que un ARS posee la propiedad Church-Rosser siincógnita↔∗y{\displaystyle x{\overset {*}{\leftrightarrow }}y}implicaincógnita↓y{\displaystyle x\downarrow y}. Un ARS es confluente si para todo w , x , e y en A , incógnita←∗w→∗y{\displaystyle x{\overset {*}{\leftarrow }}w{\overset {*}{\rightarrow }}y}implicaincógnita↓y{\displaystyle x\downarrow y}. Un ARS es localmente confluente si y solo si para todo w , x , e y en A , incógnita←w→y{\displaystyle x\leftarrow w\rightarrow y}implicaincógnita↓y{\displaystyle x{\mathbin {\downarrow }}y}Se dice que un ARS es terminante o noetheriano si no hay una cadena infinita .incógnita0→incógnita1→incógnita2→⋯{\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }. Un ARS confluente y terminado se denomina convergente o canónico .

Los teoremas importantes para los sistemas de reescritura abstractos son que un ARS es confluente si y solo si tiene la propiedad de Church-Rosser, el lema de Newman (un ARS que termina es confluente si y solo si es localmente confluente) y que el problema de la palabra 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,R{\displaystyle R}, a todas las cadenas del alfabeto que contienen los lados izquierdo y derecho, respectivamente, de algunas reglas como subcadenas . Formalmente, un sistema semi-Thue es una tupla(Σ,R){\displaystyle (\Sigma ,R)}dóndeΣ{\displaystyle \Sigma }es un alfabeto (generalmente finito) yR{\displaystyle R}es una relación binaria entre algunas cadenas (fijas) del alfabeto, llamada conjunto de reglas de reescritura . La relación de reescritura de un paso→R{\displaystyle {\underset {R}{\rightarrow }}}inducido porR{\displaystyle R}enΣ∗{\displaystyle \Sigma ^{*}}se define como: sis,t∈Σ∗{\displaystyle s,t\in \Sigma ^{*}}si hay alguna cadena, entoncess→Rt{\displaystyle s{\underset {R}{\rightarrow }}t}si existenincógnita,y,tú,v∈Σ∗{\displaystyle x,y,u,v\in \Sigma ^{*}}de tal manera ques=incógnitatúy{\displaystyle s=xuy},t=incógnitavy{\displaystyle t=xvy}, ytúRv{\displaystyle uRv}. Desde→R{\displaystyle {\underset {R}{\rightarrow }}}es una relación enΣ∗{\displaystyle \Sigma ^{*}}, la pareja(Σ∗,→R){\displaystyle (\Sigma ^{*},{\underset {R}{\rightarrow }})}se ajusta a la definición de un sistema de reescritura abstracto. Dado que la cadena vacía está enΣ∗{\displaystyle \Sigma ^{*}},R{\displaystyle R}es un subconjunto de→R{\displaystyle {\underset {R}{\rightarrow }}}. Si la relaciónR{\displaystyle R}Si es simétrico , entonces el sistema se llama sistema de Thue .

En un SRS, la relación de reducción→R∗{\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}es compatible con la operación monoide, lo que significa queincógnita→R∗y{\displaystyle x{\overset {*}{\underset {R}{\rightarrow }}}y}implicatúincógnitav→R∗túyv{\displaystyle uxv{\overset {*}{\underset {R}{\rightarrow }}}uyv}para todas las cadenasincógnita,y,tú,v∈Σ∗{\displaystyle x,y,u,v\in \Sigma ^{*}}. De manera similar, el cierre simétrico transitivo reflexivo de→R{\displaystyle {\underset {R}{\rightarrow }}}, denotado↔R∗{\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}, 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↔R∗{\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}se denomina congruencia de Thue generada porR{\displaystyle R}. En un sistema Thue, es decir siR{\displaystyle R}es simétrico, la relación de reescritura→R∗{\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}coincide con la congruencia de Thue↔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↔R∗{\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}es una congruencia, podemos definir el monoide factorialMETROR=Σ∗/↔R∗{\displaystyle {\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}}del monoide libreΣ∗{\displaystyle \Sigma ^{*}}por la congruencia de Thue. Si un monoideMETRO{\displaystyle {\mathcal {M}}}es isomorfo conMETROR{\displaystyle {\mathcal {M}}_{R}}, luego el sistema semi-Thue(Σ,R){\displaystyle (\Sigma ,R)}se denomina presentación monoide deMETRO{\displaystyle {\mathcal {M}}}.

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

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

Sistemas de reescritura de términos

Imagen 1: Diagrama triangular esquemático de la aplicación de una regla de reescritura.l⟶r{\displaystyle l\longrightarrow r}en posiciónpag{\displaystyle p}en un término, con sustitución coincidenteσ{\displaystyle \sigma }
Imagen 2: Regla del término izquierdoincógnita∗(y∗z){\displaystyle x*(y*z)}coincidencia en términosa∗((a+1)∗(a+2))1∗(2∗3){\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 la sección  Lógica anterior es un sistema de reescritura de términos. Los términos en este sistema están compuestos por operadores binarios.(∨){\displaystyle (\vee )}y(∧){\displaystyle (\wedge )}y el operador unario(¬){\displaystyle (\neg )}En las reglas también están presentes variables que representan cualquier término posible (aunque una misma variable siempre representa el mismo término a lo largo de una misma regla).

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, cuyo conjunto de símbolos admitidos está determinado por una signatura dada . Como formalismo, los sistemas de reescritura de términos poseen toda la potencia de las máquinas de Turing ; es decir, toda 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 comol→r{\displaystyle l\rightarrow r}, 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 reglal→r{\displaystyle l\rightarrow r}se puede aplicar 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.σ{\displaystyle \sigma }de tal manera que el subtérmino des{\displaystyle s}enraizado en alguna posición p es el resultado de aplicar la sustituciónσ{\displaystyle \sigma }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 r{\displaystyle r}con la sustituciónσ{\displaystyle \sigma }aplicado, ver imagen 1. En este caso,s{\displaystyle s}Se dice que se reescribe en un paso , o se reescribe directamente , parat{\displaystyle t}por el sistemaR{\displaystyle R}, formalmente denotado comos→Rt{\displaystyle s\rightarrow _{R}t},s→Rt{\displaystyle s{\underset {R}{\rightarrow }}t}, o comos→Rt{\displaystyle s{\overset {R}{\rightarrow }}t}por algunos autores.

Si un términot1{\displaystyle t_{1}}puede reescribirse en varios pasos en un términotnorte{\displaystyle t_{n}}, es decir, sit1→Rt2→R⋯→Rtnorte{\displaystyle t_{1}{\underset {R}{\rightarrow }}t_{2}{\underset {R}{\rightarrow }}\cdots {\underset {R}{\rightarrow }}t_{n}}, el términot1{\displaystyle t_{1}}Se dice que se reescribió paratnorte{\displaystyle t_{n}}, formalmente denotado comot1→R+tnorte{\displaystyle t_{1}{\overset {+}{\underset {R}{\rightarrow }}}t_{n}}. En otras palabras, la relación→R+{\displaystyle {\overset {+}{\underset {R}{\rightarrow }}}}es el cierre transitivo de la relación→R{\displaystyle {\underset {R}{\rightarrow }}}; a menudo, también la notación→R∗{\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}se utiliza para denotar el cierre reflexivo-transitivo de→R{\displaystyle {\underset {R}{\rightarrow }}}, eso es,s→R∗t{\displaystyle s{\overset {*}{\underset {R}{\rightarrow }}}t}sis=t{\displaystyle s=t}os→R+t{\displaystyle s{\overset {+}{\underset {R}{\rightarrow }}}t}. [ 17 ] Una reescritura de término dada por un conjuntoR{\displaystyle R}de reglas puede verse como un sistema de reescritura abstracto como se definió anteriormente , con términos como sus objetos y→R{\displaystyle {\underset {R}{\rightarrow }}}como su relación de reescritura.

Por ejemplo,incógnita∗(y∗z)→(incógnita∗y)∗z{\displaystyle x*(y*z)\rightarrow (x*y)*z}es una regla de reescritura, comúnmente utilizada para establecer una forma normal con respecto a la asociatividad de∗{\displaystyle *}Esa regla se puede aplicar en el numerador del término.a∗((a+1)∗(a+2))1∗(2∗3){\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}con la sustitución correspondiente{incógnita↦a,y↦a+1,z↦a+2}{\displaystyle \{x\mapsto a,\;y\mapsto a+1,\;z\mapsto a+2\}}, ver imagen 2. [ nota 2 ] Aplicando esa sustitución al lado derecho de la regla se obtiene el término(a∗(a+1))∗(a+2){\displaystyle (a*(a+1))*(a+2)}y sustituyendo el numerador por ese término se obtiene(a∗(a+1))∗(a+2)1∗(2∗3){\displaystyle {\frac {(a*(a+1))*(a+2)}{1*(2*3)}}}, 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∗{\displaystyle *}aa∗((a+1)∗(a+2))1∗(2∗3){\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, dando como resultadoa∗((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 Abstract rewriting system#Termination and convergence . 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 consta de una sola regla con un segundo miembro 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 base finitos . [ 20 ]

El siguiente sistema de reescritura de términos es normalizador, [ nota 3 ] pero no terminante, [ nota 4 ] y no confluente: [ 21 ]F(incógnita,incógnita)→gramo(incógnita),F(incógnita,gramo(incógnita))→b,h(do,incógnita)→F(h(incógnita,do),h(incógnita,incógnita)).{\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 siguientes dos ejemplos de sistemas de reescritura de términos terminantes se deben a Toyama: [ 22 ]

F(0,1,incógnita)→F(incógnita,incógnita,incógnita){\displaystyle f(0,1,x)\rightarrow f(x,x,x)}

y

gramo(incógnita,y)→incógnita,{\displaystyle g(x,y)\rightarrow x,}
gramo(incógnita,y)→y.{\displaystyle g(x,y)\rightarrow y.}

Su unión es un sistema no terminante, ya que

F(gramo(0,1),gramo(0,1),gramo(0,1))→F(0,gramo(0,1),gramo(0,1))→F(0,1,gramo(0,1))→F(gramo(0,1),gramo(0,1),gramo(0,1))→⋯{\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 terminantesR1{\displaystyle R_{1}}yR2{\displaystyle R_{2}}vuelve a terminar si todos los lados izquierdos deR1{\displaystyle R_{1}}y lados derechos deR2{\displaystyle R_{2}}son lineales y no hay " superposiciones " entre los lados izquierdos deR1{\displaystyle R_{1}}y lados derechos deR2{\displaystyle R_{2}}Todas estas propiedades se cumplen en los ejemplos de Toyama.

Consulte Orden de reescritura y Ordenación de rutas (reescritura de términos) para conocer las relaciones de ordenación utilizadas en las pruebas de terminación para 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 acotadas. [ 24 ] Varios resultados sobre los TRS de primer orden también pueden reformularse para los HRS. [ 25 ]

Sistemas de reescritura de grafos

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

Sistemas de reescritura de trazas

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

Véase también

Notas

  1. ↑ Esta variante de la regla anterior es necesaria ya que la ley conmutativa A ∨ B = B ∨ A no puede transformarse en una regla de reescritura. Una regla como A ∨ B → B ∨ A provocaría que el sistema de reescritura no terminara.
  2. ↑ ya que al aplicar esa sustitución al lado izquierdo de la reglaincógnita∗(y∗z){\displaystyle x*(y*z)}produce el numeradora∗((a+1)∗(a+2)){\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 )) → ... → g ( b ); ni b ni g ( b ) pueden reescribirse más, por lo tanto, el sistema no es confluente.
  4. ↑ Es decir, existen infinitas derivaciones, por ejemplo: 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 )) → ...

Lecturas adicionales

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
  • La página principal de reescritura
  • Grupo de Trabajo 1.6 de IFIP
  • Investigadores en el campo de la reescritura, por Aart Middeldorp , Universidad de Innsbruck
  • Portal de terminación
  • Sistema Maude : una implementación de software de un sistema genérico de reescritura de términos. [ 5 ]

Referencias

  1. ↑ Joseph Goguen, "Demostración y reescritura", 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) del original el 22 de septiembre de 2017. Recuperado el 12 de febrero de 2019 .  
  3. ↑ Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël (1992). "El enfoque de reescritura de términos para la demostración automatizada 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 las reglas de manejo de restricciones" . The Journal of Logic Programming . 37 ( 1–3 ): 95–138 . doi : 10.1016/S0743-1066(98)10005-5 .
  5. 1 2 Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, JF (2002). "Maude: Especificación y programación en lógica de reescritura" . Theoretical Computer Science . 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. 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 . Sourcebook. Elsevier. pp. 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. 1 2 Book y Otto, pág. 10
  10. ↑ Bezem et al., pág. 7,
  11. ↑ Bezem et al., 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" . Linux Audio Conference .
  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 "Sistemas de reescritura de términos" (PDF) . Artículos de Nachum Dershowitz y estudiantes . Universidad de Tel Aviv. pág. 12. Archivado (PDF) del original el 15 de agosto de 2021. Recuperado el 14 de agosto de 2021 . 
  17. ↑ N. Dershowitz, J.-P. Jouannaud (1990). Jan van Leeuwen (ed.). Sistemas de reescritura . Manual de informática teórica. Vol. B. Elsevier. págs. 243–320 .  ; aquí: Sección  2.3
  18. ↑ Max Dauchet (1989). "Simulación de máquinas de Turing mediante una regla de reescritura lineal 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" . Theoretical Computer Science . 103 (2): 409– 420. doi : 10.1016/0304-3975(92)90022-8 .
  20. ↑ Gerard Huet, DS Lankford (marzo de 1978). Sobre el problema de parada uniforme para sistemas de reescritura de términos (PDF) (Informe técnico). IRIA. pág. 8. 283. Recuperado el 16 de junio de 2013 . 
  21. ↑ Bernhard Gramlich (junio de 1993). "Relacionando la terminación interna, débil, uniforme y modular de los sistemas de reescritura de términos" . En Voronkov, Andrei (ed.). Actas de la Conferencia Internacional sobre Programación Lógica y Razonamiento Automatizado (LPAR) . LNAI. Vol. 624. Springer. págs. 285–296 . Archivado del original el 4 de marzo de 2016. Consultado el 19 de junio de 2014 .  Aquí: Ejemplo 3.3
  22. ↑ Yoshihito Toyama (1987). "Contraejemplos a la terminación para la suma directa de sistemas de reescritura de términos" (PDF) . Inf. Process. Lett . 25 (3): 141– 143. doi : 10.1016/0020-0190(87)90122-0 . hdl : 2433/99946 . Archivado (PDF) del original el 13 de noviembre de 2019. Recuperado el 13 de noviembre de 2019 .
  23. ↑ N. Dershowitz (1985). "Terminación" (PDF) . En Jean-Pierre Jouannaud (ed.). Proc. RTA . LNCS. Vol. 220. Springer. pp. 180–224 . Archivado (PDF) del original el 12-11-2013 . Recuperado el 16-06-2013 .  ; aquí: pág. 210
  24. ↑ Wolfram, DA (1993). La teoría clausal de los tipos . Cambridge University Press. págs. 47–50 . doi : 10.1017/CBO9780511569906 . ISBN  9780521395380. S2CID 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. pp. 399–430 . Archivado del original el 16 de agosto de 2021. Recuperado el 16 de agosto de 2021 .