Un sistema formal formado por términos construidos a partir de símbolos de función y variables junto con un conjunto de reglas de reescritura dirigidas de la forma l → r que reemplazan instancias de un patrón izquierdo l por el término derecho correspondiente r; la reescritura procede mediante el emparejamiento y reemplazo repetidos de subtérminos.

Principio

La computación y el razonamiento equacional se modelan como aplicaciones dirigidas de ecuaciones basadas en patrones: un paso de reescritura sustituye una instancia emparejada de l por r bajo una sustitución de coincidencia y en un contexto; propiedades como terminación (ausencia de secuencias infinitas) y confluencia (formas normales únicas) gobiernan la determinación y la decidibilidad de la igualdad.

Demostración

TRS simple para simplificación aritmética: reglas 0 + x → x, succ(x) + y → succ(x + y) reescriben expresiones a una forma normal. Un TRS terminante y confluyente da una forma normal única para cada término, por lo que la equivalencia modulo la relación de reescritura se decide normalizando ambos lados.

Aplicación incorrecta

Usar reglas de reescritura sin comprobar la terminación puede producir reducciones no terminantes; ignorar la confluencia puede dar lugar a formas normales distintas según el orden de reescritura, invalidando afirmaciones de decidibilidad. Aplicar técnicas de TRS de primer orden a lenguajes de orden superior o sensibles al contexto sin adaptación puede falsear expresividad y complejidad.

Consecuencia

Los TRS ofrecen un marco uniforme para definir computación, transformación de programas, especificación algebraica y razonamiento equacional automatizado; cuando terminación y confluencia se cumplen, proporcionan computación canónica y problemas de palabra decidibles, y conectan con semánticas (p. ej. semántica operacional) y técnicas de implementación (indexación de términos, algoritmos de completado).

Inversión

Invertir un paso de reescritura convierte la computación dirigida en un paso equacional (r → l) y es la base de procedimientos de completado (p. ej. intentar volver confluyente un conjunto de ecuaciones) o de reducción inversa; la inversión pone de manifiesto la diferencia entre computación orientada y razonamiento equacional simétrico.

Límite

Los TRS estándar son sistemas de reglas de primer orden, incondicionales e insensibles al contexto; las extensiones incluyen reescritura condicional, sensible al contexto, de orden superior y modulo‑teoría, cada una con distintas propiedades de decidibilidad y confluencia/terminación. Las afirmaciones sobre unicidad de la forma normal o decidibilidad deben especificar la clase de TRS.

Tensión semántica

Hay tensión entre ver la reescritura como computación (dirigida, operacional) y como prueba de igualdad (simétrica, algebraica); también existe una disyuntiva entre expresividad (más características) y analizabilidad (las pruebas de terminación/confluencia se vuelven más difíciles).

Síntesis

Un sistema de reescritura de términos es un modelo dirigido por patrones y basado en reglas para computación y razonamiento equacional: mediante el emparejamiento de subtermos y la aplicación de sustituciones orientadas según reglas de reescritura transforma expresiones; la terminación y la confluencia determinan cuándo la reescritura produce representaciones canónicas y igualdad decidible, mientras que las extensiones adaptan el marco a lenguajes más ricos a costa de mayor complejidad.