<p>Here we will show that you can get a Presburger formula from an equation.</p>
<p>Let us consider an equation <span class="math-container">$\alpha = \beta$</span> over the alphabet <span class="math-container">$\Sigma$</span> with the variables <span class="math-container">$v_\alpha$</span> in <span class="math-container">$\alpha$</span> and <span class="math-container">$v_\beta$</span> in <span class="math-container">$\beta$</span>.</p>
<p>For <span class="math-container">$\alpha$</span> we introduce a language <span class="math-container">$L_\alpha$</span> over <span class="math-container">$\Sigma\cup V_\alpha \cup V_\beta$</span> as follows:</p>
<ul>
<li>the <span class="math-container">$\Sigma$</span> part will capture words accepted by <span class="math-container">$\alpha$</span></li>
<li>the <span class="math-container">$V_\alpha$</span> will be used to output a symbol <span class="math-container">$v$</span> each time we use a loop with the variable <span class="math-container">$v$</span></li>
<li>the <span class="math-container">$V_\beta$</span> will simply be accepted anywhere in the word.</li>
</ul>
<p>For instance for <span class="math-container">$(ab+ba+bab)^i = (ba)^j(ab)^k$</span> the language <span class="math-container">$L_\alpha$</span> will be the interleaving of <span class="math-container">$(i(ab+ba+bab))*$</span> (marking a <span class="math-container">$i$</span> whenever we enter the starred part) with the language <span class="math-container">$(j|k)*$</span>.</p>
<p>We can also do the same for <span class="math-container">$\beta$</span> and in the example above we have <span class="math-container">$L_\beta=(j b)*(k ab)*$</span> interleaved with <span class="math-container">$i*$</span>.</p>
<p>Now, we can compute <span class="math-container">$L=L_\alpha \cap L_\beta$</span>, this <span class="math-container">$L$</span> captures the solutions of the equation above with also the position where the loops are used. Finally, we can discard the <span class="math-container">$\Sigma$</span> part of <span class="math-container">$L$</span> and look at the Parikh image, which is a semilinear set that can be represented as a Presburger formula if needed.</p>

CC BY-SA 4.0
2022-03-30T13:37:28.037Z
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
CC BY-SA 4.0
2022-03-30T18:08:49.583Z
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] https://hal.archives-ouvertes.fr/hal-00159525/file/icalp04pres.pdf
Louis
CC BY-SA 4.0
2022-03-28T18:07:23.407Z
2022-03-28T18:07:23.407Z
Louis
<p>This is mainly a reference request.
Let us define a <em>parameterized expression</em> on a finite alphabet <span class="math-container">$\Sigma$</span> as follows:</p>
<p><span class="math-container">$$e,e':= w\mid w^i \mid e\cdot e'$$</span></p>
<p>Where <span class="math-container">$w\in\Sigma^+$</span> is a word, and <span class="math-container">$i$</span> is an abstract parameter, i.e. an integer variable.</p>
<p>A <em>parameterized equation</em> is an equation <span class="math-container">$e=e'$</span>, where <span class="math-container">$e,e'$</span> are as above, and every integer variable is used at most once overall.</p>
<p>We want an algorithm outputting the set of solutions as a boolean combination of equations on the integer parameters.</p>
<p><strong>Example</strong>: <span class="math-container">$a^i b (ab)^j=(ab)^k$</span>.<br />
Here we expect the algorithm to answer: &quot;<span class="math-container">$i=1$</span> and <span class="math-container">$k=j+1$</span>&quot;</p>
<p>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 &quot;word equations&quot;. 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.</p>
<p><strong>Question 1</strong>: Do you know of a source describing a simple algorithm for this problem ?</p>
<p><strong>Question 2</strong>: What happens if we allow disjunctions of words under iterations, i.e equations like <span class="math-container">$(ab+ba+bab)^i=b^j(ab)^k$</span> ? Is there in the literature an algorithm describing the set of solutions for <span class="math-container">$i,j,k$</span> ?</p>
<p>[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:<a href="https://doi.org/10.1145/1132516.1132584" rel="noreferrer">https://doi.org/10.1145/1132516.1132584</a></p>

CC BY-SA 4.0
2022-03-24T21:47:07.263Z
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).
Louis
CC BY-SA 4.0
2022-03-25T09:40:57.687Z
@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$.
Denis
CC BY-SA 4.0
2022-03-25T11:37:00.523Z
True, but I meant that it prevents to have a representation that allows a fast check of $i=j$.
Louis
CC BY-SA 4.0
2022-03-25T12:34:55.707Z
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.
Denis
CC BY-SA 4.0
2022-03-25T12:51:09.153Z
@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.
Denis
CC BY-SA 4.0
2022-03-25T12:51:27.563Z
Hum, I am sorry I think I confused myself and it is true that you cannot make a PCP encoding. 
Edit: I see that our responses crossed :)
Louis
CC BY-SA 4.0
2022-03-25T12:58:04.873Z
Actually, I think your problem (with disjunctinons) can be encoded as a Parikh automaton where the vectors are used to capture the variables. A parikh automaton captures a semilinear set which would be a tight representation of the set of solution and you can easily test membership or add other constraints.
Louis
CC BY-SA 4.0
2022-03-25T13:08:06.997Z
Parikh automata can be of help, thanks for the pointer. But in a PA aren't you suppose to specify a semilinear set for acceptance ? Do you mean that a PA without semilinear acceptance condition represents the set, and you can do with it all desired operations ? In particular can you extract equations representing this set ?
Denis
CC BY-SA 4.0
2022-03-25T13:15:14.080Z
Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/135043/discussion-between-louis-and-denis).
Louis
<reference-request><fl.formal-languages><regular-expressions>
Word equations with integer parameters
Denis
# Word equations with integer parameters

(Asked by: username_0 on 2022-03-24)

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>

**Tags:** reference-request, fl.formal-languages, regular-expressions

> **Comments:**
> **username_1**: 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).  
> **username_0**: @username_1 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$.  
> **username_1**: True, but I meant that it prevents to have a representation that allows a fast check of $i=j$.  
> **username_0**: 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.  
> **username_0**: @username_1 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.  
> **username_1**: Hum, I am sorry I think I confused myself and it is true that you cannot make a PCP encoding.  Edit: I see that our responses crossed :)  
> **username_1**: Actually, I think your problem (with disjunctinons) can be encoded as a Parikh automaton where the vectors are used to capture the variables. A parikh automaton captures a semilinear set which would be a tight representation of the set of solution and you can easily test membership or add other constraints.  
> **username_0**: Parikh automata can be of help, thanks for the pointer. But in a PA aren't you suppose to specify a semilinear set for acceptance ? Do you mean that a PA without semilinear acceptance condition represents the set, and you can do with it all desired operations ? In particular can you extract equations representing this set ?  
> **username_1**: Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/135043/discussion-between-louis-and-denis).  

---

## 1 answers

### Answer by username_1 on 2022-03-28. Score: 4 | Accepted answer

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.

> **Comments:**
> **username_2**: 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) ?  
> **username_1**: 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] https://hal.archives-ouvertes.fr/hal-00159525/file/icalp04pres.pdf  

---

