Search

To verify graph programs in the language GP 2, we present a monadic second-order logic with counting and a Hoare-style proof calculus. The logic has quantifiers for GP 2’s attributes and for sets of nodes or edges. This allows to specify non-local graph properties such as connectedness, k-colourability, etc. We show how to construct a strongest liberal postcondition for a given graph transformation rule and a precondition. The proof rules establish the total correctness of graph programs and are shown to be sound. They allow to verify more programs than is possible with previous approaches. In particular, many programs with nested loops are covered by the calculus.

The transformation of graphs and graph-like structures is ubiquitous in computer science. When a system is described by graph-transformation rules, it is often desirable that the rules are both terminating and confluent so that rule applications in an arbitrary order produce unique resulting graphs. However, there are application scenarios where the rules are not globally confluent but confluent on a subclass of graphs that are of interest. In other words, non-resolvable conflicts can only occur on graphs that are considered as “garbage”. In this paper, we introduce the notion of confluence up to garbage and generalise Plump’s critical pair lemma for double-pushout graph transformation, providing a sufficient condition for confluence up to garbage by non-garbage critical pair analysis. We apply our results to language recognition by backtracking-free graph reduction, showing how to establish that a graph language can be decided by a system which is confluent up to garbage. We present two case studies with backtracking-free graph reduction systems which recognise a class of flow diagrams and a class of labelled series-parallel graphs, respectively. Both systems are non-confluent but confluent up to garbage.

We present the foundations of critical pair analysis for the graph programming language GP 2. Our goal is to develop a static checker that can prove or refute confluence (functional behaviour) for a large class of graph programs. In this paper, we introduce symbolic critical pairs of GP 2 rule schemata, which are labelled with expressions, and establish the completeness and finiteness of the set of symbolic critical pairs over a finite set of rule schemata. We give a procedure for their construction.

We present an approach to attributed graph transformation which requires neither infinite graphs containing data algebras nor auxiliary edges that link graph items with their attributes. Instead, we use the double-pushout approach with relabelling and extend it with rule schemata which are instantiated to ordinary rules prior to application. This framework provides the formal basis for the graph programming language GP 2. In this paper, we abstract from the data algebra of GP 2, define parallel independence of rule schema applications, and prove the Church-Rosser Theorem for our approach. The proof relies on the Church-Rosser Theorem for partially labelled graphs and adapts the classical proof by Ehrig and Kreowski, bypassing the technicalities of adhesive categories.

We review the concept of term graph narrowing as an approach for solving equations by transformations on term graphs. Term graph narrowing combines term graph rewriting with first-order term unification. This mechanism is complete for all term rewriting systems over which term graph rewriting is normalizing and confluent. This includes, in particular, all convergent term rewriting systems. Completeness means that for every solution of a given equation, term graph narrowing can find an equivalent or more general solution. The general motivation for using term graphs instead of terms is to improve efficiency: sharing common subterms saves space and avoids the repetition of computations.

Term graph rewriting is a model for computing with graphs representing functional expressions. Graphs allow to share common subexpressions which improves the efficiency of conventional term rewriting in space and time. This article reviews essentials of term graph rewriting concerning soundness, completeness, termination and confluence.

It is shown that it is undecidable in general whether a graph rewriting system (in the “double pushout approach”) is terminating. The proof is by a reduction of the Post Correspondence Problem. It is also argued that there is no straightforward reduction of the halting problem for Turing machines or of the termination problem for string rewriting systems to the present problem.

We introduce term graph narrowing as an approach for solving equations by transformations on term graphs. Term graph narrowing combines term graph rewriting with first-order term unification. Our main result is that this mechanism is complete for all term rewriting systems over which term graph rewriting is normalizing and confluent. This includes, in particular, all convergent term rewriting systems. Completeness means that for every solution of a given equation, term graph narrowing can find a more general solution. The general motivation for using term graphs instead of terms is to improve efficiency: sharing common subterms saves space and avoids the repetition of computations.

We present Hoare-style axiom schemata and inference rules for verifying the partial correctness of programs in the graph programming language GP. The pre- and postconditions of this calculus are the nested conditions of Habel, Pennemann and Rensink, extended with expressions for labels in order to deal with GP's conditional rule schemata and infinite label alphabet. We show that the proof rules are sound with respect to GP's operational semantics.

Jungle evaluation is proposed as a new graph rewriting approach to the evaluation of functional expressions and, in particular, of algebraically specified operations. Jungles – being intuitively forests of coalesced trees with shared substructures – are certain acyclic hypergraphs (or equivalently, bipartite graphs) the nodes and edges of which are labeled with the sorts and operation symbols of a signature. Jungles are manipulated and evaluated by the application of jungle rewrite rules, which generalize equations or, more exactly, term rewrite rules. Indeed, jungle evaluation turns out to be a compromise between term rewriting and graph rewriting displaying some favorable properties: the inefficiency of term rewriting is partly avoided while the possibility of structural induction is maintained, and a good part of the existing graph grammar theory is applicable so that there is some hope that the rich theory of term rewriting is not lost forever without a substitute.

