New method controls complexity in finite graph expression proofs
Width-Bounded Equational Derivations for Finite Graph Expressions
Logic in Computer Science
Summary
When proving that two expressions representing graphs are equal, it's important to track how complicated the steps between them get. The authors have found a way to measure and limit this complexity by controlling the size of intermediate parts during the proof process. They show that for certain graph expressions, there is always a way to prove equality without the complexity growing uncontrollably, regardless of the overall graph size. This helps keep the proof process more manageable and predictable.
What this means in practice
- •For program verification engineers: Guarantee bounded resource use when transforming finite graph-based program representations during automated proofs of correctness.
- •For compiler developers: Use bounded-width derivations to optimize intermediate representations involving graph structures while controlling complexity in code transformations.
A theory result. No direct application yet.
Authors
Antonios Kalampakas
Abstract
Completeness of an equational presentation guarantees an equality path but need not control the resources used along it. For finite graph expressions we measure derivational space by the largest input-output interface of an intermediate raw term. For every finite doubly ranked edge alphabet $Σ$, we prove that equal closed expressions of pattern width at most $k$ are joined by a derivation in which every step applies an equation in either direction and every intermediate width is at most a computable $B_Σ(k)$, independently of graph size. The derivation uses only the structural magmoid laws and the fifteen finite-graphoid schemes. The construction compiles each expression through protected cores and finite routing windows to an encoding-canonical representative $\operatorname{NF}_k$ of width at most $4k+4$. We call this property bounded equational coherence. We also prove $\operatorname{bw}(F)\le\operatorname{patw}(F)\le4(\operatorname{tw}(F)+1)$ whenever the underlying simple graph has at least two edges, separate layered linear from branching expressions on cliques, and provide machine-checkable witnesses and finite invariants for the first five nontrivial clique values.