Unification of drags
Résumé
We develop unification for graph rewriting based on the drag model [8]. 1 Introduction Rewriting with graphs has a long history in computer science, graphs being used to represent data structures, but also program structures and even concurrent and distributed computational models. They therefore play a key rôle in program evaluation, transformation, and optimization, and more generally program analysis; see, for example, [2]. Our work is based on a recent, purely combinatorial view of graphs [8]. Drags are labelled graphs equipped with roots and sprouts. Roots are vertices without predecessors that can be seen as input ports, while sprouts are vertices without successors labelled by variables that can be seen as output ports. Drags appear as a generalization of terms which admit many roots, arbitrary sharing, and cycles. Rewrite rules are then pairs of drags that preserve variables and roots, hence avoiding the creation of dangling edges when rewriting. A key aspect of drags is that they can be equipped with a composition operator so that matching a left-hand side of rule L w.r.t. an input drag D amounts to write D as the composition of a context graph C with L, and rewriting D with the rule L → R amounts to replace L with R in that composition. Since substitutions cannot be separated from context in presence of cycles, composition must play both rôles of plugging a context and a substitution. To assess our claim that drags are a natural generalization of terms, it is our program to extend the most useful term rewriting techniques to drags. The recursive path ordering is extended in [7]. In this paper, we consider unification. First, we generalize the subsumption order to drags thanks to composition. Our main result is then unifiable drags admit a most general unifier which can be computed in quadratic time. Comparisons with the literature is addressed in Section 2. An interesting relationship between unification of drags and of rational dags is pointed out in conclusion.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...