Sistema de reescritura abstracta


En lógica matemática e informática teórica , un sistema de reescritura abstracta (también sistema de reducción (abstracto) o sistema de reescritura abstracta ; ARS abreviado ) es un formalismo que captura la noción y propiedades por excelencia de los sistemas de reescritura . En su forma más simple, un ARS es simplemente un conjunto (de "objetos") junto con una relación binaria , tradicionalmente denotada con ; esta definición se puede refinar aún más si indexamos (etiquetamos) subconjuntos de la relación binaria. A pesar de su simplicidad, un ARS es suficiente para describir propiedades importantes de sistemas de reescritura comoformas normales , terminación y diversas nociones de confluencia .

Históricamente, ha habido varias formalizaciones de reescritura en un entorno abstracto, cada una con sus idiosincrasias. Esto se debe en parte al hecho de que algunas nociones son equivalentes, ver más abajo en este artículo. La formalización que se encuentra más comúnmente en monografías y libros de texto, y que generalmente se sigue aquí, se debe a Gérard Huet (1980). [1]

Un sistema de reducción abstracto ( ARS ) es la noción más general (unidimensional) sobre la especificación de un conjunto de objetos y reglas que se pueden aplicar para transformarlos. Más recientemente, los autores también utilizan el término sistema de reescritura de resúmenes . [2] (La preferencia por la palabra "reducción" en lugar de "reescritura" constituye una desviación del uso uniforme de "reescritura" en los nombres de sistemas que son particularizaciones de ARS. Porque la palabra "reducción" no aparece en los nombres de los sistemas más especializados, en los textos más antiguos sistema de reducción es sinónimo de ARS). [3]

Un ARS es un conjunto A , cuyos elementos generalmente se denominan objetos, junto con una relación binaria en A , tradicionalmente denotada por →, y llamada relación de reducción , relación de reescritura [2] o simplemente reducción . [3] Esta terminología (arraigada) que usa "reducción" es un poco engañosa, porque la relación no necesariamente reduce alguna medida de los objetos.

En algunos contextos, puede ser beneficioso distinguir entre algunos subconjuntos de las reglas, es decir, algunos subconjuntos de la relación de reducción →, por ejemplo, la relación de reducción completa puede consistir en reglas de asociatividad y conmutatividad . En consecuencia, algunos autores definen la relación de reducción → como la unión indexada de algunas relaciones; por ejemplo si , la notación utilizada es (A, → 1 , → 2 ).

Como objeto matemático, un ARS es exactamente lo mismo que un sistema de transición de estado sin etiquetar , y si la relación se considera una unión indexada, entonces un ARS es lo mismo que un sistema de transición de estado etiquetado con los índices como etiquetas. Sin embargo, el enfoque del estudio y la terminología son diferentes. En un sistema de transición de estado, uno está interesado en interpretar las etiquetas como acciones, mientras que en un ARS el enfoque está en cómo los objetos pueden transformarse (reescribirse) en otros. [4]


Ejemplo de un sistema de reescritura localmente confluente que no tiene la propiedad Church-Rosser