Reescritura

En les matemàtiques, ciències de la computació i la llògica, la reescritura inclou una àmplia gama de métodos per a reemplaçar subtérminos d'una fòrmula en atres térmens. Tals métodos poden conseguir-se per sistemes de reescritura (també coneguts com a motors de reescritura o sistemes de reducció). En la seua forma més bàsica, consistixen en un conjunt d'objectes, ademés de relacions representant funcions per a transformar tals objectes.

Pot ser que reescritura siga no determinista. Pot ser que una regla per a reescriure un terme puga aplicar-se de moltes maneres diferents a dit terme, o que puguen aplicar-se més d'una regla. Els sistemes de reescritura no proveïxen un algoritme per a canviar un terme per un atre, sino un conjunt de possibles aplicacions de regles. No obstant, quan es combinen en un algoritme apropiat, els sistemes de reescritura poden vore's com programes informàtics, i varis programes per a demostrar teoremes i llenguages de programació declarativa es basen en la reescritura de térmens.

Eixemples

Llògica

En la llògica, el procediment per a obtindre la forma normal conjuntiva (FNC) d'una fòrmula es pot implementar com un sistema de reescritura. Les regles per a un eixemple de tal sistema serien:

$\mathrm{\neg }\mathrm{\neg }A\to A$ (eliminació de doble negació)

$\mathrm{\neg }(A\wedge B)\to \mathrm{\neg }A\vee \mathrm{\neg }B$ (Lleis de De Morgan)

$\mathrm{\neg }(A\vee B)\to \mathrm{\neg }A\wedge \mathrm{\neg }B$

$(A\wedge B)\vee C\to (A\vee C)\wedge (B\vee C)$ (distributividad)

$A\vee (B\wedge C)\to (A\vee B)\wedge (A\vee C),$

a on el símbol ($\to$) indica que una expressió que coincidixca en el costat esquerre de la regla es pot reescriure com una formada pel costat dret, i a on cada símbol denota una subexpresión. En tal sistema, cada regla s'elegix de per a que el costat esquerre siga equivalent al costat dret i, en conseqüència, quan el costat esquerre coincidixca en una subexpresión, realisar una reescritura d'eixa subexpresión de l'esquerra al dret es manté la consistència i el valor llògics de tota l'expressió.

Aritmètica

Els sistemes de reescritura de térmens es poden utilisar per a calcular operacions aritmètiques entre número natural. Per a fer açò, cada u de tals números deu codificar-se com un terme. La codificació més senzilla és l'utilisada en els axioma de Peano, basada en la constant 0 (zero) i la funció successora S. Per eixemple, els números 0, 1, 2 i 3 estan representats pels térmens 0, S(0), S(S(0)) i S(S(S(0))), respectivament. El següent terme sistema de reescritura es pot usar per a calcular la suma i el producte de número natural donats.

$\begin{array}{ccc}A+0& \to A& \text{(1)},\\ A+S(B)& \to S(A+B)& \text{(2)},\\ A\cdot 0& \to 0& \text{(3)},\\ A\cdot S(B)& \to A+(A\cdot B)& \text{(4)}.\end{array}$

Per eixemple, el càlcul que 2+2 resolta en 4 es pot duplicar per reescritura de terme de la següent 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)))),$

a on el número de la regla es dona damunt de la flecha de reescritura a (el símbol $\to$).

Per un atre eixemple, el càlcul de 2⋅2 es fa aixina:

$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{\text{s.a.}}{\to }$ $S(S(S(S(0)))),$

a on l'últim pas utilisa el càlcul de l'eixemple anterior.

Llingüística

En la llingüística, les regles d'estructura de frases, també cridades regles de reescritura, s'utilisen en alguns sistemes de gramàtica generativa, com un mig per a generar les oracions gramaticalmente correctes d'un idioma. Tal regla típicament seguix la forma $\mathrm{A}\mathrm{\to }\mathrm{X}$, a on A és una etiqueta de categoria sintàctica, com un sintagma nominal o una oració, i X és una seqüència de tals etiquetes o morfemes, expressant el fet que A pot ser reemplaçada per X en generar l'estructura constitutiva d'una oració. Per eixemple, la regla $\mathrm{O}\mathrm{\to }\mathrm{S}\mathrm{N}\mathrm{S}\mathrm{V}$ significa que una oració (O) pot consistir en una sintagma nominal (SN) seguida d'una sintagma verbal (SV); atres regles especificaran en quins subconstituyentes pot consistir un sintagma nominal o verbal, i aixina successivament.