It is well known that every algorithmic problem definable by a formula of first-order logic can be solved in polynomial time, since all these problems are in L (see Aho and Ullman (1979) and Immerman (1987)). Using an old technique of Hanf (Hanf 1965) and other techniques developed to prove the decidability of formal theories in mathematical logic, it is shown that an arbitrary FO-problem over relational structures of bounded degree can be solved in linear time.

We consider the relationship between three ways of defining graph derivability. That the traditional double-pushout approach and Banach's inward version are equivalent in the case of injective left-hand sides is proved in a purely categorical setting. In the case of noninjective left-hand sides, equivalence can be shown in special categories if the right-hand side is injective. Both approaches have the same generative power in the category of graphs if the pushout connecting the outward production with the inward one is a pullback as well. Finally, it is shown that Banach's point of view establishes a close relationship between the categorical approach and Kaplan's Δ-grammars, allowing a slight generalization of Δ-grammars and making them an operational description of the categorical approach.

We show that for every term graph in a left-linear but non-orthogonal term graph rewrite system, one can construct an event structure that represents all the possible reductions that can occur in reduction sequences starting from that term graph. Every finite reduction sequence from that graph corresponds to a configuration of the event structure, and Lévy-equivalent sequences correspond to the same configuration.

Garbage collection is modelled in the event structure by an ‘erases’ relation. The asymmetric conflicts that arise in non-orthogonal rewrite systems are modelled by introducing a ‘prevents’ relation. The configurations of the event structure then form the state space of an event automaton. Taking the directed completion of this space yields a prime algebraic domain.

Using a categorical semantics that has been developed recently as a basis, we study composition and refinement as horizontal and vertical structuring techniques for typed graph transformation systems. Composition of graph transformation systems with respect to common subsystems is shown to be compatible with the semantics, i.e., the semantics of the composed system is obtained as the composition of the semantics of the component systems. Moreover, the structure of a composed graph transformation system is preserved during a refinement step in the sense that compatible refinements of the components induce a refinement of the composition. The concepts and results are illustrated by a sample development of a small information system using entity relationship modelling techniques.

We present two type systems for term graph rewriting: conventional typing and (polymorphic) uniqueness typing. The latter is introduced as a natural extension of simple algebraic and higher-order uniqueness typing. The systems are given in natural deduction style using an inductive syntax of graph denotations with familiar constructs such as let and case.

The conventional system resembles traditional Curry-style typing systems in functional programming languages. Uniqueness typing extends this with reference count information. In both type systems, typing is preserved during evaluation, and types can be determined effectively. Moreover, with respect to a graph rewriting semantics, both type systems turn out to be sound.

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.