Word equations with integer parameters

Question

This is mainly a reference request. Let us define a parameterized expression on a finite alphabet $\Sigma$ as follows:

$$e,e':= w\mid w^i \mid e\cdot e'$$

Where $w\in\Sigma^+$ is a word, and $i$ is an abstract parameter, i.e. an integer variable.

A parameterized equation is an equation $e=e'$, where $e,e'$ are as above, and every integer variable is used at most once overall.

We want an algorithm outputting the set of solutions as a boolean combination of equations on the integer parameters.

Example: $a^i b (ab)^j=(ab)^k$.
Here we expect the algorithm to answer: "$i=1$ and $k=j+1$"

This seems to be done in more general cases, e.g. by [1] which deals with word variables, as most papers I can find when searching for "word equations". But I expect that this simpler case is a lot easier to handle. Unfortunately it is hard to find references, probably because I don't know the correct keywords to search for this. I think I can solve the problem by hand but would like to know relevant references on the subject.

Question 1: Do you know of a source describing a simple algorithm for this problem ?

Question 2: What happens if we allow disjunctions of words under iterations, i.e equations like $(ab+ba+bab)^i=b^j(ab)^k$ ? Is there in the literature an algorithm describing the set of solutions for $i,j,k$ ?

[1] Wojciech Plandowski. 2006. An efficient algorithm for solving word equations. In Proceedings of the thirty-eighth annual ACM symposium on Theory of Computing (STOC '06). Association for Computing Machinery, New York, NY, USA, 467–476. DOI:https://doi.org/10.1145/1132516.1132584

Answer 1

Here we will show that you can get a Presburger formula from an equation.

Let us consider an equation $\alpha = \beta$ over the alphabet $\Sigma$ with the variables $v_\alpha$ in $\alpha$ and $v_\beta$ in $\beta$.

For $\alpha$ we introduce a language $L_\alpha$ over $\Sigma\cup V_\alpha \cup V_\beta$ as follows:

• the $\Sigma$ part will capture words accepted by $\alpha$
• the $V_\alpha$ will be used to output a symbol $v$ each time we use a loop with the variable $v$
• the $V_\beta$ will simply be accepted anywhere in the word.

For instance for $(ab+ba+bab)^i = (ba)^j(ab)^k$ the language $L_\alpha$ will be the interleaving of $(i(ab+ba+bab))*$ (marking a $i$ whenever we enter the starred part) with the language $(j|k)*$.

We can also do the same for $\beta$ and in the example above we have $L_\beta=(j b)*(k ab)*$ interleaved with $i*$.

Now, we can compute $L=L_\alpha \cap L_\beta$, this $L$ captures the solutions of the equation above with also the position where the loops are used. Finally, we can discard the $\Sigma$ part of $L$ and look at the Parikh image, which is a semilinear set that can be represented as a Presburger formula if needed.