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

  • 1
    $\begingroup$ 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). $\endgroup$
    – Louis
    Mar 24 at 21:47
  • $\begingroup$ @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$. $\endgroup$
    – Denis
    Mar 25 at 9:40
  • $\begingroup$ True, but I meant that it prevents to have a representation that allows a fast check of $i=j$. $\endgroup$
    – Louis
    Mar 25 at 11:37
  • $\begingroup$ 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. $\endgroup$
    – Denis
    Mar 25 at 12:34
  • 1
    $\begingroup$ @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. $\endgroup$
    – Denis
    Mar 25 at 12:51

1 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.

  • $\begingroup$ 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) ? $\endgroup$
    – Drup
    Mar 30 at 13:37
  • $\begingroup$ 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 $\endgroup$
    – Louis
    Mar 30 at 18:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.