$\displaystyle=\Big{(}\sum_{n<k}\mathsf{C}_{F^{n},s}(x)\Big{)}+\Big{(}\mathsf{C}_{F^{k},s}(x)\cdot({F^{*}}\triangleright{\varepsilon})\Big{)}$

Notice that the sums are unambiguous since $L=\mathcal{L}(F)$ is a code. The
concatenation $F^{k}\cdot F^{*}$ is also unambiguous.

  * •

$x=(\rightarrow,p,q)\in s$

We turn now to the more interesting left-right steps. Again, if $n<k$ then the
output of $\rho$ is $[\\![\mathsf{C}_{F^{n},s}(x)]\\!](w)$. Assume now that
$n\geq k$. We apply Lemma 5.7 to deduce that the run $\rho$ is $k$-forward-
progressing. See Figure 10 for a sample run which is $2$-forward-progressing.
We split $\rho$ in $\rho_{0}\rho_{1}\cdots\rho_{n-k}$ where $\rho_{0}$ is the
prefix of $\rho$ going until the first crossing from $u_{k}$ to $u_{k+1}$.
Then, $\rho_{1}$ goes until the first crossing from $u_{k+1}$ to $u_{k+2}$.
Continuing in the same way, for $1\leq i<n-k$, $\rho_{i}$ goes until the first
crossing from $u_{k+i}$ to $u_{k+i+1}$. Finally, $\rho_{n-k}$ is the remaining
suffix, going until the run exits from $w$ on the right. Since the run $\rho$
is $k$-forward progressing, we deduce that $\rho_{i}$ does not go back to
$u_{1}\cdots u_{i-1}$, hence it stays inside $u_{i}\cdots u_{i+k}$, starting
on the left of $u_{i+k}$ and exiting on the right of $u_{i+k}$.

Since $X=\varphi(L)$ is $k$-stabilising, we have $\varphi(u_{1}\cdots
u_{k+i})=\varphi(w)$ for all $0\leq i\leq n-k$. Now, $\rho_{0}\cdots\rho_{i}$
is a run on $u_{1}\cdots u_{k+i}$ starting on the left in state $p$ and
exiting on the right. Since $\mathcal{A}$ is deterministic and
$x=(\rightarrow,p,q)\in\varphi(w)=\varphi(u_{1}\cdots u_{k+i})$ we deduce that
$\rho_{i}$ exits on the right of $u_{k+i}$ in state $q$. In particular,
$\rho_{0}$ is a run on $u_{1}\cdots u_{k}$ starting on the left in state $p$
and exiting on the right in state $q$. Moreover, for each $1\leq i\leq n-k$,
$\rho_{i}$ is the concatenation of a zigzag internal run over $(u_{i}\cdots
u_{i+k-1},u_{i+k})$ starting with
$(q,\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})$
ending with
$(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q_{i})=Z_{s^{\prime},s^{\prime\prime}}(q,\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})$
where $s^{\prime}=\varphi(u_{i}\cdots u_{i+k-1})$,
$s^{\prime\prime}=\varphi(u_{i+k})$ and a $(\rightarrow,q_{i},q)$ run over
$u_{i+k}$.

Figure 10: A left-right run which is 2-forward-progressing.

Let $v_{i}$ be the output produced by $\rho_{i}$ for $0\leq i\leq n-k$. Then,
using Lemma 5.16, the productions $v_{i}$ with $0<i\leq n-k$ are given by the
SDRTE $f$ defined as

$\displaystyle
f=\sum_{\begin{subarray}{c}s^{\prime},s^{\prime\prime},q^{\prime}\,\mid\\\
(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q^{\prime})=Z_{s^{\prime},s^{\prime\prime}}(q,\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})\end{subarray}}\mathsf{ZC}_{F^{k},s^{\prime}}^{F,s^{\prime\prime}}(q,\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})\odot\big{(}({\mathcal{L}(F^{k},s^{\prime})}\triangleright{\varepsilon})\cdot\mathsf{C}_{F,s^{\prime\prime}}((\rightarrow,q^{\prime},q))\big{)}$

Then the product $v_{1}\cdots v_{n-k}$ is produced by the $(k+1)$-chained
Kleene-star $[L,f]^{(k+1)\star}(w)$. From the above discussion, we also deduce
that $v_{0}=[\\![\mathsf{C}_{F^{k},s}(x)]\\!](u_{1}\cdots u_{k})$. Therefore,
we define

$\displaystyle\mathsf{C}_{E,s}(x)$
$\displaystyle=\Big{(}\sum_{n<k}\mathsf{C}_{F^{n},s}(x)\Big{)}+\Big{(}\big{(}\mathsf{C}_{F^{k},s}(x)\cdot({F^{*}}\triangleright{\varepsilon})\big{)}\odot[F,f]^{(k+1)\star}\Big{)}$

  * •

$x=(\leftarrow,p,q)\in s$

