En informática , la reescritura de grafos con doble empuje (o reescritura de grafos DPO) se refiere a un marco matemático para la reescritura de grafos . Se introdujo como uno de los primeros enfoques algebraicos para la reescritura de grafos en el artículo "Gramáticas de grafos: un enfoque algebraico" (1973). [1] Desde entonces se ha generalizado para permitir la reescritura de estructuras que no son grafos y para manejar condiciones de aplicación negativas, [2] entre otras extensiones.
Un sistema de transformación de grafos DPO (o gramática de grafos ) consta de un grafo finito , que es el estado inicial, y un conjunto finito o contable de intervalos etiquetados en la categoría de grafos finitos y homomorfismos de grafos, que sirven como reglas de derivación. Generalmente se considera que los intervalos de las reglas están compuestos de monomorfismos , pero los detalles pueden variar. [3]
La reescritura se realiza en dos pasos: eliminación y adición.
Después de que se fija una coincidencia del lado izquierdo , se eliminan los nodos y los bordes que no están en el lado derecho. Luego se pega el lado derecho.
Pegar gráficos es, de hecho, una construcción de pushout en la categoría de gráficos, y la eliminación es lo mismo que encontrar un complemento de pushout, de ahí el nombre.
La reescritura de gráficos con doble inserción permite la especificación de transformaciones de gráficos al especificar un patrón de tamaño y composición fijos que se debe buscar y reemplazar, donde se puede conservar parte del patrón. La aplicación de una regla es potencialmente no determinista: pueden ser posibles varias coincidencias distintas. Estas pueden no superponerse o compartir solo elementos conservados, mostrando así un tipo de concurrencia conocida como independencia paralela, [4] o pueden ser incompatibles, en cuyo caso, o bien las aplicaciones a veces se pueden ejecutar secuencialmente, o bien una puede incluso excluir a la otra.
Se puede utilizar como lenguaje para el diseño y programación de software (normalmente se elige una variante que trabaje con estructuras más ricas que los grafos). La terminación para la reescritura de grafos DPO es indecidible porque el problema de correspondencia de Post se puede reducir a ella. [5]
La reescritura del gráfico DPO puede verse como una generalización de las redes de Petri . [4]
Se han buscado axiomas para describir categorías en las que funcionará la reescritura de DPO. Una posibilidad es la noción de categoría adhesiva , que también disfruta de muchas propiedades de cierre. Nociones relacionadas son los sistemas HLR, categorías cuasiadhesivas y categorías -adhesivas, categorías HLR adhesivas. [6]
Los conceptos de categoría adhesiva y sistema HLR están relacionados (una categoría adhesiva con coproductos es un sistema HLR [7] ).
Por ejemplo, la reescritura de hipergrafos , gráficos tipificados y gráficos atribuidos [8] se pueden manejar porque se pueden convertir en sistemas HLR adhesivos.