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).[1][2] 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[3] y lenguajes de programación declarativa se basan en la reescritura de términos.[4][5]
Ejemplos
[editar]Lógica
[editar]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.[6] Las reglas para un ejemplo de tal sistema serían:
donde el símbolo () 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
[editar]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.[7]
Por ejemplo, el cálculo que 2+2 resuelta en 4 se puede duplicar por reescritura de término de la siguiente manera:
donde el número de la regla se da encima de la flecha de reescritura a (el símbolo ).
Por otro ejemplo, el cálculo de 2⋅2 se hace así:
donde el último paso utiliza el cálculo del ejemplo anterior.
Lingüística
[editar]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,[8] como un medio para generar las oraciones gramaticalmente correctas de un idioma. Tal regla típicamente sigue la forma , 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 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.
Notas
[editar]- ↑ Esta variante de la regla anterior es necesario ya que la ley conmutativa A∨B = B∨A no puede convertirse en una regla de reescritura. Una regla como A∨B → B∨A haría que el sistema de reescritura sea interminable.
Referencias
[editar]- ↑ Joseph Goguen "Proving and Rewriting" International Conference on Algebraic and Logic Programming, 1990 Nancy, France pp 1-24
- ↑ Sculthorpe, Neil; Frisby, Nicolas; Gill, Andy (2014). «The Kansas University rewrite engine». Journal of Functional Programming 24 (4): 434-473. ISSN 0956-7968. doi:10.1017/S0956796814000185. Archivado desde el original el 22 de septiembre de 2017. Consultado el 12 de febrero de 2019.
- ↑ Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël (1992). «The term rewriting approach to automated theorem proving». The Journal of Logic Programming 14 (1–2): 71-99. doi:10.1016/0743-1066(92)90047-7.
- ↑ Frühwirth, Thom (1998). «Theory and practice of constraint handling rules». The Journal of Logic Programming 37 (1–3): 95-138. doi:10.1016/S0743-1066(98)10005-5.
- ↑ Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J.F. (2002). «Maude: Specification and programming in rewriting logic». Theoretical Computer Science 285 (2): 187-243. doi:10.1016/S0304-3975(01)00359-0.
- ↑ Kim Marriott; Peter J. Stuckey (1998). Programming with Constraints: An Introduction. MIT Press. pp. 436-. ISBN 978-0-262-13341-8.
- ↑ Jürgen Avenhaus; Klaus Madlener (1990). «Term Rewriting and Equational Reasoning». En R.B. Banerji, ed. Formal Techniques in Artificial Intelligence. Sourcebook. Elsevier. pp. 1-43. Here: Example in sect.4.1, p.24.
- ↑ Robert Freidin (1992). Foundations of Generative Syntax. MIT Press. ISBN 978-0-262-06144-5.