Ehrig et al. (2006) — Fundamentals of Algebraic Graph Transformation

Paper Summary

This tutorial, based on the EATCS monograph of the same name (Springer, 2006), presents the algebraic approach to graph transformation — a category-theoretic framework for rule-based modification of graphs. Ehrig, Prange, and Ehrig situate graph transformation as the natural generalization of Chomsky grammars (from strings to graphs), term rewriting (from trees to graphs), and textual specification (to visual modeling). The work addresses a fundamental problem: how to define, apply, compose, and reason about graph rewriting rules with formal guarantees.

The core construction is the Double Pushout (DPO) approach, originating from 1973. A graph production (rewriting rule) is a span L <- K -> R, where L is the left-hand side (pattern to match), R is the right-hand side (replacement), and K is the interface (gluing graph) — the substructure preserved by the transformation. Applying a rule requires finding a match morphism m : L -> G in a host graph G, then constructing two pushouts: one that removes m(L) \ m(l(K)) from G to produce a context graph D, and one that glues R \ r(K) onto D to produce the result graph H. The construction is unique up to isomorphism when the gluing condition (identification points and dangling points must be gluing points) is satisfied.

The tutorial develops several major theorems. The Local Church-Rosser Theorem establishes that parallel independent direct transformations (where matched regions overlap only on preserved structure) can be sequentialized in either order and both reach the same result. The Parallelism Theorem provides a bijective correspondence between sequentially independent transformation sequences and parallel transformations via the disjoint union production p1 + p2. The Concurrency Theorem generalizes this to dependent transformations via E-concurrent productions p1 *_E p2, establishing synthesis-analysis correspondence even when transformations share context.

For global properties, the tutorial presents the Critical Pair Lemma: a graph transformation system is locally confluent if and only if all its critical pairs (minimal parallel-dependent overlaps) are strictly confluent. Combined with termination (guaranteed for layered grammars satisfying suitable layer conditions), this yields functional behavior — every graph has a unique normal form.

The work then lifts the entire theory into adhesive HLR categories — a categorical abstraction defined by a class M of monomorphisms satisfying van Kampen square properties. This abstraction is the key theoretical contribution: it unifies graph transformation with hypergraph transformation, Petri net transformation, algebraic specification transformation, and typed attributed graph transformation under a single proof framework. The tutorial shows that product, slice, coslice, comma, and functor category constructions preserve the adhesive HLR property, enabling compositional construction of new suitable categories.

The final sections introduce typed attributed graphs (E-graphs with data algebras), application conditions (constraints on matches), and negative application conditions (NACs) — morphisms x : L -> X that prevent a rule from firing when a larger pattern X is found. NACs are shown to be transformable into equivalent left application conditions on matches, and graph constraints on results can be lifted into equivalent application conditions on productions. The tutorial concludes with an application to visual language modeling (statechart generation) and model transformation (statecharts to Petri nets), demonstrating the framework’s practical applicability via the AGG tool.

Key Concepts

Double Pushout (DPO) construction: Rule application via two categorical pushouts over a span L <- K -> R, giving deletion and addition as universal constructions with uniqueness guarantees.
Gluing condition: Applicability criterion for a production via a match: identification points (nodes/edges identified by the match) and dangling points (nodes with incident edges outside the match image) must all be in the gluing graph K’s image. Necessary and sufficient for context graph existence.
Typed graphs and type graphs: A type graph TG classifies nodes and edges; typed graphs are pairs (G, type : G -> TG). All constructions lift to the typed setting via the comma category GraphsTG.
Parallel and sequential independence: Two direct transformations are parallel independent when their matched regions overlap only on preserved structure. Sequential independence: the comatch of the first overlaps with the match of the second only on preserved structure. The Local Church-Rosser Theorem establishes commutativity under both forms.
Parallelism Theorem: Bijective correspondence between sequentially independent transformation sequences and parallel transformations via disjoint union productions.
Concurrency Theorem: Generalizes parallelism to dependent transformations via E-concurrent productions, with synthesis-analysis bijection.
Critical pairs and local confluence: Minimal parallel-dependent overlaps. A GTS is locally confluent iff all critical pairs are strictly confluent (Critical Pair Lemma). With termination, yields global determinism.
Adhesive HLR categories: Abstract categorical framework — a category C with monomorphism class M satisfying van Kampen square properties. Unified proof substrate for Graphs, Hypergraphs, PTNets, typed attributed graphs, and algebraic specifications.
Negative Application Conditions (NACs): Morphisms x : L -> X constraining rule applicability — a match m satisfies NAC(x) iff no injective extension of m through x exists. Prevents rules from firing when forbidden patterns are present.
Application condition transformation: Graph constraints on result graphs can be transformed into right application conditions on comatches, which can be further transformed into left application conditions on matches, enabling static analysis of rule effects.
Typed attributed graph transformation: Integration of typed graphs with DSIG-algebras for data attributes. The category (AGraphsATG, M) is adhesive HLR, so all theorems apply.

