Combining Word Equations, Regular Languages and Arithmetic

The term 'word equations' refers to equations in discrete, typically non-commutative, algebraic structures such as monoids and groups, whose elements may be represented as finite sequences (called words) of symbols from some fixed set A. I will focus on finitely generated free monoids A*: a word equation is then an equation where each side is a concatenation of variables and symbols from A, and solutions are any substitutions of the variables for words in A* resulting in both sides becoming identical. For example, the substitution X -> bab is a solution to the equation Xab = baX where X is a variable and a,b are letters from A.

Some of the early interest in word equations centred around a hope that they might help resolve Hilbert’s 10th problem in the negative by providing a link between computations of Turing machines and Diophantine equations. While this endeavour ultimately failed when Makanin famously discovered a general algorithm for solving word equations in 1977, it lead to a series of breakthroughs in solving equations in various algebraic structures and played a role in the proofs of two fundamental conjectures of Tarski from the 1940s.

Over 40 years on from Makanin’s discovery, substantial interest in word equations has arisen in the field of software analysis and verification. Many modern software programs rely heavily on the manipulation of the string datatype which is naturally modelled by words in a free monoid. A plethora of automated tools have been developed for analysing these string-manipulating programs which have at their core the (often limited) ability to reason about word equations in combination with other typical kinds of properties of strings such as regular language membership and length-comparisons.

Despite much progress in the intervening decades, working with word equations with additional constraints remains a major challenge, exacerbated by a still rather limited understanding of their solution-sets. I aim to discuss some recent results, important open problems and the appropriate context relevant to solving word equations with additional constraints, focusing in particular on the combination of word equations, regular language membership, and (linear) arithmetic over lengths.