The case of right-left runs is almost symmetric to the case of left-right
runs. Again, if $n<k$ then the output of $\rho$ is
$[\\![\mathsf{C}_{F^{n},s}(x)]\\!](w)$. Assume now that $n\geq k$. We apply
Lemma 5.9 to deduce that the run $\rho$ is $k$-backward-progressing. As
illustrated in Figure 11, we split $\rho$ in
$\rho_{n-k+1}\cdots\rho_{2}\rho_{1}$ where $\rho_{n-k+1}$ is the prefix of
$\rho$ going until the first crossing from $u_{n-k+1}$ to $u_{n-k}$. Then,
$\rho_{n-k}$ goes until the first crossing from $u_{n-k}$ to $u_{n-k-1}$.
Continuing in the same way, for $n-k>i>1$, $\rho_{i}$ goes until the first
crossing from $u_{i}$ to $u_{i-1}$. Finally, $\rho_{1}$ is the remaining
suffix, going until the run exits from $u_{1}$ on the left. Since the run
$\rho$ is $k$-backward progressing, we deduce that, for $1\leq i\leq n-k$, the
run $\rho_{i}$ does not go back to $u_{i+k+1}\cdots u_{n}$. Hence it is the
concatenation of a zigzag internal run over $(u_{i},u_{i+1}\cdots u_{i+k})$,
starting with some
$(q_{i},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}})$
and exiting with
$(\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q^{\prime}_{i})=Z_{s^{\prime},s^{\prime\prime}}(q_{i},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}})$
where $s^{\prime}=\varphi(u_{i})$, $s^{\prime\prime}=\varphi(u_{i+1}\cdots
u_{i+k})$, and a $(\leftarrow,q^{\prime}_{i},q_{i-1})$-run over $u_{i}$ (see
again Figure 11). Let $v_{i}$ be the output produced by $\rho_{i}$ for $1\leq
i\leq n-k+1$. The output produced by $\rho$ is $v=v_{n-k+1}\cdots v_{2}v_{1}$.
Now, the situation is slightly more complicated than for left-right runs where
we could prove that $q_{i}=q$ for each $i$. Instead, let us remark that
$q_{i}$ is the unique state (by determinacy of $\mathcal{A}$) such that there
is a run over $u_{i+1}\cdots u_{n}$ following step $(\leftarrow,p,q_{i})$. But
since $X$ is $k$-stabilising, we know that $\varphi(u_{i+1}\cdots
u_{n})=\varphi(u_{i+1}\cdots u_{i+k})$. Then, given
$s^{\prime}=\varphi(u_{i})$ and $s^{\prime\prime}=\varphi(u_{i+1}\cdots
u_{i+k})$, we get that $q_{i}$ is the unique state such that
$(\leftarrow,p,q_{i})\in s^{\prime\prime}$ and $q_{i-1}$ the one such that
$(\leftarrow,p,q_{i-1})\in s^{\prime}s^{\prime\prime}$. Thus we define the
function $g$ generating the $v_{i}$ with $1\leq i\leq n-k$ by

$g=\sum_{\begin{subarray}{c}s^{\prime},s^{\prime\prime},p^{\prime},q^{\prime},q^{\prime\prime}\,\mid\,(\leftarrow,p,p^{\prime})\in
s^{\prime\prime},\\\
(\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q^{\prime})=Z_{s^{\prime},s^{\prime\prime}}(p^{\prime},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}}),\,(\leftarrow,q^{\prime},q^{\prime\prime})\in
s^{\prime}\end{subarray}}\mathsf{ZC}_{F,s^{\prime}}^{F^{k},s^{\prime\prime}}(p^{\prime},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}})\odot\Big{(}\mathsf{C}_{F,s^{\prime}}((\leftarrow,q^{\prime},q^{\prime\prime}))\cdot({\mathcal{L}(F^{k},s^{\prime\prime})}\triangleright{\varepsilon})\Big{)}$

Figure 11: A right-left run which is 2-backward-progressing.

Finally, a right-left run for $F^{*}$ is either a right-left run over $F^{n}$
for $n<k$, or the concatenation of a right-left run $\rho_{n-k+1}$ over the
$k$ rightmost iterations of $F$, and a sequence of runs $\rho_{i}$ with $1\leq
i\leq n-k$ as previously and whose outputs are computed by $g$. Therefore, we
define

$\mathsf{C}_{E,s}(x)=\Big{(}\sum_{n<k}\mathsf{C}_{F^{n},s}(x)\Big{)}+\Big{(}\sum_{\begin{subarray}{c}s=s^{\prime}s^{\prime\prime},\,p^{\prime}\,\mid\\\
(\leftarrow,p,p^{\prime})\in
s^{\prime\prime}\end{subarray}}({\mathcal{L}(F^{*},s^{\prime})}\triangleright{\varepsilon})\cdot\mathsf{C}_{F^{k},s^{\prime\prime}}((\leftarrow,p,p^{\prime}))\Big{)}\odot[F,g]_{r}^{(k+1)\star}$

  * •

$x=(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},p,q)\in
s$

We finally deal with right-right runs, thus completing the case of $E=F^{*}$.
If $n<k$, then the output of $\rho$ is $[\\![\mathsf{C}_{F^{n},s}(x)]\\!](w)$.
Assume now that $n\geq k$. If $\rho$ only visits the last $k$ factors, then
$w$ can be decomposed as $uv$ where $u\in\mathcal{L}(F^{*},s^{\prime})$ and
$v\in\mathcal{L}(F^{k},s^{\prime\prime})$ with $s=s^{\prime}s^{\prime\prime}$
and
$(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},p,q)\in
s^{\prime\prime}$. The output of $\rho$ is
$[\\![({\mathcal{L}(F^{*},s^{\prime})}\triangleright{\varepsilon})\cdot\mathsf{C}_{F^{k},s^{\prime\prime}}(x)]\\!](w)$.

Otherwise, by Lemma 5.11, we know that there is a _unique_ integer $1\leq
i\leq n-k$ such that $\rho$ only visits $u_{i}\cdots u_{n}$, and is the
concatenation of 3 runs $\rho_{1},\rho_{2}$ and $\rho_{3}$, where $\rho_{1}$
is a $k$-backward-progressing run over $u_{i+1}\cdots u_{n}$, $\rho_{2}$ is a
zigzag internal run over $(u_{i},u_{i+1}\cdots u_{i+k})$ and $\rho_{3}$ is a
$k$-forward-progressing run over $u_{i+1}\cdots u_{n}$, as depicted in Figure
6.

Let $r=\varphi(u_{1}\cdots u_{i-1})$, $s^{\prime}=\varphi(u_{i})$ and
$s^{\prime\prime}=\varphi(u_{i+1}\cdots u_{i+k})$. Since $i$ is uniquely
determined, the tuple $(r,s^{\prime},s^{\prime\prime})$ is also unique. Notice
that $s^{\prime\prime}=\varphi(u_{i+1}\cdots u_{n})$ since $X$ is
$k$-stabilising and $s^{\prime\prime}\in X^{k}$, hence we have
$s=rs^{\prime}s^{\prime\prime}$. Moreover, the starting and ending states of
$\rho_{2}$ are the _unique_ states $p^{\prime},q^{\prime}$ such that
$(\leftarrow,p,p^{\prime})\in s^{\prime\prime}$,
$Z_{s^{\prime},s^{\prime\prime}}(p^{\prime},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}})=(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q^{\prime})$
and $(\rightarrow,q^{\prime},q)\in s^{\prime\prime}$. Once the tuple
$(r,s^{\prime},s^{\prime\prime},p^{\prime},q^{\prime})$ is fixed, using the
previous points, we have SDRTEs computing the outputs of $\rho_{1}$ and
$\rho_{3}$:

