Word Equations with Length Constraints via Weak Arithmetics and Matrix Reachability Problems

Abstract

The problem of determining whether a word equation admits a solution whose lengths belong to some semilinear set is fundamental to the theory of string-solving. Despite this and connections to Hilbert’s Tenth Problem, its decidability has been open since 1968. We prove this problem decidable for the class of quadratic word equations in at most two unknowns. We use a novel technique recasting the problem as halfspace reachability in the matrix semigroup $SA(n,\{mathbb{N})$. We also look at word equations’ length abstractions: the sets of their solutions’ length-vectors. It is known that these need not be semilinear; with the above problem in mind we seek to understand their expressivity. We show that the length abstractions of quadratic word equations differ finitely from unions of arithmetic progressions. Tools for showing inexpressibility by regular and quadratic word equations result. Each relation definable in existential Presburger arithmetic with divisibility (EPAD) can be built from word equations’ length abstractions. Conversely, the length abstraction of $Xw_1Y=Yw_2X$ is shown EPAD-equidefinable with a certain vector reachability problem.