Reescritura

Reescritura  : una amplia gama de técnicas, métodos y resultados teóricos asociados con los procedimientos para el reemplazo secuencial de partes de fórmulas o términos de un lenguaje formal de acuerdo con un esquema dado: un sistema de reglas de reescritura . En su forma más general, estamos hablando de la colección de un determinado conjunto de objetos y reglas: las relaciones entre estos objetos que indican cómo transformar este conjunto.

La reescritura puede ser no determinista. Por ejemplo, un sistema de reglas de reescritura puede incluir una regla que se puede aplicar al mismo término de varias maneras diferentes, pero no contiene, al mismo tiempo, una indicación de qué método particular se debe aplicar en un caso particular. Sin embargo, si el sistema de reescritura se enmarca como un algoritmo entendido sin ambigüedades, puede considerarse como un programa de computadora. Varios sistemas interactivos de demostración de teoremas [1] y lenguajes de programación declarativos [2] [3] se basan en técnicas de reescritura .

Conceptos básicos y ejemplos

Las principales propiedades de los sistemas de reescritura pueden formularse sin recurrir a una implementación específica de las mismas en forma de operaciones sobre términos. Para ello se suele utilizar el concepto de Abstract Reduction System o ARS (del inglés  Abstract Reduction Systems ) . ARS consta de un conjunto A y un conjunto de relaciones binarias sobre él, que se denominan reducciones . Se dice que A se reduce o reescribe a b en un solo paso con respecto al ARS dado si el par ( a , b ) pertenece a alguno . Las propiedades más importantes de los sistemas de reducción son:

Obviamente, confluencia implica confluencia débil y parada, respectivamente, parada débil. Sin embargo, la confluencia y la parada no están relacionadas. Por ejemplo, un sistema que consta de una regla a•b → b•a es confluente pero no interrumpido. Un sistema que consta de dos reglas a → b y a → c es interrumpido pero no confluente, y las tres reglas juntas forman un sistema que no es interrumpido ni confluente.

El carácter de parada de un sistema de reducción permite asignar a cada elemento su forma normal,  un elemento en el que puede reducirse, pero que ya no se reduce a sí mismo. Si, además, se observa confluencia, entonces tal forma normal siempre será única o canónica . En este sentido, la propiedad de Church-Rosser es especialmente valiosa, ya que permite resolver de manera rápida y eficiente el problema de la igualdad de dos elementos a y b con respecto al sistema de igualdades correspondiente al conjunto de reducciones sin importar la dirección . Para ello basta con calcular las formas normales de ambos elementos. Dado que en este caso la forma normal también será canónica, los elementos serán iguales si y solo si los resultados coinciden.

Teoría de la reescritura clásica

Aunque la noción de reescritura se introdujo originalmente para el cálculo lambda , la mayor parte de los resultados y aplicaciones actualmente se refieren a la reescritura de primer orden. Los sistemas de reescritura de este tipo se denominan Term Rewrite Systems o TRS (del inglés.  Term rewrite systems ).

Véase también

Notas

  1. ↑ Jieh Hsiang, Helène Kirchner, Pierre Lescanne, Michaël Rusinowitch. El enfoque de reescritura de términos para la demostración automatizada de teoremas  //  The Journal of Logic Programming. — 1992-10-01. — vol. 14 , edición. 1 . — pág. 71–99 . — ISSN 0743-1066 . - doi : 10.1016/0743-1066(92)90047-7 . Archivado el 6 de mayo de 2021.
  2. ↑ Teoría y práctica de las reglas de manejo de restricciones  //  The Journal of Logic Programming. — 1998-10-01. — vol. 37 , edición. 1-3 . — pág. 95–138 . — ISSN 0743-1066 . - doi : 10.1016/S0743-1066(98)10005-5 . Archivado desde el original el 5 de julio de 2022.
  3. ↑ Maude: especificación y programación en lógica de reescritura  //  Ciencias de la Computación Teórica. - 2002-08-28. — vol. 285 , edición. 2 . — pág. 187–243 . — ISSN 0304-3975 . - doi : 10.1016/S0304-3975(01)00359-0 . Archivado desde el original el 7 de marzo de 2022.