$[\\![\mathsf{C}_{E,s^{\prime\prime}}((\leftarrow,p,p^{\prime}))]\\!](u_{i+1}\cdots
u_{n})\hskip
28.45274pt[\\![\mathsf{C}_{E,s^{\prime\prime}}((\rightarrow,q^{\prime},q))]\\!](u_{i+1}\cdots
u_{n})$

and from Lemma 5.16, the output of $\rho_{2}$ is
$[\\![\mathsf{ZC}_{F,s^{\prime}}^{F^{k},s^{\prime\prime}}(p^{\prime},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}})]\\!](u_{i}u_{i+1}\cdots
u_{i+k})$. This leads to the following SDRTE:

$\displaystyle
h=\sum_{\begin{subarray}{c}r,s^{\prime},s^{\prime\prime},p^{\prime},q^{\prime}\,\mid\\\
s=rs^{\prime}s^{\prime\prime},\,(\leftarrow,p,p^{\prime})\in
s^{\prime\prime}\\\
Z_{s^{\prime},s^{\prime\prime}}(p^{\prime},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}})=(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q^{\prime})\\\
(\rightarrow,q^{\prime},q)\in
s^{\prime\prime}\end{subarray}}({\mathcal{L}(F^{*},r)}\triangleright{\varepsilon})\cdot\Big{(}$
$\displaystyle\big{(}{\mathcal{L}(F,s^{\prime})}\triangleright{\varepsilon}\big{)}\cdot\mathsf{C}_{E,s^{\prime\prime}}((\leftarrow,p,p^{\prime}))$
$\displaystyle\odot\mathsf{ZC}_{F,s^{\prime}}^{F^{k},s^{\prime\prime}}(p^{\prime},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}})\cdot({F^{*}}\triangleright{\varepsilon})$
$\displaystyle\odot({\mathcal{L}(F,s^{\prime})}\triangleright{\varepsilon})\cdot\mathsf{C}_{E,s^{\prime\prime}}((\rightarrow,q^{\prime},q))\Big{)}$

Notice that if $r,s^{\prime},s^{\prime\prime},p^{\prime},q^{\prime}$ satisfy
the conditions of the sum, then there is a unique index $i$ with
$\varphi(u_{i})=s^{\prime}$ and $\varphi(u_{i+1}\cdots
u_{n})=s^{\prime\prime}$: there is a $(\leftarrow,p,p^{\prime})$-run on
$u_{i+1}\cdots u_{n}$ but not on $u_{i}\cdots u_{n}$. Hence all the Cauchy
products in $h$ are unambiguous and uniquely decompose $w$ in $u_{1}\cdots
u_{i-1}$ matched by $\mathcal{L}(F^{*},r)$, $u_{i}$ matched by
$\mathcal{L}(F,s^{\prime})$ and $u_{i+1}\cdots u_{n}$ matched by
$\mathsf{C}_{E,s^{\prime\prime}}((\leftarrow,p,p^{\prime}))$ and
$\mathsf{C}_{E,s^{\prime\prime}}((\rightarrow,q^{\prime},q))$. Also,
$u_{i}u_{i+1}\cdots u_{i+k}$ is matched by
$\mathsf{ZC}_{F,s^{\prime}}^{F^{k},s^{\prime\prime}}(p^{\prime},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}})$
and $n\geq i+k$.

Finally, for the right-right step
$x=(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},p,q)$
we define

$\displaystyle\mathsf{C}_{E,s}(x)=$
$\displaystyle\Big{(}\sum_{n<k}\mathsf{C}_{F^{n},s}(x)\Big{)}+\Big{(}\sum_{s=s^{\prime}s^{\prime\prime}}({\mathcal{L}(F^{*},s^{\prime})}\triangleright{\varepsilon})\cdot\mathsf{C}_{F^{k},s^{\prime\prime}}(x)\Big{)}+h\,.$

The sums above are unambiguous. Indeed, the first case happens exactly when
$w\in F^{n}$ for $n<k$. The second happens exactly when $n\geq k$ and the
right-right run does not visit $u_{n-k}$. Otherwise, the third case happens.

######  Example 5.19.

Let us continue with our example in Figure 2. Here we illustrate computing an
SDRTE for some $E=F^{*}$ and some left-right step. We consider $F=a^{+}b$ so
that $\varphi(F)=Y_{2}$ as computed in Example 3.5, where we also computed
$Z_{2}=Y_{2}^{4}$. Consider $x=(\rightarrow,q_{6},q_{2})\in Z_{2}$. We explain
how to compute $\mathsf{C}_{E,Z_{2}}(x)$. Since $\varphi(F)=Y_{2}$ is
4-stabilising, the runs following step $x$ over words in
$\mathcal{L}(E,Z_{2})=(a^{+}b)^{\geq 4}$ are 4-forward-progressing, and the
construction in the proof above uses a 5-chained star111Actually, the runs
over step $x$ are 3-forward-progressing. Hence, we could simplify the example
below by using a 4-chained star only. But we decided to use a 5-star in order
to follow the construction described in the proof above..

