Controlling resource use in graph expression equality proofs
Width-Bounded Equational Derivations for Finite Graph Expressions
Logic in Computer Science
Summary
When checking if two complex graph expressions are the same, it can take a lot of steps and resources. The authors show a way to measure and limit the 'width' or size of intermediate steps during these proofs. This means that for certain types of graph expressions, the process of proving equality can be done efficiently without the resources growing with the graph size. They provide a method that compiles expressions into a standardized form that keeps this width bounded. This work helps better understand and control how complicated graph transformations happen.
finite graph expressionsequational derivationwidth boundednesspattern widthstructural magmoid lawsfinite graphoid schemesderivational spacecanonical formcliquerouting window
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.