1. **Is there an elementary and efficient algorithm for testing the membership to a double coset of f.g. subgroups in a free group?**
2. **Has this membership problem been implemented in GAP/Magma?**


More precisely, I have a finitely generated free group $F$, two finitely generated subgroups $A,B$, given by their free generating sets, and an element $f\in F$. I would like to determine whether $f \in AB$.


I was hoping for something in the spirit of Stallings core graphs, but the standard reference (the paper of Kapovich and Myasnikov [*Kapovich, Ilya; Myasnikov, Alexei*, [**Stallings foldings and subgroups of free groups**](http://dx.doi.org/10.1006/jabr.2001.9033), J. Algebra 248, No. 2, 608-668 (2002). [ZBL1001.20015](https://zbmath.org/?q=an:1001.20015).]) does not seem to treat membership to double cosets.


Theoretically the required algorithm certainly exists. In fact, a much stronger property was proved by Grunschlag ( see Theorem 4.10 in [*Grunschlag, Zeph*, Computing angles in hyperbolic groups, Gilman, Robert H. (ed.), Groups, languages and geometry. 1998 AMS-IMS-SIAM joint summer research conference on geometric group theory and computer science, South Hadley, MA, USA, July 5-9, 1998. Providence, RI: American Mathematical Society. Contemp. Math. 250, 59-88 (1999). [ZBL0953.20034](https://zbmath.org/?q=an:0953.20034).]



Membership to double cosets in free groups
Here is a second answer that is just rephrasing @DerekHolt’s answer based on the comments. So upvote his answer first! Let $X$ be a finite alphabet. An inverse automaton is a finite directed graph labeled over the alphabet $X$ which is folded in the sense of Stallings, meaning you cannot find two edges entering or leaving a vertex with the same label. Equivalently these are immersions over a bouquet of circles. An inverse automaton has a unique initial state and a set of final states. It recognizes a subset of the free group by looking at all reduced words labelling a path from the initial state to a final state, where inverse letters read edges backward. The language accepted by an inverse automaton is a finite union of cosets of finitely generated subgroups.


The languages accepted by inverse automata are closed under intersection. You simply build the product automaton whose vertices are pairs of vertices and there is an edge labeled by $x$ from $(p,q)$ to $(p’,q’)$ if and only if there are edges from $p$ to $p’$ and $q$ to $q’$ labeled by $x$. This construction is the fiber product of the two inverse automata viewed as immersions over a bouquet of circles. The initial state is the pair of initial states and the final states are those pairs $(p,q)$ where both $p$ and $q$ are final in their respective automata. This is an inverse automata that will accept precisely those reduced words which both automata accept. In particular, the intersection is empty iff the initial vertex of the product construction cannot reach any terminal vertex.


Now to recognize $Hw$ write a linear automaton reading the word $w$ (with inverse letters read backward) and attach at the initial point a generating set for $H$ as loops and apply Stallings foldings. The initial vertex is the intial vertex of $w$ and the final vertex is the end point of $w$. These may collapse after folding. This is essentially the Stallings core of $H$ with a thorn labeled $w$ sticking out of the base point and Stallings uses this automaton in his proof of Marshall Hall's Theorem.


We can do a similar thing for $gK$, but we put the generators of $K$ as loops at the end of the path labelled $g$, and then to test if $w\in HgK$ we just form the product automaton for $Hw$ and $gK$ and check if the final state is reachable from the initial state.


Note $w=hgk$ iff $h^{-1}w=gk$. So $Hw$ and $gK$ intersect iff $w\in HgK$.