Let $w=u_{1}u_{2}\cdots u_{n}$ with $n\geq 4$ and $u_{1},u_{2},\ldots,u_{n}\in
a^{+}b$. As can be seen on Figure 12 (with $n=8$), the 4-forward-progressing
run $\rho$ over $w$ following step $x=(\rightarrow,q_{6},q_{2})$ splits as
$\rho=\rho_{0}\cdots\rho_{4}$ where $\rho_{0}$ is the prefix from $u_{1}$ till
first crossing from $u_{4}$ to $u_{5}$, $\rho_{1}$ is the part from $u_{5}$
till the first crossing from $u_{5}$ to $u_{6}$, $\rho_{2}$ is the part of the
run from $u_{6}$ till the first crossing from $u_{6}$ to $u_{7}$, $\rho_{3}$
is the part of the run from $u_{7}$ till the first crossing from $u_{7}$ to
$u_{8}$, and $\rho_{4}$ is the part from $u_{8}$ till exiting at the right of
$u_{8}$.

We obtain

$\displaystyle\mathsf{C}_{(a^{+}b)^{*},Z_{2}}((\rightarrow,q_{6},q_{2}))$
$\displaystyle=(\mathsf{C}_{(a^{+}b)^{4},Z_{2}}((\rightarrow,q_{6},q_{2}))\cdot({(a^{+}b)^{*}}\triangleright{\varepsilon}))\odot[a^{+}b,f]^{5\star}$
where $\displaystyle f$
$\displaystyle=\mathsf{ZC}_{(a^{+}b)^{4},Z_{2}}^{a^{+}b,Y_{2}}(q_{2},\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})\odot\Big{(}({a^{+}b)^{4}}\triangleright{\varepsilon})\cdot\mathsf{C}_{a^{+}b,Y_{2}}((\rightarrow,q_{1},q_{2}))\Big{)}$
$\displaystyle\mathsf{ZC}_{(a^{+}b)^{4},Z_{2}}^{a^{+}b,Y_{2}}(q_{2},\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})$
$\displaystyle=\Big{(}({(a^{+}b)^{4}}\triangleright{\varepsilon})\cdot\mathsf{C}_{a^{+}b,Y_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{2},q_{3}))\Big{)}\odot\Big{(}\mathsf{C}_{(a^{+}b)^{4},Z_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q_{3},q_{1}))\cdot({a^{+}b}\triangleright{\varepsilon})\Big{)}$
and the expressions below where computed in Example 5.18
$\displaystyle\mathsf{C}_{a^{+}b,Y_{2}}((\rightarrow,q_{1},q_{2}))$
$\displaystyle={a^{+}b}\triangleright{\varepsilon}$
$\displaystyle\mathsf{C}_{a^{+}b,Y_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{2},q_{3}))$
$\displaystyle=({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})$
$\displaystyle\mathsf{C}_{(a^{+}b)^{4},Z_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q_{3},q_{1}))$
$\displaystyle=({(a^{+}b)^{2}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({a^{+}b}\triangleright{\varepsilon})$
$\displaystyle\mathsf{C}_{(a^{+}b)^{4},Z_{2}}((\rightarrow,q_{6},q_{2}))$
$\displaystyle=\Big{(}({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{2}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\Big{)}\odot{}$
$\displaystyle\qquad\Big{(}({a^{+}b}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{2}}\triangleright{\varepsilon})\Big{)}$

Figure 12: Illustration for Example 5.19

After simplifications, we obtain

$\displaystyle f$
$\displaystyle=\mathsf{ZC}_{(a^{+}b)^{4},Z_{2}}^{a^{+}b,Y_{2}}(q_{2},\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})$
$\displaystyle=\Big{(}({(a^{+}b)^{4}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\Big{)}\odot\Big{(}({(a^{+}b)^{2}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{2}}\triangleright{\varepsilon})\Big{)}\,.$

For instance, consider $w=u_{1}u_{2}\cdots u_{8}$ with $u_{i}=a^{i}b$. Then,

$\displaystyle f(u_{1}\cdots u_{5})$ $\displaystyle=a^{5}ba^{3}b$
$\displaystyle f(u_{2}\cdots u_{6})$ $\displaystyle=a^{6}ba^{4}b$
$\displaystyle f(u_{3}\cdots u_{7})$ $\displaystyle=a^{7}ba^{4}b$
$\displaystyle f(u_{4}\cdots u_{8})$ $\displaystyle=a^{8}ba^{5}b$
$\displaystyle[\\![\mathsf{C}_{(a^{+}b)^{4},Z_{2}}((\rightarrow,q_{6},q_{2}))]\\!](u_{1}\cdots
u_{4})$ $\displaystyle=aba^{4}ba^{2}b$
$\displaystyle[\\![\mathsf{C}_{(a^{+}b)^{*},Z_{2}}((\rightarrow,q_{6},q_{2}))]\\!](u_{1}\cdots
u_{8})$
$\displaystyle=\makebox[28.45274pt][l]{$aba^{4}ba^{2}ba^{5}ba^{3}ba^{6}ba^{4}ba^{7}ba^{4}ba^{8}ba^{5}b$\,.}$

We conclude the section by showing how to construct SDRTEs equivalent to
2DFTs.

######  Theorem 5.20.

Let $\mathcal{A}=(Q,\Sigma,\Gamma,\delta,\gamma,q_{0},F)$ be an aperiodic
2DFT. We can construct an equivalent SDRTE $C_{\mathcal{A}}$ over alphabet
$\Sigma$ with
$\mathsf{dom}([\\![C_{\mathcal{A}}]\\!])=\mathsf{dom}([\\![\mathcal{A}]\\!])$
and $[\\![\mathcal{A}]\\!](w)=[\\![C_{\mathcal{A}}]\\!](w)$ for all
$w\in\mathsf{dom}([\\![\mathcal{A}]\\!])$.

######  Proof 5.21.

We first construct below an SDRTE $C^{\prime}_{\mathcal{A}}$ with
$\mathsf{dom}([\\![C^{\prime}_{\mathcal{A}}]\\!])={\vdash}\mathsf{dom}([\\![\mathcal{A}]\\!]){\dashv}$
and such that
$[\\![\mathcal{A}]\\!](w)=[\\![C^{\prime}_{\mathcal{A}}]\\!]({\vdash}w{\dashv})$
for all $w\in\mathsf{dom}([\\![\mathcal{A}]\\!])$. Then, we obtain
$C^{\prime\prime}_{\mathcal{A}}$ using Proposition 4.3 by

$C^{\prime\prime}_{A}={({{\vdash}}^{-1}{C^{\prime}_{\mathcal{A}}})}{{\dashv}}^{-1}\,.$

Finally, we get rid of lingering endmarkers in
$C^{\prime\prime}_{\mathcal{A}}$ using Lemma 4.5 to obtain $C_{\mathcal{A}}$
as the projection of $C^{\prime\prime}_{\mathcal{A}}$ on $\Sigma^{*}$.

Let $\varphi\colon(\Sigma\uplus\\{{\vdash},{\dashv}\\})^{*}\to\mathsf{TrM}$ be
the canonical surjective morphism to the transition monoid of $\mathcal{A}$.
Since $\mathcal{A}$ is aperiodic, the monoid $\mathsf{TrM}$ is also aperiodic.
We can apply Theorem 3.6 to the restriction of $\varphi$ to $\Sigma^{*}$: for
each $s\in\mathsf{TrM}$, we get an unambiguous, stabilising, SD-regular
expression $E_{s}$ with $\mathcal{L}(E_{s})=\varphi^{-1}(s)\cap\Sigma^{*}$.
Let $E={\vdash}\cdot(\bigcup_{s\in\mathsf{TrM}}E_{s})$ which is an
unambiguous, stabilising, SD-regular expression with
$\mathcal{L}(E)={\vdash}\Sigma^{*}$. Applying Theorem 5.14, for each monoid
element $s\in\mathsf{TrM}$ and each step
$x\in\\{\rightarrow,\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},\leftarrow\\}\times
Q^{2}$, we construct the corresponding SDRTE $\mathsf{C}_{E,s}(x)$. We also
apply Lemma 5.16 and construct for each state $p\in Q$ an SDRTE
$\mathsf{ZC}_{E,s}^{{\dashv},t}(p,\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})$
where $t=\varphi({\dashv})$.

Figure 13: Removing end markers. On the left when there is a non trivial zig
zag until reaching a final state $q$; on the right when we have an empty
zigzag. $q_{0}$ is the initial state and $q\in F$.

Finally, we define

$C^{\prime}_{\mathcal{A}}=\sum_{\begin{subarray}{c}s,p,q\mid q\in F\\\
(\rightarrow,q_{0},p)\in s\\\
Z_{s,t}(p,\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})=(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q)\end{subarray}}\big{(}\mathsf{C}_{E,s}((\rightarrow,q_{0},p))\cdot({{\dashv}}\triangleright{\varepsilon})\big{)}\odot\mathsf{ZC}_{E,s}^{{\dashv},t}(p,\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})$