How gen uses this

gen-dispatch

gen-dispatch uses algebraic graph transformation vocabulary for its rule system, applied to Nix’s pure functional evaluation instead of literal graph mutation. Given rules, a position and a context, it answers which rules fire there and what actions they produce. The actions are opaque to gen-dispatch, and their vocabulary belongs to the consumer.

Rule structure as a DPO span analogue. mkRule { nac ? ; identity ? ; priority ? ; overrides ? ; group ? ; produces ? ; } condition produce corresponds to the span L <- K -> R. The condition is the left-hand pattern that a match tests, produce generates the right-hand side actions, and the rule’s identity plays the part of the interface, stable across repeated dispatch.
Match morphism. The caller-supplied match function realises Ehrig’s match morphism m : L -> G. For rules built with fromFunction, builtins.functionArgs gives the context keys the rule requires, which act as the pattern matched against the working context, the host graph. fromFunctionMatch performs that match by checking that every required argument is present.
Negative application conditions. A rule’s nac field implements Ehrig’s NAC(x). Within one group, dispatch filters candidate rules by NAC and condition together, then applies overrides, sorts by priority, applies the exclusive filter, fires the surviving rules and classifies their actions into groups. A rule with a nac fires only when the NAC pattern does not match, which is Ehrig’s “there does not exist an injective p : X -> G with p . x = m”.
Overrides as rule replacement. A rule’s overrides list suppresses named rules by identity, and override { original; replacement; } builds that pairing. This corresponds to controlled deletion in DPO, removing matched structure before adding new structure.
Conflict resolution in place of critical pair analysis. gen-dispatch resolves conflicts by overrides, then priority, then the optional exclusive mode, with declaration order breaking ties deterministically. Ehrig’s critical pairs address the same question, what happens when several rules fire on overlapping structure. The Critical Pair Lemma says local confluence requires every critical pair to be strictly confluent. gen-dispatch reaches determinism through explicit ordering without enumerating critical pairs.
Iteration as a transformation sequence. dispatch is a pure one-shot function of rules and context. Iteration belongs to the caller, which threads domain state through repeated dispatch, for example with gen-scope’s circular, and reads the actions at the fixed point. The sequence G0 => G1 => ... => Gn ends when the state stops changing, a normal form. Because actions are recomputed from the converged state, they depend on that state and not on the path to it.
Rule composition. restrict (narrow the condition), override (replace a rule) and chain (feed A’s actions to B) parallel the tutorial’s production operations: restriction of matches, concurrent productions and E-concurrent sequential composition.
Groups as typed layers. Rules belong to groups, and dispatch walks the groups in a caller-supplied order, completing each before the next. gen-graph computes that order from entryAfter, entryBefore, entryBetween and entryAnywhere constraints. This parallels typed graph transformation systems where the type graph constrains which productions apply in which order.

gen-graph

gen-graph’s edge map operations (unionEdges, intersectEdges, differenceEdges) correspond to the set operations on graph components used in pushout and pullback constructions. Its fixpoint refuses a step whose output does not contain its input, which keeps an iterated transformation monotone.

Rules that change a graph

