# Word equations with integer parameters

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

• For question 2, I think you need to refine where exactly you allow disjunction because otherwise you can easily an encoding of the Post correspondence problem as $(u_1| \dots | u_n)^i = (v_1 | \dots | v_m)^j$ (which is undecidable). Mar 24, 2022 at 21:47
• @Louis this does not exactly correspond to the Post correspondance problem, as using $u_1$ on the left does not force using $v_1$ on the right. In PCP, you are looking for a sequence of indices $i_1,i_2,\dots$ such that $u_{i_1}u_{i_2}\dots=v_{i_1}v_{i_2}\dots$. Here it is clearly decidable whether these two regular languages intersect, i.e. whether there exists a (nonzero) solution for $i,j$. Mar 25, 2022 at 9:40
• True, but I meant that it prevents to have a representation that allows a fast check of $i=j$. Mar 25, 2022 at 11:37
• It's not clear to me that it is undecidable whether there is a solution with $i=j$. You seem to claim it reduces to PCP but I don't see how. Mar 25, 2022 at 12:34
• @Louis Actually, the problem is decidable by reduction to PDA emptiness. You can build a PDA by taking a product of the NFAs $U$ and $V$ computing $(u_1|…|u_n)^*$ and $(v_1|…|v_m)^*$ respectively. The stack alphabet is a,b and the stack keeps track of which side is ahead and by how many iterations. E.g. if $U$ is the first to complete a loop, it pushes "$a$" on the stack to signify that $U$ is ahead by $1$, etc. A stack of $a^n$ (resp. $b^n$) means that $U$ (resp. $V$) is ahead by $n$ words. The PDA accepts when both $U$ and $V$ accept and the stack is empty. Mar 25, 2022 at 12:51

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.

• Thanks, that's a very interesting technique ! Do you have some pointers for a readable description of algorithms to compute the Presburger formula for the Parikh image of a regular automaton (or a regex with shuffle and intersection) ?
– Drup
Mar 30, 2022 at 13:37
• It is given by theorem 1 of [1]: the idea would be to take the NFA for the final language (where Σ has been removed) and quantify over the number of times each transition is taken and add some constraints to make sure a corresponding run exists (this gives a linear size formula). Then you might want to eliminate quantifiers (but if I remember correctly this is expensive). [1] hal.archives-ouvertes.fr/hal-00159525/file/icalp04pres.pdf Mar 30, 2022 at 18:08