See alo Figure 13 illustrating $C^{\prime}_{\mathcal{A}}$. We can easily check
that $C^{\prime}_{\mathcal{A}}$ satisfies the requirements stated above.

######  Example 5.22.

We complete the series of examples by giving an SDRTE equivalent with the
transducer $\mathcal{A}$ of Figure 2 on words in $E_{1}=b(a^{+}b)^{\geq
4}\subseteq\mathsf{dom}(\mathcal{A})$. Notice that by Example 3.5, we have
$\varphi(E_{1})=Z_{1}=Y_{1}Z_{2}$. We compute first
$\mathsf{C}_{E_{1},Z_{1}}((\rightarrow,s,q_{2}))$. We use the unambiguous
product $E_{1}=b\cdot E_{2}$ with $E_{2}=(a^{+}b)^{\geq 4}$. From Example 3.5,
we have
$(\rightarrow,s,q_{0}),(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q_{5},q_{6})\in
Y_{1}=\varphi(b)$ and
$(\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{0},q_{5}),(\rightarrow,q_{6},q_{2})\in
Z_{2}=\varphi(E_{2})$. We deduce that in the product, the zigzag part consists
of the two steps
$(\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{0},q_{5})$
and
$(\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q_{5},q_{6})$.
Therefore we obtain:

$\displaystyle\mathsf{C}_{E_{1},Z_{1}}((\rightarrow,s,q_{2}))$
$\displaystyle=\big{(}\mathsf{C}_{b,Y_{1}}((\rightarrow,s,q_{0}))\cdot({E_{2}}\triangleright{\varepsilon})\big{)}\odot\mathsf{ZC}_{b,Y_{1}}^{E_{2},Z_{2}}(q_{0},\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})\odot\big{(}({b}\triangleright{\varepsilon})\cdot\mathsf{C}_{E_{2},Z_{2}}((\rightarrow,q_{6},q_{2}))\big{)}$
$\displaystyle\mathsf{ZC}_{b,Y_{1}}^{E_{2},Z_{2}}(q_{0},\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})$
$\displaystyle=\big{(}({b}\triangleright{\varepsilon})\cdot\mathsf{C}_{E_{2},Z_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{0},q_{5}))\big{)}\odot\big{(}\mathsf{C}_{b,Y_{1}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q_{5},q_{6}))\cdot({E_{2}}\triangleright{\varepsilon})\big{)}\,.$

Since
$\mathsf{C}_{b,Y_{1}}((\rightarrow,s,q_{0}))=\mathsf{C}_{b,Y_{1}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{90.0}{$\curvearrowleft$}}},q_{5},q_{6}))={b}\triangleright{\varepsilon}$,
we obtain after simplifications

$\displaystyle\mathsf{C}_{E_{1},Z_{1}}((\rightarrow,s,q_{2}))$
$\displaystyle=\big{(}({b}\triangleright{\varepsilon})\cdot\mathsf{C}_{E_{2},Z_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{0},q_{5}))\big{)}\odot\big{(}({b}\triangleright{\varepsilon})\cdot\mathsf{C}_{E_{2},Z_{2}}((\rightarrow,q_{6},q_{2}))\big{)}\,.$