In a framework built on gen, rules add structure to the scope graph: new nodes, new edges and new declarations. Each rule application corresponds to a DPO application. The rule’s pattern is the match morphism into the current scope context, its emitted actions build the right-hand side, and the existing context that persists across the step is the interface K. Rules that act on disjoint regions commute, as the Local Church-Rosser Theorem states for parallel-independent transformations, and rules with overlapping effects are ordered by group. A terminating, locally confluent system has unique normal forms, which is why the result of rule evaluation does not depend on firing order.

Appendix: Follow-up Work

Unexploited Ideas

Pushout complement construction (Part III, slide 30). The tutorial’s two steps, delete matched elements except the interface and then add new elements, are separate opaque actions in gen-dispatch. A single delete-then-add primitive that preserves the interface would give structural guarantees that consumers currently provide themselves.
Embedding Theorem (Part III, slides 32-34). A transformation extends to a larger graph through consistent morphisms. When context grows, rules are dispatched again. The theorem suggests that when the shared boundary is preserved, the extension can be constructed without re-dispatch, which would allow incremental rule evaluation.
E-concurrent productions (Part IV, slides 42-44). The Concurrency Theorem’s p1 *_E p2 fuses dependent sequential transformations into one production. chain is a manual approximation. A formal E-concurrent construction could fuse rule sequences automatically.
Graph constraints as application conditions (Part VI, slides 64-68). Transforming graph constraints into equivalent left application conditions (H |= c iff m |= lacc) would allow checking, before applying a rule, whether it keeps a well-formedness constraint.
Adhesive HLR generalisation (Part V). gen-dispatch works concretely on Nix attrsets. Formalising those structures as objects of an adhesive HLR category would establish that the classical theorems (Church-Rosser, Parallelism, Concurrency, Critical Pair Lemma) hold for its dispatch.
Typed attributed graph transformation with inheritance (Part VI, slide 69). Inheritance in the type graph, with abstract node types and concrete subtypes, maps to an entity hierarchy: an abstract entity type with concrete host and home subtypes, where rules written for the abstract type apply to every instance.

Potential New Libraries or Features

Static critical pair analysis. Given a rule set, compute all critical pairs (minimal overlapping matches) and check strict confluence, reporting which rule pairs can produce non-confluent results with minimal counterexamples. This implements the Critical Pair Lemma and would catch rule conflicts at definition time. It would consume gen-dispatch rules and gen-select selectors.
Incremental dispatch. Apply the Embedding Theorem: when context grows, determine which earlier results remain valid by checking their boundary, and dispatch again only the rules the change affects. This needs a record of which context elements each dispatch actually read.
Concurrent productions. Fuse sequentially dependent rule pairs into E-concurrent productions. When two rules always fire in sequence and share intermediate structure, a fused rule skips the intermediate state.

Research Directions

Confluence verification. Can a rule set be verified locally confluent statically? The Critical Pair Lemma says to enumerate critical pairs and check strict confluence. Rules over scope graphs may have an infinite critical pair space, and bounded model checking up to a size limit would give practical confidence.
Termination through layer conditions. Ehrig’s termination theorem for layered typed graph grammars needs layer conditions on deleting and non-deleting productions. Rules that only add structure are non-deleting. Formalising dispatch groups as layers and showing each layer’s productions meet the conditions would give a termination proof for rule evaluation.
Nix attrsets as an adhesive HLR category. // is left-biased and so is not a categorical pushout. Attrsets with disjoint keys and union as the pushout likely satisfy the van Kampen square property. Establishing this would let dispatch correctness follow from the categorical framework instead of case-by-case checking.
NAC composition. Ehrig’s NACs are checked individually. Rules often need conjunctions of negative conditions, such as “fire only when aspect X is absent and entity Y has not been created”. Formalising conjunction, disjunction and nesting of NACs, while keeping their transformation into left application conditions, would strengthen gen-dispatch’s constraints.

Palettes adapted from Catppuccin (Macchiato) (MIT), Tokyo Night (Apache-2.0), gruvbox (MIT), Catppuccin (Latte) (MIT), Rosé Pine (Dawn) (MIT).