# Reescritura

En las matemáticas, ciencias de la computación y la lógica, la reescritura incluye una amplia gama de métodos para reemplazar subtérminos de una fórmula con otros términos. Tales métodos pueden lograrse por sistemas de reescritura (también conocidos como motores de reescritura o sistemas de reducción). En su forma más básica, consisten en un conjunto de objetos, además de relaciones representando funciones para transformar tales objetos.
Puede que reescritura sea no determinista. Puede que una regla para reescribir un término pueda aplicarse de muchas maneras diferentes a dicho término, o que puedan aplicarse más de una regla. Los sistemas de reescritura no proveen 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 verse como programas informáticos, y varios programas para demostrar teoremas y lenguajes de programación declarativa se basan en la reescritura de términos.

## Ejemplos
### Lógica

En la lógica, el procedimiento para obtener la forma normal conjuntiva (FNC) de una fórmula se puede implementar como un sistema de reescritura. Las reglas para un ejemplo de tal sistema serían:
    $\neg \neg A\to A$ (eliminación de doble negación)
    $\neg (A\land B)\to \neg A\lor \neg B$ (Leyes de De Morgan)
    $\neg (A\lor B)\to \neg A\land \neg B$
    $(A\land B)\lor C\to (A\lor C)\land (B\lor C)$ (distributividad)
    $A\lor (B\land C)\to (A\lor B)\land (A\lor C),$
donde el símbolo ($\to$) indica que una expresión que coincida con el lado izquierdo de la regla se puede reescribir como una formada por el lado derecho, y donde cada símbolo denota una subexpresión. En tal sistema, cada regla se elige de para que el lado izquierdo sea equivalente al lado derecho y, en consecuencia, cuando el lado izquierdo coincida con una subexpresión, realizar una reescritura de esa subexpresión de la izquierda al derecho se mantiene la consistencia y el valor lógicos de toda la expresión.

### Aritmética

Los sistemas de reescritura de términos se pueden utilizar para calcular operaciones aritméticas entre números naturales. Para hacer esto, cada uno de tales números 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 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 usar para calcular la suma y el producto de números naturales dados.
    ${\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 que 2+2 resuelta en 4 se puede duplicar por reescritura de término de la siguiente manera:
    $S(S(0))+S(S(0))$ $\;\;{\stackrel {(2)}{\to }}\;\;$ $S(\;S(S(0))+S(0)\;)$ $\;\;{\stackrel {(2)}{\to }}\;\;$ $S(S(\;S(S(0))+0\;))$ $\;\;{\stackrel {(1)}{\to }}\;\;$ $S(S(S(S(0)))),$
donde el número de la regla se da encima de la flecha de reescritura a (el símbolo $\to$).
Por otro ejemplo, el cálculo de 2⋅2 se hace así:
    $S(S(0))\cdot S(S(0))$ $\;\;{\stackrel {(4)}{\to }}\;\;$ $S(S(0))+S(S(0))\cdot S(0)$ $\;\;{\stackrel {(4)}{\to }}\;\;$ $S(S(0))+S(S(0))+S(S(0))\cdot 0$ $\;\;{\stackrel {(3)}{\to }}\;\;$ $S(S(0))+S(S(0))+0$ $\;\;{\stackrel {(1)}{\to }}\;\;$ $S(S(0))+S(S(0))$ $\;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;$ $S(S(S(S(0)))),$
donde el último paso utiliza el cálculo del ejemplo anterior.

### Lingüística

En la lingüística, las reglas de estructura de frases, también llamadas reglas de reescritura, se utilizan en algunos sistemas de gramática generativa, como un medio para generar las oraciones gramaticalmente correctas de un idioma. Tal regla típicamente sigue la forma ${\rm {A\rightarrow X}}$, donde A es una etiqueta de categoría sintáctica, como un sintagma nominal o una oración, y X es una secuencia de tales etiquetas o morfemas, expresando el hecho que A puede ser reemplazada por X al generar la estructura constitutiva de una oración. Por ejemplo, la regla ${\rm {O\rightarrow SN\ SV}}$ significa que una oración (O) puede consistir en una sintagma nominal (SN) seguida de una sintagma verbal (SV); otras reglas especificarán en cuáles subconstituyentes puede consistir un sintagma nominal o verbal, y así sucesivamente.