Term rewriting is commonly implemented by graph reduction in order to improve efficiency. In general, however, graph reduction is not complete: a term may be not normalizable through graph derivations although a normal form exists. Term rewriting systems which permit a complete implementation by graph reduction are called graph-reducible. We show that the following property is sufficient for graph-reducibility: every term having a normal form can be normalized by parallel term rewrite steps in which a rule is applied to all occurrences of some subterm. As a consequence, a broad class of term rewriting systems which includes all terminating and all orthogonal systems can be shown to be graph-reducible.

It is shown that it is undecidable in general whether a terminating graph rewriting system is confluent or not—in contrast to the situation for term and string rewriting systems. Critical pairs are introduced to hypergraph rewriting, a generalisation of graph rewriting, where it turns out that the mere existence of common reducts for all critical pairs of a graph rewriting system does not imply local confluence. A Critical Pair Lemma for hypergraph rewriting is then established which guarantees local confluence if each critical pair of a system has joining derivations that are compatible in that they map certain nodes to the same nodes in the common reduct.

This paper presents an abstract framework and multiple diagram-based methods for proving meaning preservation, i.e., that all rewrite steps of a rewriting system preserve the meaning given by an operational semantics based on a rewriting strategy. While previous rewriting-based methods have generally needed the treated rewriting system as a whole to have such properties as, e.g., confluence, standardization, and/or termination or boundedness of developments, our methods can work when all of these conditions fail, and thus can handle more rewriting systems. We isolate the new lift/project with termination diagram as the key proof idea and show that previous rewriting-based methods (Plotkin's method based on confluence and standardization and Machkasova and Turbak's method based on distinct lift and project properties) implicitly use this diagram. Furthermore, our framework and proof methods help reduce the proof burden substantially by, e.g., supporting separate treatment of partitions of the rewrite steps, needing only elementary diagrams for rewrite step interactions, excluding many rewrite step interactions from consideration, needing weaker termination properties, and providing generic support for using developments in combination with any method.

Term graph rewriting differs from term rewriting in that common subexpressions can be shared, improving the efficiency of rewriting in space and time. Moreover, computations by term graph rewriting terminate more often than computations by term rewriting. In this paper, simplification orders on term graphs are introduced as a means for proving termination of term graph rewriting. Simplification orders are based on an extension of the homeomorphic embedding relation from trees to term graphs. By generalizing Kruskal's Tree Theorem to term graphs, it is shown that simplification orders are well-founded. Then a recursive path order on term graphs is defined by analogy with the well-known order on terms, and is shown to be a simplification order. Examples of termination proofs with the recursive path order are given for rewrite systems that are non-terminating under term rewriting.

A necessary and sufficient condition for termination of graph rewriting systems is established. Termination is equivalent to the finiteness of all forward closures, being certain minimal derivations in which each step depends on previous steps. This characterization differs from corresponding results for term rewriting in that the latter hold only for subclasses of term rewriting systems. When applied to term graph rewriting, the result characterizes termination of arbitrary term rewriting systems under graph rewriting. In particular, it captures non-terminating term rewriting systems that are terminating under graph rewriting.

Term graphs represent functional expressions such that common subexpressions can be shared, making expression evaluation more efficient than with strings or trees. Rewriting of term graphs proceeds by both applications of term rewrite rules and folding steps which enhance the degree of sharing. The present paper introduces critical pairs in term graph rewriting and establishes a Critical Pair Lemma as an analogue to the well-known result in term rewriting. This leads to a decision procedure for confluence in the presence of termination. As a by-product, the procedure can be used as a confluence test for term rewriting and as such it extends the classical test of Knuth and Bendix because it applies to all terminating and to certain non-terminating term rewriting systems.

Collapsed trees are (hyper)graphs which represent functional expressions such that common subexpressions can be shared. Rewrite steps with collapsed trees include applications of term rewrite rules as well as “folding steps” which identify common subexpressions. Different aspects of this model of computation are considered: (1) It is shown that collapsed tree rewriting is complete with respect to equational validity in the same sense as term rewriting is. (2) Collapsed tree rewriting and term rewriting are compared with respect to confluence. (3) Termination and convergence of collapsed tree rewriting turn out to be modular properties, in contrast to the situation for term rewriting.

We present a survey of confluence properties of (acyclic) term graph rewriting. Results and counterexamples are given for four different kinds of term graph rewriting: besides plain applications of rewrite rules, extensions with the operations of collapsing and copying, and with both operations together are considered. Collapsing and copying together constitute bisimilarity of term graphs. We establish sufficient conditions for, and counterexamples to, confluence and confluence modulo bisimilarity of term graph rewriting over various classes of term rewriting systems.