Let $E=(a^{+}b)^{*}$ as in Example 5.19. Since
$\mathcal{L}(E_{2},Z_{2})=\mathcal{L}(E,Z_{2})$ we have
$\mathsf{C}_{E_{2},Z_{2}}(x)=\mathsf{C}_{E,Z_{2}}(x)$ for all steps $x$.
Recall that in Example 5.19 we have computed
$\mathsf{C}_{E,Z_{2}}((\rightarrow,q_{6},q_{2}))$. Moreover,
$\mathsf{C}_{E_{2},Z_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{0},q_{5}))=\mathsf{C}_{(a^{+}b)^{4},Z_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{0},q_{5}))\cdot({E}\triangleright{\varepsilon})$
and a computation similar to Example 5.18 gives

$\displaystyle\mathsf{C}_{(a^{+}b)^{4},Z_{2}}((\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}},q_{0},q_{5}))$
$\displaystyle=({(a^{+}b)^{2}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({a^{+}b}\triangleright{\varepsilon})\,.$

Finally, with the notations of Example 5.19, we obtain

$\displaystyle\mathsf{C}_{E_{1},Z_{1}}((\rightarrow,s,q_{2}))={}\phantom{\odot}$
$\displaystyle\big{(}({b(a^{+}b)^{2}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{+}}\triangleright{\varepsilon})\big{)}$
$\displaystyle{}\odot{}$
$\displaystyle\big{(}({b}\triangleright{\varepsilon})\cdot\mathsf{C}_{E,Z_{2}}((\rightarrow,q_{6},q_{2}))\big{)}$
$\displaystyle={}\phantom{\odot}$
$\displaystyle\big{(}({b(a^{+}b)^{2}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{+}}\triangleright{\varepsilon})\big{)}$
$\displaystyle{}\odot{}$
$\displaystyle\big{(}({b}\triangleright{\varepsilon})\cdot\mathsf{C}_{(a^{+}b)^{4},Z_{2}}((\rightarrow,q_{6},q_{2}))\cdot({(a^{+}b)^{*}}\triangleright{\varepsilon})\big{)}$
$\displaystyle{}\odot{}$
$\displaystyle\big{(}({b}\triangleright{\varepsilon})\cdot[a^{+}b,f]^{5\star}\big{)}$
$\displaystyle={}\phantom{\odot}$
$\displaystyle\big{(}({b(a^{+}b)^{2}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{+}}\triangleright{\varepsilon})\big{)}$
$\displaystyle{}\odot{}$
$\displaystyle\big{(}({b}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{2}}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{*}}\triangleright{\varepsilon})\big{)}$
$\displaystyle{}\odot{}$
$\displaystyle\big{(}({ba^{+}b}\triangleright{\varepsilon})\cdot({a}\triangleright{a})^{+}\cdot({b}\triangleright{b})\cdot({(a^{+}b)^{\geq
2}}\triangleright{\varepsilon})\big{)}$ $\displaystyle{}\odot{}$
$\displaystyle\big{(}({b}\triangleright{\varepsilon})\cdot[a^{+}b,f]^{5\star}\big{)}\,.$

Note that for our example, we have a simple case of using Theorem 5.20, since
${\vdash}$ is visited only once at state $s$, and there are no transitions
defined on ${\dashv}$, i.e., $\varphi({\dashv})=\emptyset$. So for
$E^{\prime}={\vdash}E_{1}$, we have
$(\rightarrow,s,q_{2})\in\varphi(E^{\prime})$ and
$\mathsf{ZC}_{E^{\prime},\varphi(E^{\prime})}^{{\dashv},\emptyset}(q_{2},\mathrel{\leavevmode{\rotatebox[origin={c}]{-90.0}{$\curvearrowright$}}})=\varepsilon$
(zigzag part empty as seen in the right of Figure 13). Thus, an expression
equivalent to $\mathcal{A}$ on words in $E_{1}$ effectively boils down to
$\mathsf{C}_{E_{1},Z_{1}}((\rightarrow,s,q_{2}))$. For the sake of simplicity,
we stop the example here and do not provide the expression on the full domain
$\mathsf{dom}(\mathcal{A})=b(a^{*}b)^{\geq 2}a^{*}$. ∎

##  6 Adding composition

Since SDRTEs are used to define functions over words, it seems natural to
consider the composition of functions, as it is an easy to understand but
powerful operator. In this section, we discuss other formalisms using
composition as a basic operator, and having the same expressive power as
SDRTEs.

Theorem 1.1 gives the equivalence between SDRTEs and aperiodic two-way
transducers, the latter being known to be closed under composition. Hence,
adding composition to SDRTEs does not add expressiveness, while allowing for
easier modelisation of transformations.

Moreover, we prove that, should we add composition of functions, then we can
replace the $k$-chained star operator and its reverse by the simpler $1$-star
$[L,f]^{1\star}$ and its reverse, which in particular are one-way (left-to-
right or right-to-left) operator when $f$ is also one-way.

Finally, we prove that we can furthermore get rid of the reverse operators as
well as the Hadamard product by adding two basic functions: _reverse_ and
_duplicate_. The reverse function is straightforward as it reverses its input.
The duplicate function is parameterised by a symbol, say $\\#$, duplicates its
input inserting $\\#$ between the two copies: $\mathsf{dup}_{\\#}(u)=u\\#u$.

######  Theorem 6.1.

The following families of expressions have the same expressive power:

  1. 1.

SDRTEs,

  2. 2.

SDRTEs with composition of functions,

  3. 3.

SDRTEs with composition and chained star restricted to $1$.

  4. 4.

Expressions with simple functions, unambiguous sum, Cauchy product, $1$-star,
duplicate, reverse and composition.

######  Proof 6.2.

It is trivial that $\ref{thm-wC-1c}\subseteq\ref{thm-wC-SDRTEc}$ as 3 is
obtained as a syntaxical restriction of 2. Although it is not needed in our
proof, note that $\ref{thm-wC-SDRTE}\subseteq\ref{thm-wC-SDRTEc}$ holds for
the same reason. Now, thanks to Theorem 1.1, we know that SDRTEs are
equivalent to aperiodic two-way transducers that are closed under composition.
Hence, composition does not add expressive power and we have $\ref{thm-wC-
SDRTEc}\subseteq\ref{thm-wC-SDRTE}$.

