Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms

Detlef Plump; Ziad Ismaili Alaoui

arxiv: 2501.09144 · v5 · pith:3MNHSTRVnew · submitted 2025-01-15 · 💻 cs.PL · cs.PF

Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms

Ziad Ismaili Alaoui , Detlef Plump This is my paper

Pith reviewed 2026-05-23 05:06 UTC · model grok-4.3

classification 💻 cs.PL cs.PF

keywords graph programmingGP 2time complexityconnectivityacyclicityshortest pathsBellman-Fordrule-based algorithms

0 comments

The pith

Enhanced graph data structures let GP 2 programs check connectivity and acyclicity in linear time and solve shortest paths in O(nm) time on arbitrary graphs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that three rule-based programs written in the graph programming language GP 2 achieve the same asymptotic running times as standard imperative implementations of connectivity testing, acyclicity testing, and single-source shortest paths. The first two programs run in linear time even when input graphs are disconnected or have unbounded node degrees. The third program runs in O(nm) time, matching the Bellman-Ford bound, again without restrictions on the input. Correctness and complexity are proved formally for each program, and the results rest on an improved graph representation produced by the GP 2 compiler together with new ways of writing the rules that exploit that representation.

Core claim

By extending the graph data structure generated by the GP 2 compiler, the authors implement three programs whose running times match those of imperative algorithms: linear time for connectivity and acyclicity on possibly disconnected graphs of arbitrary degree, and O(nm) time for single-source shortest paths with integer weights on arbitrary graphs.

What carries the argument

The enhanced graph data structure produced by the GP 2 compiler, which supplies the constant-time and amortized-efficient primitives needed for the rule applications in the three programs.

If this is right

Connectivity and acyclicity testing become linear-time tasks inside the GP 2 language without degree or connectivity restrictions.
Single-source shortest paths become an O(nm) task inside GP 2 on arbitrary weighted graphs.
Rule-based graph programs can now be shown to compete directly with imperative code on three fundamental graph problems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same data-structure change may allow additional graph algorithms to be expressed efficiently in GP 2.
If the compiler extension generalizes, other rule-based languages could adopt similar structures to close the complexity gap with imperative code.
Runtime experiments on varied graph classes already indicate practical viability; further classes could be tested to map the practical range.

Load-bearing premise

The enhanced graph data structure supports the needed operations in constant or amortized time with no hidden costs that would push the programs beyond linear or O(nm) bounds on arbitrary inputs.

What would settle it

A concrete counter-example graph (for example a high-degree disconnected graph) on which one of the first two programs exceeds linear time or the shortest-path program exceeds O(nm) time.

read the original abstract

We report on recent advances in rule-based graph programming, which allow us to match the time complexity of some fundamental imperative graph algorithms. In general, achieving the time complexity of graph algorithms implemented in conventional languages using a rule-based graph-transformation language is challenging due to the cost of graph matching. Previous work demonstrated that with rooted rules, certain algorithms can be implemented in the graph programming language GP 2 such that their runtime matches the time complexity of imperative implementations. However, this required input graphs to have a bounded node degree and (for some algorithms) to be connected. In this paper, we overcome these limitations by enhancing the graph data structure generated by the GP 2 compiler and exploiting the new structure in programs. We present three case studies: the first program checks whether input graphs are connected, the second program checks whether input graphs are acyclic, and the third program solves the single-source shortest-paths problem for graphs with integer edge-weights. The first two programs run in linear time on (possibly disconnected) input graphs with arbitrary node degrees. The third program runs in time $O(nm)$ on arbitrary input graphs, matching the time complexity of imperative implementations of the Bellman-Ford algorithm. For each program, we formally prove its correctness and time complexity, and provide runtime experiments on various graph classes.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

GP 2 now matches imperative time bounds for connectivity, acyclicity, and SSSP on arbitrary graphs via a compiler data-structure upgrade and three new programs with proofs.

read the letter

The paper's core advance is removing the bounded-degree and connectedness limits that earlier GP 2 work needed for linear-time results. By changing the graph representation the compiler produces, the authors give programs that check connectivity and acyclicity in linear time and solve single-source shortest paths in O(nm) time on any input graph, matching Bellman-Ford. They supply the actual programs, formal proofs of correctness and complexity, and runtime measurements on varied graph families. That combination is what makes the claim concrete rather than hand-wavy. The data-structure change is the real technical step; the rest follows from using it in the rules. The proofs are presented as covering the new operations, and the experiments give some empirical backing. If the proofs are tight, this is a useful step for anyone trying to keep graph-transformation languages competitive on standard algorithms. The main soft spot is that the efficiency claims rest entirely on those proofs correctly accounting for every operation on high-degree or disconnected graphs; any hidden linear factor in the new structure would break the stated bounds. Nothing in the abstract suggests an inconsistency, but the argument is only as strong as the detailed proof steps. This work is aimed at researchers in graph transformation and declarative graph algorithms. Readers who care about making rule-based systems run at the same speed as imperative ones on core problems will get direct value from the programs and proofs. It is worth sending to peer review because it delivers verifiable claims on a practical limitation rather than just another language extension.

Referee Report

0 major / 2 minor

Summary. The paper claims that enhancements to the GP 2 compiler's graph data structure enable three rule-based programs to match the time complexity of imperative algorithms: linear-time checks for connectivity and acyclicity on arbitrary (possibly disconnected) graphs with unbounded node degrees, and O(nm) time for single-source shortest paths on arbitrary graphs (matching Bellman-Ford). Formal proofs of correctness and time complexity are provided for each program along with runtime experiments.

Significance. If the stated formal proofs establish the claimed bounds with no hidden asymptotic costs from the enhanced data structure on high-degree or disconnected graphs, the result is significant: it removes prior restrictions on input graphs and shows that rule-based graph transformation languages can achieve optimal imperative complexities for these core problems.

minor comments (2)

The description of the enhanced graph data structure (mentioned in the abstract as key to the complexity results) would benefit from an explicit statement of its space overhead and the precise amortized costs of the operations used in the three programs.
Cross-references between the program listings, the formal proofs, and the experimental setup could be made more explicit to aid verification of the complexity claims.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. No specific major comments are listed in the report.

Circularity Check

0 steps flagged

No significant circularity; claims rest on formal proofs of new programs

full rationale

The paper introduces an enhanced GP 2 graph data structure and three new programs, then states that it formally proves correctness and time complexity for each (linear time for connectivity and acyclicity on arbitrary graphs; O(nm) for shortest paths). No equations reduce a claimed result to its own inputs by construction, no parameters are fitted then renamed as predictions, and no load-bearing uniqueness theorems or ansatzes are imported via self-citation. The derivation chain is self-contained against the stated proofs and the new compiler structure; external benchmarks are not required for the circularity assessment.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on the correctness of the new compiler-generated graph data structure and standard assumptions of graph theory plus GP 2 semantics; no free parameters or invented entities are introduced in the abstract.

axioms (1)

domain assumption GP 2 language semantics and graph representation allow the described compiler enhancement to preserve rule-matching behavior while improving access times.
Invoked implicitly as the foundation for the three programs' claimed complexities.

pith-pipeline@v0.9.0 · 5764 in / 1246 out tokens · 37673 ms · 2026-05-23T05:06:20.433493+00:00 · methodology

Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)