Redundancy and subsumption in high-level replacement systems
Abstract
System verification in the broadest sense deals with those semantic properties that can be decided or deduced by analyzing a syntactical description of the system. Hence, one may consider the notions of redundancy and subsumption in this context as they are known from the area of rule-based systems. A rule is redundant if it can be removed without affecting the semantics of the system; it is subsumed by another rule if each application of the former one can be replaced by an application of the latter one with the same effect. In this paper, redundancy and subsumption are carried over from rule-based systems to high-level replacement systems, which in turn generalize graph and hypergraph grammars. The main results presented in this paper are a characterization of subsumption and a sufficient condition for redundancy, which involves composite productions.
Full text
Redundancy and Subsumption in High-Level Replacement Systems H.-J. Kreowski1,G.Valiente 1,2 1Mathematics and Computer Science Department, University of Bremen, Germany 2Department of Software, Technical University of Catalonia, Catalonia, Spain Abstract. System verification in the broadest sense deals with those semantic properties that can be decided or deduced by analyzing a syntactical description of the system. Hence, one may consider the notions of redundancy and subsumption in this context as they are known from the area of rule-based systems. A rule is redundant if it can be removed without affecting the semantics of the system; it is subsumed by another rule if each application of the former one can be replaced by an application of the latter one with the same effect. In this paper, redundancy and subsumption are carried over from rule-based systems to high-level replacement systems, which in turn generalize graph and hypergraph grammars. The main results presented in this paper are a characterization of subsumption and a sufficient condition for redundancy, which involves composite productions. 1 Introduction High-level replacement systems [6] generalize the algebraic approach to graph transformation, both the double-pushout approach [3] and the single-pushout approach [5], to other classes of replacement systems. They provide a common categorical framework for different classes of replacement systems, such as grammars on graphs, relational structures, and algebraic specifications, based on categories and pushouts. This paper deals with aspects of verification of both double-pushout (DPO) and single-pushout (SPO) high-level replacement systems. System verification in the broadest sense is concerned with those semantic properties that can be decided or deduced by analyzing a syntactical description of the system. The properties studied in this paper are redundancy and subsumption, as they are known from the area of rule-based systems (see, for instance, [2], [8], [9]). Consider a high-level replacement system, that is, a set of productions, an initial object, and a class of terminal objects. A production is subsumed by another if any application of the former is mimicked by the latter. As a first result, Partially supported by the EC TMR Network GETGRATS (General Theory of Graph Transformation Systems) and by the ESPRIT Basic Research Working Group APPLIGRAPH (Applications of Graph Transformation) through the University of Bremen, and by the Spanish DGES project PB96-0191-C02.
we present a sufficient condition for subsumption. If a production pis covered by a production p,thatis,pis directly derived by p,thenpis also subsumed by p. This is interesting because covering is easier to check than subsumption, since it is defined by a single direct derivation. It turns out that covering is not only sufficient, but also necessary for subsumption in the case of single-pushout highlevel replacement systems, whereas this is not true in the double-pushout case. Moreover, we consider subsumption of a production by composite productions. Even in this case, one can show that the subsumed production is redundant, that is, the semantics of the given system does not change if the production is removed. Altogether, one obtains a procedure that removes some redundancy from a given system: Enumerate composite productions, check them for covering, and remove every covered production. 2 High-Level Replacement Systems In this section, we recall the basic notions and notations of high-level replacement systems the rewriting of which is based on both double-pushout (DPO)and single-pushout (SPO)constructions. Starting with the DPO case, let Cbe a category, whose objects will be regarded as high-level structures and whose morphisms will be regarded as structurepreserving mappings between these objects. The morphisms in a distinguished class Mwill be used in productions, while general morphisms in Cwill be used to define application of productions to high-level structures. Definition 1 (DPO HLR system). Let Cbe a category with a distinguished class Mof morphisms. 1. A DPO production p=(L←K→R)in Cconsists of a pair of objects (L, R),calledleft-hand side object and right-hand side object respectively, an object K,calledinterface object, and two morphisms K→Land K→R belonging to M. 2. An object Gcan be directly derived into an object Husing a DPO production p=(L←K→R), denoted by G⇒Hvia pif there are pushout squares L K o o / / R GD o o / / H in C. 3. Let P be a set of DPO productions. A derivation G⇒∗Hfrom Gto Hin P is a sequence of n⩾0direct derivations G=G0⇒G1⇒···⇒Gn=H via (p1,...,p n)provided that p1,...,p n∈ P . 4. A high-level replacement system H=(S, P , T )in Cconsists of a start object Sin C,aset P of DPO productions, and a class T of terminal objects in C.
5. The language L(H)of a high-level replacement system H=(S, P , T ),also denoted by L(S, P , T ), is given by the set of all terminal objects in Cderivable from Sby P , that is, L(H)={G∈ T |S⇒∗G}. The following example presents high-level replacement system (which is actually a graph grammar) that allows the generation and recognition of all Eulerian graphs, based on [10, Sect. 3.2]. Recall that a graph is Eulerian if it has an Euler circuit, that is, a circuit that contains every edge of the graph exactly once. Eulerian graphs are characterized by being connected and having only nodes of even degree [1]. Example 2. Let Cbe the category of undirected graphs and Mbe the class of all injective graph morphisms. Consider the following double-pushout high-level replacement system (S, P,T) for generating and recognizing all Eulerian graphs, where Sis a graph with a single node and no arc, P={p1,...,p 9},andTis the class of all graphs. LKR p1 LKR p2 LKR p3 LKR p4 LKR p5 LKR p6 LKR p7 LKR p8 LKR p9 The dotted lines indicate the morphisms from the interface object to the lefthand side object and to the right-hand side object, respectively. The SPO case differs from the DPO case in two aspects: A production consists of a single morphism and a direct derivation of a single pushout. In typical examples like graphs, the morphism of a production may be a partial mapping (where nodes and edges outside the domain of definition specify the items to be removed) while the occurrence of the left-hand side in the host graph should be a total mapping. To formalize such situations, a category and a subcategory are assumed. Definition 3 (SPO HLR system). Let Cbe a category and let Obe a subcategory of Csuch that Ocoincides with Con objects.
1. An SPO production p=(L→R)in Cconsists of a pair of objects (L, R), called left-hand side object and right-hand side object respectively, and a morphism L→Rin C. 2. An object Gcan be directly derived into an object Husing an SPO production p=(L→R), denoted by G⇒Hvia pif there is a pushout square L / / R G / / H in Csuch that L→Gis in O. 3. Let P be a set of SPO productions. A derivation G⇒∗Hfrom Gto Hin P is a sequence of n⩾0direct derivations G=G0⇒G1⇒···⇒Gn=H via (p1,...,p n)provided that p1,...,p n∈ P . 4. A high-level replacement system H=(S, P , T )in Cconsists of a start object Sin C,aset P of SPO productions, and a class T of terminal objects in C. 5. The language L(H)of a high-level replacement system H=(S, P , T ),also denoted by L(S, P , T ), is given by the set of all terminal objects in Cderivable from Sby P , that is, L(H)={G∈ T |S⇒∗G}. Example 4. If one ignores the interface graphs in the productions of Example 2 and interprets the dotted lines as inclusions of the left-hand side nodes into the right-hand side nodes, one obtains SPO productions in the category of graphs with partial graph morphisms. Choosing the category of graphs with total graph morphisms as subcategory, the application of an SPO production has the same effect as the application of the corresponding DPO production, that is, the edges of the left-hand side are removed and the right-hand side is added by merging the related nodes. 3 Redundancy and subsumption Verification of high-level replacement systems is concerned with formal properties of the systems. Some of the formal properties to be verified arise from the rule-based paradigm itself; cf. [10]. In particular, redundancy and subsumption are generalized in this section from rule-based systems to high-level replacement systems. A high-level replacement system is redundant if it contains a production that can be removed without affecting the semantics of the system. In particular, such productions may be subsumed by other productions. A production subsumes (or is more general than) another production if the subsuming production can be applied and it yields the same result whenever the subsumed production can be applied. Definition 5 (Redundancy and Subsumption). Let P be a set of productions (either of the DPO or SPO type).
1. A production q∈ P is redundant if there is a derivation G⇒∗Hin P −{q} whenever there is a derivation G⇒∗Hin P . 2. A production p∈ P subsumes aproductionq∈ P , denoted by p⩽q,ifthere is a direct derivation G⇒Hvia pwhenever there is a direct derivation G⇒Hvia q. Obviously, a production qis redundant if it is subsumed by a production p. Moreover, a high-level replacement system H=(S, P,T) for some start object Sand class of terminal objects Tgenerates the same language as H−q= (S, P−{q},T)ifqis redundant or, in particular, if qis subsumed by some p∈ P−{q}. The other way round, a production q∈Pis redundant if L(S, P,T)= L(S, P−{q},T) for any start object Sand any class Tof terminal objects. Example 6. Productions p6to p9in Example 2 are redundant. Production p6 is subsumed by production p5, and productions p7and p8are subsumed by production p4. Production p9is discussed in Example 16. Redundancy and subsumption may be undesirable for several reasons. First, the presence of redundant and subsumed productions may degrade execution efficiency. Second, and most important, it may make system validation more difficult. 4 A characterization of subsumption Subsumption can be regarded as a local form of redundancy, since it only involves two productions: the subsuming production and the subsumed production. Nevertheless, subsumption is difficult to check because the definiton involves arbitrary objects to be derived by the involved productions. To avoid this obstacle, we introduce the notion of a covering, which relates two productions by means of a single direct derivation and is, therefore, much easier to check. Using the sequential composition of pushouts, covering can be shown to imply subsumption. Moreover, it turns out that covering and subsuption are equivalent notions in the SPO case, but not in the DPO case. Definition 7 (Covering in DPO HLR systems). Production p=(L←K→ R)coversproduction p=(L←K→R)if there exist morphisms L→L, K→Kand R→Rsuch that L→L←Kis a pushout of L←K→Kand K→R←Ris a pushout of K←K→R. L (PO) K o o / / (PO) R LK o o / / R Theorem 8. Let p=(L←K→R)and p=(L←K→R)be two productions. Then p⩽pif pcovers p.
Proof. Consider a direct derivation G⇒Hvia pof the form L K o o / / R GD o o / / H By hypothesis, there exist pushout squares (1) and (2), and by (vertical) composition of pushout squares, there also exist pushout squares (3) and (4), that is, there exists a direct derivation G⇒Hvia p. L (1) K o o / / (2) R LK o o / / R L (3) K o o / / (4) R GD o o / / H Observation 9. There are DPO productions pand psuch that p⩽p,butp does not cover p. Proof. Consider the following counter-example in the category Gra of graphs and graph morphisms. Let p=(•←•→•)andp=(•←∅→•)betwo productions given by identities and by empty morphisms, respectively. There exists a derivation G⇒Hvia pif and only if the left-hand side node is mapped to an isolated node of G. Moreover, in this case, we have H=Gbecause the isolated node is removed and added again. Using the same occurrence, we obtain a derivation G⇒Gvia p.Inotherwords,p⩽p. However, pdoes not cover pbecause there is no morphism •→∅in Gra, and, therefore, no double pushout of the form • • o o / / • •∅ o o / / • In the case of single-pushout high-level replacement systems, however, subsumption is characterized by covering. Definition 10 (Covering in SPO HLR systems). Production p=(L→R) covers production p=(L→R)if there exist morphisms L→Lin Oand R→Rsuch that L→R←Ris a pushout of L←L→R. L / / (PO) R L / / R
Theorem 11. Let p=(L→R)and p=(L→R)be two productions. Then p⩽pif and only if pcovers p. Proof. (If part) Consider a direct derivation G⇒Hvia pof the form L / / R G / / H By hypothesis, there exists pushout square (1), and by (vertical) composition of pushout squares, there also exists pushout square (2), since the composition of morphism L→Lwith morphism L→Gis also in O. That is, there exists a direct derivation G⇒Hvia p. L / / (1) R L / / R L / / (2) R G / / H (Only-if part) Since the hypothesis holds for any direct derivation through production p, in particular it holds for the direct derivation L⇒Rvia p, that is, for the direct derivation given by pushout square (1) where the vertical morphisms are the identities. Then, there also exists a direct derivation L⇒R via p, that is, there exist morphisms L→Land R→Rsuch that square (2) is a pushout square. Then pcovers p. L / / (1) R L / / R L / / (2) R L / / R Contrary to the case of (linear) rule-based systems, however, mutual subsumption does not mean isomorphic productions. Observation 12. p⩽pand p⩽pdoes not imply p=p. Proof. Consider the following counter-example in the category Set of sets and functions. Let A={a}and B={b, c}be two sets, and let p=(A, A, A)and
p=(B, B, B) be two double-pushout productions given by identities. LKR p=( a (1) a o o / / (2) a ) p=( b b o o / / b c (3) c o o / / (4) c ) p=( aa o o / / a) There exist morphisms L→L,K→Kand R→Rgiven by a→ bsuch that (1) and (2) become pushout squares, and there exist morphisms L→L, K→Kand R→Rgiven by b→ a, c → asuch that (3) and (4) also become pushout squares. However, pand pare not isomorphic productions. A similar counter-example applies to single-pushout productions. 5 A sufficient condition for redundancy While subsumption between productions of a high-level replacement system can be regarded as a local form of redundancy, one obtains more global forms of redundancy by the combination and composition of several production to subsume other productions. Actually, the most general notion of composition is given by the construction of concurrent productions, which consists of the composition of two productions over a dependency relation Dbetween the right-hand side object of the first production and the left-hand side object of the second production. The resulting composite production is called D-concurrent production. We recall the notion for double-pushout high-level replacement systems as given in [4]. To guarantee that all necessary constructions exist, we assume so-called HLR2 categories, which are defined in the Appendix (according to [6]). Definition 13 (Concurrent DPO production). 1. Let p=(L←K→R)and p=(L←K→R)be two productions and let Dbe an object together with two morphisms D→Rand D→L.Thepair (D→R, D →L), or short D,iscalledadependency relation for (p, p) if the pushout object H∗of D→Rand D→Lexists and if there are unique pushout complements of K→R→H∗and K→L→H∗up to isomorphism. 2. Given a dependency relation (D→R, D →L)for (p, p),theD-concurrent production p∗Dp=(L∗←K∗→R∗)of pand pis given by the construc-
tion in the following diagram, where: D ~ ~ | | | | | | | | ! ! B B B B B B B B (1) L (3) K o o / / (2) R A A A A A A A A L ~ ~ | | | | | | | | (2) K o o / / (3) R L∗C∗ o o / / (=) H∗ (4) C∗ o o / / (=) R∗ K∗ d d h h P P P P P P P P P P P P P P 6 6 m m m m m m m m m m m m m m : : (a) H∗is the pushout object in diagram (1); (b) C∗and C∗are the pushout complements in diagrams (2) and (2),respectively; (c) L∗and R∗are the pushout objects in diagrams (3) and (3), respectively; and (d) K∗isthepullbackobjectindiagram(4) with K∗→L∗=K∗→C∗→ L∗and K∗→R∗=K∗→C∗→R∗. 3. Two productions p=(L←K→R)and p=(L←K→R)are composable if there exists a dependency relation Dfor (p, p),andinsucha case their composite production is given by the D-concurrent production p∗Dp=(L∗←K∗→R∗).IfDis not needed explicitly, the composite production is denoted by p∗p. Notice that two productions are always composable if Chas an initial object, which is the case of a HLR2 category; see the Appendix. The D-concurrent production p∗Dpbecomes the parallel composition p+pwhen Dis the initial object in C. A special case of composition, namely via a dependency relation D=L, is particularly interesting from a verification point of view, since the matching algorithm of the high-level replacement system can then be used to test for redundant productions, namely by finding a match of Lin R. L (PO) K o o / / (PO) R LK o o / / R (PB) K o o / / R K a a C C C C C C C C < < y y y y y y y y Using the following fact, which is proved for double-pushout high-level replacement systems in [4] as analysis step of the so-called Concurrency Theorem, we can show that a production qis redundant if it is subsumed by a composite production.