To prove that $\ref{thm-wc-BasicFun}\subseteq\ref{thm-wC-1c}$, we simply have
to prove that the duplicate and reverse functions can be expressed with SDRTEs
using only the $1$-star operator and its reverse. The duplicate function
definition relies on the Hadamard and is given by the expression:

$\mathsf{dup}_{\\#}=(\mathsf{id}_{\Sigma^{*}}\cdot({\varepsilon}\triangleright{\\#}))\odot\mathsf{id}_{\Sigma^{*}}$

where $\mathsf{id}_{\Sigma^{*}}$ is the identity function and can be written
as $[\Sigma,\mathsf{id}_{\Sigma}]^{1\star}$ where
$\mathsf{id}_{\Sigma}=\sum_{a\in\Sigma}{a}\triangleright{a}$. The reverse
function is also easy to define using the $1$-star reverse:

$\mathsf{rev}=[\Sigma,\mathsf{id}_{\Sigma}]_{r}^{1\star}$

To prove the last inclusion $\ref{thm-wC-SDRTE}\subseteq\ref{thm-wc-
BasicFun}$, we need to express the Hadamard product and the (reverse)
$k$-chained star, using duplicate, reverse and composition.

The Hadamard product $f\odot g$ is easy to define using $\mathsf{dup}_{\\#}$
where $\\#$ is a fresh marker:

$f\odot g=(f\cdot({\\#}\triangleright{\varepsilon})\cdot
g)\circ\mathsf{dup}_{\\#}\,.$

We show now how to reduce $k$-star to $1$-star using duplicate and
composition. The proof is by induction on $k$. When $k=1$ there is nothing to
do. Assume that $k>1$. We show how to express $[L,f]^{k\star}$ using
$(k-1)$-star, $1$-star and duplicate. The main idea is to use composition to
mark each factor in $L$ in order to duplicate them, then use a $(k-1)$-star to
have a reach of $k$ factors of $L$ (with some redundant information), and
lastly use composition to prune the input to a form suitable to finally apply
$f$.

More formally, let $\\#$ and $\$$ be two fresh markers and define

$f_{1}=[L,\mathsf{dup}_{\$}\cdot({\varepsilon}\triangleright{\\#})]^{1\star}$

with domain $L^{*}$ and, when applied to a word $u=u_{1}\cdots u_{n}$ with
$u_{i}\in L$, produces $u_{1}\$u_{1}\\#u_{2}\$u_{2}\\#u_{3}\$u_{3}\\#\cdots
u_{n-1}\$u_{n-1}\\#u_{n}\$u_{n}\\#\in\\{\varepsilon\\}\cup\Sigma^{*}\$(\Sigma^{*}\\#\Sigma^{*}\$)^{*}\Sigma^{*}\\#$.
Notice that $\Sigma^{*}\\#\Sigma^{*}\$$ is a $1$-SD prefix code and that
taking $k-1$ consecutive factors from this language allows us to have a reach
of $k$ factors of $L$. Then we define the function $g$

$g=\big{(}\mathsf{id}_{\Sigma^{*}}\cdot({\\#\Sigma^{*}\$}\triangleright{\varepsilon})\big{)}^{k-2}\cdot\big{(}\mathsf{id}_{\Sigma^{*}}\cdot({\\#}\triangleright{\varepsilon})\cdot\mathsf{id}_{\Sigma^{*}}\cdot({\$}\triangleright{\varepsilon})\big{)}$

with domain $(\Sigma^{*}\\#\Sigma^{*}\$)^{k-1}$ and, when applied to a word
$v_{1}\\#v^{\prime}_{1}\$v_{2}\\#v^{\prime}_{2}\$\cdots
v_{k-1}\\#v^{\prime}_{k-1}\$$, produces $v_{1}v_{2}\cdots
v_{k-1}v^{\prime}_{k-1}$. In particular,
$g(u_{i+1}\\#u_{i+2}\$u_{i+2}\\#u_{i+3}\$\cdots
u_{i+k-1}\\#u_{i+k}\$)=u_{i+1}\cdots u_{i+k}$. Finally, we have

$[L,f]^{k\star}=\big{(}({\varepsilon}\triangleright{\varepsilon})+({\Sigma^{*}\$}\triangleright{\varepsilon})\cdot[\Sigma^{*}\\#\Sigma^{*}\$,f\circ
g]^{(k-1)\star}\cdot({\Sigma^{*}\\#}\triangleright{\varepsilon})\big{)}\circ
f_{1}\,.$

The reverse $k$-star $[L,f]_{r}^{k\star}$ is not expressed in a
straightforward fashion using reverse composed with $k$-star, because while
reverse applies on all the input, the reverse $k$-star swaps the applications
of function $f$ while keeping the function $f$ itself untouched. In order to
express it, we reverse a $k$-star operator not on $f$, but on $f$ reversed.
The result is that the applications of $f$ are reversed twice, thus preserving
them. Formally, we have:

$[L,f]_{r}^{k\star}=\mathsf{rev}\circ[L,\mathsf{rev}\circ f]^{k\star}$

##  7 Conclusion

We conclude with some interesting avenues for future work, arising from the
open questions based on this paper.

We begin with complexity questions, and then move on to other directions for
future work. The complexity of our procedure, especially when going from the
declarative language SDRTE to the computing machine 2DFT, is open. This part
relies heavily on the composition of 2DFTs which incurs at least one
exponential blowup in the state space. A possibility to reduce the complexity
incurred during composition, is to obtain _reversible_ 2FT (2RFT) for each of
the intermediate functions used in the composition. 2RFTs are a class of 2DFTs
which are both deterministic and co-deterministic, and were introduced in
[10], where they prove that composition of 2RFTs results in a 2RFT with
polynomially many states in the number of states of the input transducers.
Provided that the composition of 2RFTs preserves aperiodicity, if we could
produce 2RFTs in our procedures in section 5.1, then we would construct a 2RFT
which is polynomial in the size of the SDRTE. Another open question is the
efficiency of evaluation, i.e., given an SDRTE and an input word, what is the
time complexity of obtaining the corresponding output. This is crucial for an
implementation, along the lines of DReX [2].

Yet another direction is to extend our result to transformations over infinite
words. While Perrin [19] generalized the SF=AP result of Schützenberger to
infinite words in the mid 1980s, Diekert and Kufleitner [12, 13] generalized
Schützenberger’s SD=AP result to infinite words. One could use this SD=AP over
infinite words and check how to adapt our proof to the setting of
transformations over infinite words. Finally, a long standing open problem in
the theory of transformations is to decide if a function given by a 2DFT is
realizable by an aperiodic one. This question has been solved in the one-way
case, or in the case when we have _origin_ information [5], but the general
case remains open. We believe that our characterisation of stabilising runs
provided in Section 5.2.1 could lead to a forbidden pattern criteria to decide
this question.

## References

  * [1] Rajeev Alur and Pavol Černý.  Expressiveness of streaming string transducers.  In 30th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, volume 8 of LIPIcs. Leibniz Int. Proc. Inform., pages 1–12. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2010.
  * [2] Rajeev Alur, Loris D’Antoni, and Mukund Raghothaman.  Drex: A declarative language for efficiently evaluating regular string transformations.  In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 125–137, 2015.  doi:10.1145/2676726.2676981.
  * [3] Rajeev Alur, Adam Freilich, and Mukund Raghothaman.  Regular combinators for string transformations.  In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, pages 9:1–9:10. ACM, 2014\.
  * [4] Nicolas Baudru and Pierre-Alain Reynier.  From two-way transducers to regular function expressions.  In Mizuho Hoshi and Shinnosuke Seki, editors, 22nd International Conference on Developments in Language Theory, DLT 2018, volume 11088 of Lecture Notes in Computer Science, pages 96–108. Springer, 2018.
  * [5] Mikolaj Bojanczyk.  Transducers with origin information.  In Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, pages 26–37, 2014.  doi:10.1007/978-3-662-43951-7\\_3.
  * [6] Mikolaj Bojanczyk, Laure Daviaud, and Shankara Narayanan Krishna.  Regular and first-order list functions.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 125–134, 2018.  doi:10.1145/3209108.3209163.
  * [7] J. Richard Büchi.  Weak second-order arithmetic and finite automata.  Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 6:66–92, 1960.
  * [8] Olivier Carton and Luc Dartois.  Aperiodic two-way transducers and fo-transductions.  In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 160–174. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.  doi:10.4230/LIPIcs.CSL.2015.160.
  * [9] Bruno Courcelle.  Monadic second-order definable graph transductions: a survey [see MR1251992 (94f:68009)].  Theoret. Comput. Sci., 126(1):53–75, 1994.  Seventeenth Colloquium on Trees in Algebra and Programming (CAAP ’92) and European Symposium on Programming (ESOP) (Rennes, 1992).  URL: http://dx.doi.org/10.1016/0304-3975(94)90268-2, doi:10.1016/0304-3975(94)90268-2.
  * [10] Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote.  On reversible transducers.  In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 113:1–113:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.  doi:10.4230/LIPIcs.ICALP.2017.113.
  * [11] Vrunda Dave, Paul Gastin, and Shankara Narayanan Krishna.  Regular Transducer Expressions for Regular Transformations.  In Martin Hofmann, Anuj Dawar, and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic In Computer Science (LICS’18), pages 315–324, Oxford, UK, July 2018\. ACM Press.
  * [12] Volker Diekert and Manfred Kufleitner.  Bounded synchronization delay in omega-rational expressions.  In Computer Science - Theory and Applications - 7th International Computer Science Symposium in Russia, CSR 2012, Nizhny Novgorod, Russia, July 3-7, 2012. Proceedings, pages 89–98, 2012.  doi:10.1007/978-3-642-30642-6\\_10.
  * [13] Volker Diekert and Manfred Kufleitner.  Omega-rational expressions with bounded synchronization delay.  Theory of Computing Systems, 56(4):686–696, 2015.
  * [14] Volker Diekert and Manfred Kufleitner.  A survey on the local divisor technique.  Theoretical Computer Science, 610:13–23, Jan 2016.
  * [15] Joost Engelfriet and Hendrik Jan Hoogeboom.  MSO definable string transductions and two-way finite-state transducers.  ACM Trans. Comput. Log., 2(2):216–254, 2001.  URL: http://dx.doi.org/10.1145/371316.371512, doi:10.1145/371316.371512.
  * [16] Emmanuel Filiot, Shankara Narayanan Krishna, and Ashutosh Trivedi.  First-order definable string transformations.  In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs, pages 147–159. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014.  URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.147, doi:10.4230/LIPIcs.FSTTCS.2014.147.
  * [17] Paul Gastin.  Modular descriptions of regular functions.  In Algebraic Informatics - 8th International Conference, CAI 2019, Niš, Serbia, June 30 - July 4, 2019, Proceedings, pages 3–9, 2019\.  doi:10.1007/978-3-030-21363-3\\_1.
  * [18] Robert McNaughton and Seymour Papert.  Counter-Free Automata.  The MIT Press, Cambridge, Mass., 1971.
  * [19] Dominique Perrin.  Recent results on automata and infinite words.  In Mathematical Foundations of Computer Science 1984, Praha, Czechoslovakia, September 3-7, 1984, Proceedings, pages 134–148, 1984.  doi:10.1007/BFb0030294.
  * [20] Dominique Perrin and Jean-Eric Pin.  Infinite Words: Automata, Semigroups, Logic and Games, volume 141\.  Elsevier, 2004.
  * [21] Marcel Paul Schützenberger.  On finite monoids having only trivial subgroups.  Information and Control, 8(2):190–194, 1965.
  * [22] Marcel-Paul Schützenberger.  Sur certaines opérations de fermeture dans les langages rationnels.  In Symposia Mathematica, Vol. XV (Convegno di Informatica Teorica, INDAM, Roma, 1973), pages 245–253. Academic Press, 1975.