We study the separability problem for automatic relations (i.e., relations on finite words definable by synchronous automata) in terms of
recognizable relations (i.e., finite unions of products of regular languages). This problem takes as input two automatic relations
$R$ and $R'$, and asks if there exists a recognizable relation $S$ that contains $R$ and does not intersect $R'$. We show this problem to
be undecidable when the number of products allowed in the recognizable relation is fixed. In particular, checking if there exists
a recognizable relation $S$ with at most $k$ products of regular languages that separates $R$ from $R'$ is undecidable, for each fixed $k \geq 2$.

-.4ex  This pdf contains internal links: clicking on a "notion@@notice" leads to its ""definition@@notice"".[This result was achieved by using the "knowledge" package and its companion tool "knowledge-clustering".]

§ INTRODUCTION

The study of classes of relations on words has become an important topic in language theory
<cit.>, and also in areas such as databases and verification where they are used to
build expressive languages. For instance, classes of relations of this kind are relevant for querying strings over relational
databases <cit.>, comparing paths in graph databases <cit.>, or defining
string constraints for model checking <cit.>.
The most studied such classes include recognizable, automatic, and rational relations, each one of the latter two
strictly extending
the previous one.
""Rational relations"" are those definable by multi-head automata, with heads possibly moving asynchronously;
"automatic relations" are "rational relations" that are accepted by multi-head automata whose heads are forced to move synchronously; and
"recognizable relations" correspond to finite unions of products of regular languages (or, equivalently, to languages recognized via finite monoids, by Mezei's Theorem). By definition, all of these classes coincide with the
class of regular languages when restricted to unary relations.

Prior work has focused on the ""$\REC$-definability problem"",
which takes as input an $n$-ary "rational relation" $R$ and asks
whether it is equivalent to a "recognizable relation"
$\bigcup_i L_{i,1} \times \cdots \times L_{i,n}$, where each $L_{i,j}$ is a regular language.
Intuitively, the problem asks whether the different components of
the "rational relation" $R$ are almost independent of one another.
The study of "$\REC$-definability"
is relevant since relations enjoying this property are often amenable to some analysis including, e.g.,
abstract interpretations in program verification, variable elimination in constraint logic programming, and
query processing over constraint databases (see the introduction of <cit.> for a thorough discussion on this topic).

In general, "$\REC$-definability" of "rational relations" is undecidable, but it becomes decidable for two important subclasses:
deterministic "rational relations" and "automatic relations".
For deterministic "rational relations",  "$\REC$-definability" has been shown to be decidable in double-exponential time for binary relations by Valiant <cit.>—improving Stearns's triple-exponential bound <cit.>. The decidability result was later extended to relations of arbitrary arity by Carton, Choffrut and Grigorieff <cit.>.

For "automatic relations", the decidability of "$\REC$-definability"
can be obtained by a  simple reduction to the problem of checking whether a finite automaton recognizes an infinite language <cit.> – which is decidable via a standard reachability argument.
The precise complexity of the problem, however, was only recently pinned down. By applying
techniques based on Ramsey Theorem over infinite graphs, it was shown that "$\REC$-definability" of "automatic relations" is
"PSpace"-complete when
relations are specified by non-deterministic automata <cit.> <cit.>.

On the other hand, much less is known about the ""$\REC$-separability problem"", which takes two $n$-ary "rational relations"
$R,R' \subseteq \A^* \times \A^*$ and checks whether there is a "recognizable relation"
$S = \bigcup_i L_{i,1} \times \cdots \times L_{i,n}$
with $R \subseteq S$ and $R' \cap S = \emptyset$. In other words, this problem asks whether we can overapproximate $R$ with a recognizable
relation $S$ that is constrained not to intersect with $R'$. Separability problems of this kind abound in theoretical computer science, in particular
in formal language theory where they have gained a lot of attention over the last few years —see, e.g., <cit.>.

The following paragraph is not very clear.
As for definability, the "$\REC$-separability problem" for "rational relations"
is in general undecidable.
In this paper we focus on the separability problem for "automatic relations", that is, the restriction of the "$\REC$-separability
problem" defined above to the case when both $R$ and $R'$ are "automatic relations".
Notice that when $R'$ is the complement of $R$ this problem boils down to "$\REC$-definability".
However, "$\REC$-separability" for "automatic relations" is more general than "$\REC$-definability", and to this day it is unknown whether
it is decidable.

Main contributions and technical approach.

While we do not solve the separability problem for "automatic relations",
we report on some significant progress in our understanding of the problem.
We start by establishing a tight connection between "$\REC$-separability" and the colorability problem
for “"automatic graphs"”, which may shed some light on the difficulty of the former problem.
An "automatic graph" <cit.>I don't understand these citations, what are they doing here? is an infinite graph defined on the set of all finite words, whose edge set is described by a binary "automatic relation". The "regular colorability problem" is then checking if the "automatic graph" defined by a binary automatic relation is finitely colorable, with the restriction that each color is a regular language.
Concretely, we show that the "$\REC$-separability problem" for binary "automatic relations" is equivalent, under polynomial time reductions, to the "regular colorability problem".
Moreover, we introduce a hierarchy $(\kREC)_{k > 0}$ of "recognizable relations"
so that the coloring problem, when restricted to $k>0$ colors—called "$k$-regular colorability problem"— reduces to the separability problem by relations of $\kREC$. Concretely:

There are polynomial-time reductions:

* from the "$\REC$-separability problem" to the "regular colorability problem";

* from the "regular colorability problem" to the "$\REC$-separability problem"; and

* from the "$k$-regular colorability problem" to the $\kREC$-"separability problem", for every $k > 0$.

Further, the last two reductions are so that the second relation in the instance of the "separability problem" is the identity $\Id$.

The "regular colorability problem" seems challenging, and in particular we lack tools for establishing that an "automatic graph" is finitely colorable; let alone checking that said colors define regular sets.

On the other hand, it is easy to see that the "$k$-regular colorability problem"
is undecidable for each fixed $k > 1$ if we lift the restriction that colors define regular sets, i.e.,
checking if an "automatic graph" admits a $k$-coloring—this has been proved in an unpublished thesis by
Köcher <cit.>. We establish that this undecidability holds even with the restriction on colors being regular sets:

The "$k$-regular colorability problem" on "automatic graphs" is undecidable, for every $k\geq 2$. This holds also for connected "automatic graphs".

By reduction from the "$k$-regular colorability problem" we obtain an important consequence for our separability problem:
It is undecidable to check if two "automatic relations" can be separated by a "recognizable relation"
defined by a fixed number of unions of products of regular languages. More specifically, fix $k > 0$
and define $\intro*\kPROD$ as the class of "recognizable relations" of the form $S = \bigcup_{1 \leq i \leq k} L_{i,1} \times \cdots \times L_{i,n}$—this hierarchy is intertwined with
the $(\kREC)_{k > 0}$ hierarchy introduced previously. We
show that the $\kPROD$-"separability problem", "ie", the problem of checking separability for binary "automatic relations" $R$ and $R'$ in terms of a recognizable relation $S$ in the class
$\kPROD$, is undecidable for $k \geq 2$.

The $\kPROD$-"separability problem" is undecidable, for every $k \geq 2$.

At this point, a natural question is whether our decision of restricting the study to the class $\kPROD$, for fixed $k > 1$, is not too strong, in the sense that
it turns undecidable not only the separability but also the definability problem for "automatic relations". We show that this is not the case; in fact, by using a
simple adaptation of the proof techniques in <cit.> we can show that the problem of checking if an automatic relation can be expressed
as a recognizable relation in $\kPROD$, for a fixed $k > 0$, is decidable in single-exponential time:
The $\kPROD$-"definability problem" is decidable, for every $k > 0$.

For simplicity, we focus on binary "automatic relations" only. Extending the decidability results to $n$-ary automatic relations, for $n > 2$ is direct by applying tools in <cit.>.

§ PRELIMINARIES

Automatic and recognizable relations.

Let $\A$ be a finite alphabet. We write $\A_\bot$ for the
extension of $\A$ with a fresh symbol $\bot$.
Given a pair $(w_1,w_2) \in \A^* \times \A^*$,
we write $w_1 \otimes w_2$ for the word over alphabet
$\A_\bot \times \A_\bot$ that is obtained as follows: first, padding the shorter word with $\bot$'s until both words are of the same length,
and then reading the two words synchronously as if they were a single word over a binary alphabet. For example, if $w_1 = aaba$ and $w_2 = aa$, then
$w_1 \otimes w_2 = (a,a)(a,a)(b,\bot)(a,\bot)$.

For any relation $R \subseteq \A^* \times \A^*$, let us write
$\intro*\lotimes R$ to denote the set

\[\lotimes R \ \defeq \ \set{u \otimes v \mid (u,v) \in R} \ \subseteq \ (\A_\bot \times \A_\bot)^*.\]

We then have the following:

* $R \subseteq \A^* \times \A^*$ is an ""automatic relation"" iff $\lotimes R$ is a regular language;

* $R \subseteq \A^* \times \A^*$ is a ""recognizable relation"" iff
$R = \bigcup_{i=1}^n A_i \times B_i$,
where $n \in \N$ and all the $A_i$'s and $B_i$'s are regular languages over $\A$.

We denote by $\intro*\REC$ the class of all "recognizable relations".

For any fixed constant $c > 0$, the relation $R$ composed by all pairs of words of the form $(a^n,a^{n+c})$, for $n \geq 0$, is "automatic". In turn, $R$ is not "recognizable". An example of a non-"automatic relation" is the one consisting of all pairs of the form $(a^n,a^{d \cdot n})$, for $n > 0$, for any constant $d > 1$.

Let $R$ and $R'$ be "automatic relations" over an alphabet $\A$. A "recognizable relation" $S$ over $\A$
""separates"" $R$ from $R'$
if $R \subseteq S$ and $R' \cap S = \emptyset$.

Consider the "automatic relations" $R = \{(a^n,a^{n+1}) \mid n\geq 0\}$ and $R' = \{(a^n,a^{n+2}) \mid n\geq 0\}$.
They are "separable" by the "recognizable relation"

\[S = (A_{\rm even} \times A_{\rm odd}) \, \cup \, (A_{\rm odd} \times A_{\rm even}),\]

where $A_{\rm even}$ and $A_{\rm odd}$ are the regular languages $(aa)^*$ and $a(aa)^*$, respectively.

We study the following separability problem, for a class $\cal C$ of "recognizable relations".

Problem:     $\cal C$-""separability problem""

Input:     "Automatic relations" $R$ and $R'$ over $\A$

Question:     Is there a "recognizable relation" in $\cal C$ over $\A$
that "separates" $R$ from $R'$?

We also consider the $\cal C$-""definability problem"",
which takes as input an automatic relation $R$ and asks if there is a recognizable relation $S$ with $S = R$.
It is easy to see that the $\cal C$-"definability problem" corresponds to an instance
of the $\cal C$-"separability problem".

For any class $\cal C$ of recognizable relations, the $\cal C$-"definability problem" is Turing-reducible to the $\cal C$-"separability problem".

Reduce an instance $R$ of the "definability problem" to the instance
$(R,\, (\A^*\times \A^*) \setminus R)$ of the "separability problem".

The following is known regarding the complexity of the $\REC$-definability problem.

The $\REC$-"definability problem" for "automatic relations" specified by non-deterministic automata
is "PSpace"-complete.

Automatic graphs.
Let $R$ be a binary "automatic relation" over $\A$. This relation naturally defines a directed graph
$\intro*\GraphR = (\A^*,R)$, "ie",
the nodes of $\GraphR$ are the words over $\A^*$ and there is an edge in $\GraphR$ from word $u$ to word $v$ iff $(u,v) \in R$.
An ""automatic graph"" is a graph of the form $\GraphR$, for $R$ an "automatic relation".
A ""$k$-coloring"" of $\GraphR$ is a partition of $\A^*$
into $k$ sets $V_1, \dotsc V_k$ such that $(V_i \times V_i) \cap E = \emptyset$ for every $i$.

Consider again the "automatic relation" $R = \{(a^n,a^{n+c}) \mid n \geq 0\}$, where $c > 0$ is a fixed constant. The graph $\GraphR$ is formed by a disjoint union of $c$ infinite directed paths, and thus it is "2-colorable".
A ""$k$-regular coloring"" of $\GraphR$ is a "$k$-coloring" whose colors $(V_i)_{1 \leq i \leq k}$ are regular languages.
A ""regular coloring"" is a "$k$-regular coloring" for some $k$.

The "automatic graph" $\GraphR$ from <Ref> is "2-regular colorable". In fact, it suffices to define color $V_1$ as having every word of the form $a^n$ with
$n \equiv i$ (mod $2c$), for $i \in [0,c-1]$, and $V_2 = \A^* \setminus V_1$.
The ""$k$-regular colorability problem"" is the problem of whether $\GraphR$ has a "$k$-regular coloring", given an "automatic relation" $R$. The ""regular colorability problem"" is the problem of whether $\GraphR$ has a "regular coloring".

§ SEPARABILITY IS EQUIVALENT TO REGULAR COLORABILITY

We start by showing that the "separability problem" in terms of arbitrary "recognizable relations" is equivalent, under polynomial time reductions,
to the "regular colorability problem". To make our statement precise, we need some terminology introduced below.
Let $\intro*\kREC$ be the class of languages expressed by unions of products of $k$ regular languages which form a partition, that is (in the binary case), relations of the form $(L_{i_1} \times L_{j_1}) \cup \dotsb \cup (L_{i_\ell} \times L_{j_\ell})$ for some regular partition $L_1, \dotsc, L_{k}$ of $\A^*$ and $\ell \in \N$.
Note that $\REC = \bigcup_k \kREC$.

Let us denote by $\intro*\Id$ the identity relation (on any implicit alphabet). Observe that $\Id$ is "automatic" but not "recognizable".

We start with the last two reductions.
Given an "automatic graph" $\GraphR[E]$ over an alphabet $\A$, consider the instance $R_1,R_2$ for the $\REC$-"separability problem", where
$R_1 = E$ and $R_2 = \Id$.

If $\GraphR[E]$ is "$k$-regular colorable" via the coloring $V_1, \dotsc, V_k$ then the $\kREC$ relation
$\bigcup_{i \neq j} V_i \times V_j$ separates $R_1$ and $R_2$.

Conversely, if a $\kREC$ relation $R \subseteq \A^* \times \A^*$ on the partition $V_1 \dcup \dotsb \dcup V_k = \A^*$ separates $R_1$ and $R_2$, then $\bigcup_{i \neq j} V_i \times V_j$ also separates $R_1$ and $R_2$, and this implies that $V_1, \dotsc, V_k$ is a $k$-coloring for $\GraphR[E]$.

For the first reduction, let us introduce some terminology.
Given two relations $R_1,R_2$ over $\A^*$, say that $u \in \A^*$ is ""compatible"" with
$u' \in \A^*$ when for all word $v \in \A^*$:

*: $(u,v) \in R_1 \Rightarrow (u',v) \not\in R_2$
*: $(v,u) \in R_1 \Rightarrow (v,u') \not\in R_2$,

*: $(u',v) \in R_1 \Rightarrow (u,v) \not\in R_2$
and   *: $(v,u') \in R_1 \Rightarrow (v,u) \not\in R_2$.

Define the ""incompatibility graph"" $\intro*\incompGraph{R_1}{R_2}$
as the graph whose vertices are all words of $\A^*$,
and with an edge from $u$ to $v$ whenever $u$ is not "compatible" with $v$.
Note that $\incompGraph{R}{\Id}$ is exactly the graph $\GraphR$.
For a less trivial example of an "incompatibility graph", see <Ref>.

If $R_1$ and $R_2$ are "automatic", then so is $\incompGraph{R_1}{R_2}$.
Moreover, we can build an automaton for $\incompGraph{R_1}{R_2}$ in polynomial time in the size of the automata for $R_1$ and $R_2$.

Given an instance $(R_1,R_2)$ of the "separability problem", we
reduce it to the "regular colorability problem" on its "incompatibility graph" $\incompGraph{R_1}{R_2}$.

Left-to-right implication:
Assume that there exists $S$ in $\kREC$ that "separates" $R_1$ from $R_2$.

Then $S$ can be written as $(A_{i_1}\times A_{j_1}) \cup \cdots \cup (A_{i_\ell}\times A_{j_\ell})$,
where $(A_1,\hdots,A_k)$ is a partition of $\A^*$ in $k$ regular languages.
We define the color of a word $u \in \A^*$ as the unique $i \in \lBrack 1,k \rBrack$
"st" $u \in A_i$. In other words, the coloring is simply $(A_1,\hdots,A_k)$.

This is indeed a proper coloring: if $u$ and $u'$ have the same color,
we claim that $u$ is "compatible" with $u'$. In fact, take any $v \in \A^*$. If $(u,v) \in R_1$,
then $(u,v) \in S$, so $(u,v) \in A_{i_m}\times A_{j_m}$ for some $m$. But since $u$ has the same color
as $u'$, the fact that $u \in A_{i_m}$ implies $u' \in A_{i_m}$, and hence
$(u',v) \in A_{i_m}\times A_{j_m}\subseteq S$.
But $S$ separates $R_1$ from $R_2$, and therefore $(u',v) \not\in R_2$. This tells us that  holds.
The other conditions hold by symmetry.
We conclude that $(A_1,\hdots,A_k)$ defines
a proper coloring of $\incompGraph{R_1}{R_2}$, and this coloring, with $k$ colors, is
"regular@regular coloring" since the $A_i$'s are regular languages by definition.

Right-to-left implication: Assume that $\incompGraph{R_1}{R_2}$ is finitely colorable, say by
$(A_1,\hdots,A_k)$. Then let $S$ be the union of all $S_i$'s where

\begin{align*}
S_{i} & \defeq \{(u,v) \mid u \in A_i \text{ and } (u',v) \in R_1 \text{ for some } u' \in A_i \}\\
&         \hphantom{\defeq~}\cup \{(u,v) \mid v \in A_i \text{ and } (u,v') \in R_1 \text{ for some } v' \in A_i \}.
\end{align*}

Since $(A_1,\hdots,A_k)$ covers every node of $\incompGraph{R_1}{R_2}$, we get $R_1 \subseteq S$.
Moreover, we claim that $R_2 \cap S = \emptyset$. Indeed, if $(u,v) \in S$,
then $(u,v) \in S_{i}$ for some $i,j$. It either means that 1
$(u',v) \in R_1$ for some $u' \in A_i$, or 2 $(u,v') \in R_2$
for some $v' \in A_i$. In case 1, the fact that $u \in A_i$ implies that $u$ and $u'$
have the same color. Thus, $u$ must be "compatible" with $u'$ and hence
$(u,v) \not\in R_2$ using . The other case is symmetric.
Therefore, $(u,v) \not\in R_2$, and thus $S$ separates $R_1$ from $R_2$.

Finally,  $S$ is "recognizable"; in fact,
$S = \bigcup_{i=1}^k \bigl( A_i \times R_1[A_i] \bigr) \cup \bigl( R_1^{-1}[A_i] \times A_i \bigr)$,
where for any set $X \subseteq \A^*$ we define $R_1[X]$ (resp. $R_1^{-1}[X]$) as the set
of $v\in \A^*$ (resp. $u \in \A^*$) such that $(u,v) \in R_1$ for some $u \in X$
(resp. $v\in X$).
Hence, $R_1$ and $R_2$ are $\REC$-"separable".

It is not known to date whether the "regular colorability problem" is decidable, and hence
the same holds for the $\REC$-"separability problem"
in light of the previous theorem. This is due to the fact that there are no known characterizations of when an "automatic graph" is finitely colorable.
In spite of this, we believe that the connection between separability and finite colorability is of interest, as it provides us with a way to define and study meaningful
restrictions of our problems. The first such a restriction corresponds to the "$k$-regular colorability problem" for "automatic graphs", which we study in the next section.

§ $\BOLDSYMBOL{K}$-REGULAR COLORABILITY PROBLEM

While we do not know how to approach the "regular colorability problem", we show that as soon as we add the restriction that the number of colors be bounded, the problem becomes undecidable; i.e., the "$k$-regular colorability problem" is undecidable for $k\geq 2$. Using this, we obtain in the next section
the undecidability for the "separability problem" on two natural classes of
"recognizable relations". This is proven by a reduction from a suitable problem on reversible
Turing Machines with certain restrictions, which we call “well-founded”.

§.§ Regularity of Reachability for Turing Machines

We use the standard notation $u[i..j]$ to denote the factor of a word $u$ between (and including) positions $i$ and $j$, and $u[i]$ to denote $u[i..i]$.

Consider any deterministic Turing Machine (TM) $T = \tup{Q,\Gamma,\bot,\delta,q_0,F}$, where $Q$ is the set of states, $\Gamma$ is tape alphabet, $\bot$ is the blank symbol, $\delta: (Q \setminus F) \times \Gamma_\bot \to Q \times \Gamma \times \set{L,R}$ is the transition (partial) function, where $\Gamma_\bot = \Gamma \cup \set\bot$, and $q_0$ and $F$ is the initial and set of final states, respectively.

We represent a configuration with tape content $w \cdot \bot^\omega$ (where $w \in \Gamma^* \cdot \set{\bot}$), in state $q$ and with the head pointing to the cell number $1 \leq i \leq |w|$, as the string

\[
w[1..i-1] \cdot (w[i],q) \cdot w[i+1..|w|]
\]

over the alphabet $\A_T = \Gamma \cup (\Gamma_\bot \times Q)$.
In light of this representation, we will henceforth denote by “configuration” any string from the set  $\intro*\configs \defeq (\Gamma^* \cdot (\Gamma_\bot \times Q)) \cup  (\Gamma^* \cdot (\Gamma \times Q) \cdot \Gamma^*)$. The ""initial configuration"" is $(\bot,q_0)$.
The ""configuration graph"" of $T$ is the infinite graph $\intro*\confGraph$ having $\configs$ as set of vertices and an edge from $c$ to $c'$, denoted $c \rightarrow c'$, if $c'$ is the configuration of the next step of $T$ starting from $c$. Observe that the "configuration graph" $\confGraph$ of any TM $T$ is an effective "automatic graph" (see, e.g., <cit.>).

We say that a deterministic TM $T$ is ""reversible"" if every node of $\confGraph$ has in-degree at most 1, in other words if the machine is co-deterministic.
We say that a TM $T$ is a ""well-founded Reversible Turing Machine"" (wf-RTM) if its "configuration graph" is such that (1) the "initial configuration" has in-degree 0 (2) every node has in-degree and out-degree at most one (3) there are no infinite backward paths $c_1 \leftarrow c_2 \leftarrow \dotsb$ in $\confGraph$.

Note that every "well-founded Reversible Turing Machine" is deterministic and "reversible" and, moreover,
its "configuration graph" is a (possibly infinite) disjoint union of
directed paths, which are all finite, or isomorphic to $(\mathbb{N}, +1)$.
The set of ""reachable configurations"", denoted by $\intro*\Reach$, is
the set of all configurations that admit a path from the "initial configuration"

in $\confGraph$, for a given TM $T$.
Such a configuration graph is depicted on <Ref>.

The ""reachable regularity problem"" is the problem of, given a "wf-RTM" $T$, whether its set of "reachable configurations" is a regular language. To show that is it undecidable, we exhibit a reduction from the halting problem on deterministic "reversible" Turing machines.

The halting problem on deterministic "reversible" Turing machines is undecidable.

For more details and pointers on reversible Turing machines, see <cit.>.

The "reachable regularity problem" is undecidable.

By reducing the halting problem on deterministic reversible Turing machines,
in such a way that the "reachable configurations" whose
state $q$ coincide with the state of the original machine are
of the form $(u q v a^n b^n)$ where $(u q v)$ is a configuration of the original machine,
$a$ and $b$ are new symbols,
and $n\in\N$. Transitions are defined in such a way that the new machine is a
"wf-RTM", and moreover:

* if the original machine was halting, then the "reachable configurations"
of the new one is finite and hence regular;

* otherwise, the set of "reachable configurations" is not regular,
which follows from the non-regularity of any infinite subset of $\{a^n b^n \mid n \in \N\}$.

More details and an illustration can be found in <Ref>.

§.§ Undecidability of the $\boldsymbol{k}$-Regular Colorability Problem

We can now show undecidability for the "$k$-regular colorability problem" by reduction from the "reachable regularity problem" as defined before.

Given an "automatic graph", the set of nodes with no predecessor is effectively a regular language.

Configuration graph of a "well-founded Reversible Turing Machine".

The automatic graph to which it is reduced.

Reduction used in the proof of <Ref>.

By reduction from the "reachable regularity problem" for "wf-RTM"s
(<Ref>). We first show it for $k=2$.
Given a "wf-RTM" $T$, let $c_{\textit{init}}$ be its "initial configuration".
Observe that the set $\intro*\Init$ of all vertices of $\confGraph$ with in-degree $0$ is an effective regular language (by <Ref>), and that $c_{\textit{init}} \in \Init$. Let $B$ and $R$ be fresh symbols.
Consider the "automatic graph" $\GraphR[E]$ having
an edge from $(z,c)$ to $(z',c')$ if either

* $(z,z') = (B,R)$ and $c=c'$;

* $(z,z') = (R,B)$ and there is an edge from $c$ to $c'$ in $\confGraph$; or

* $(z,z') = (B,B)$, $c = c_{\textit{init}}$ and $c' \in \Init \setminus \set{c_{\textit{init}}}$.

Fresh symbols $B$ and $R$ are utilized to represent two versions of each configuration - one in Blue and one in Red. This graph is depicted
on <Ref>.
Note that $\GraphR[E]$ is connected and "2-colorable": in fact, it is a directed (possibly infinite) tree with root $(B,c_{\textit{init}})$.

We claim that $\GraphR[E]$ is "$2$-regular colorable" if, and only if, the set of "reachable configurations" of $T$ is a regular language.
In fact, up to permuting the two-colors,
$\GraphR[E]$ admits a unique 2-coloring, defined by:

\[
C_1 ~~ \defeq ~~ \{B\} \times \Reach ~~\cup~~ \{R\} \times (\configs \setminus \Reach)
\]

and $C_2$ is the complement of $C_1$.
If $\Reach$ is regular, then so is $C_1$. Dually, if $C_1$ is regular, then
$\Reach$ is the set of configurations $c$ such that $(B,c) \in C_1$ and hence is regular.
It follows that $\GraphR[E]$ is "$2$-regular colorable" if and only if
the "reachable configurations" of $T$ are regular, which concludes the proof for $k=2$.

To prove the statement for any $k>2$, we define $\GraphR[E_k]$ as the result of adding a $(k-2)$-clique to $\GraphR[E]$ and adding an edge from every vertex of the clique to every vertex incident to an edge of $E$. This forces the clique to use $k-2$ colors that cannot be used in the remaining part of the graph and the proof is then analogous.

Note that this reduction provides an easy way of building
graphs in the shape of <Ref> that are "2-colorable" (in fact, they are trees) but not "2-regular colorable". In fact, we can provide a slightly more
direct construction.

On the alphabet $\A = \{a,b\}$, the tree $\+T$ whose set of vertices is $V = a^*b^*$ and whose set
of edges is $E = E_{\mathrm{incr}} \cup E_{\mathrm{init}}$, with

\begin{align*}
E_{\mathrm{incr}} & = \{(a^pb^q,\, a^{p+1}b^{q+1}) \mid p,q \in \N\} \\
E_{\mathrm{init}} & = \{(\varepsilon,\, a^p) \mid p \in \N\} \cup \{(\varepsilon,\, b^q) \mid q \in \N\},
\end{align*}

is "automatic" but not "2-regular colorable": indeed, its only "2-coloring"
consists in partitioning the vertices of $\+T$ into

\[
C = \{a^n b^n \mid n \in 2\N\}
\cup \{a^p b^q \mid p > q \text{ and $q$ is odd}\}
\cup \{a^p b^q \mid p < q \text{ and $p$ is odd}\}
\]

and its complement $V \setminus C$.
Let $P = \{a^p b^q \mid p, q \in 2\N\} = (aa)^*(bb)^*$:
$P$ is regular, yet $C \cap P = \{a^n b^n \mid n \in 2\N\}$ is not.
Hence, $C$ is not regular, and thus $\+T$ is not "2-regular colorable".

The "automatic tree@automatic graph" $\+T$ of <Ref>,
and its unique "2-coloring" $(C, V\setminus C)$, which is not "regular@@coloring".

§ SEPARABILITY FOR BOUNDED RECOGNIZABLE RELATIONS

In this section we capitalize on the undecidability result of the previous section, showing how this implies the undecidability for the "separability problem" on two natural classes of bounded "recognizable relations", namely: $\kREC$, and $\kPROD$.
Remember that, for any $k$, $\reintro*\kPROD$ is the subclass of $\REC$ consisting of unions of $k$ cross-products of regular languages (which is a subclass of $\kREC[2^{2k}]$).

First, observe that the $\kREC[1]$-"separability problem" is trivially decidable, since the only possible "separator" is $\A^* \times \A^*$. However, for any other $k>1$, the problem is undecidable.

The $\kREC$-"separability problem" is undecidable, for every $k>1$.

A consequence of the reduction from the "$k$-regular colorability problem" of <Ref>, combined with the undecidability of the latter for every $k>1$ (<Ref>).

On the $\kPROD$ hierarchy we will find the same phenomenon. In particular the case $k=1$ is also trivially decidable.

The $\kPROD[1]$-"separability problem" is decidable.

Given two "automatic relations" $R_1, R_2$, there exists $S \in $ [1]
that "separates" $R_1$ from $R_2$ if and only if $\pi_1(R_1)\times \pi_2(R_1)$
"separates" $R_1$ from $R_2$.

As soon as $k>1$, the $\kPROD$ "separability problem" becomes undecidable. This is a consequence of the following simple lemma.

A symmetric "automatic relation" $R$ and the identity $\Id$ are "separable" by a relation in $\kPROD[2]$ iff they have a "separator" of the form $(A \times B) \cup (B \times A)$.

Assume that $S \in \kPROD[2]$ "separates" $R$ from $\Id$.
Then $R \subseteq S$, but since $R$ is symmetric, $R = R^{-1} \subseteq S^{-1}$ so
$R \subseteq S \cap S^{-1}$, and hence $R \subseteq S \cap S^{-1}$.
Moreover, since $S$ has a trivial intersection with $\Id$, so does $S \cap S^{-1}$.
Hence, $S \cap S^{-1}$ "separates" $R$ from $\Id$.

Since $S \in \kPROD[2]$, there exists $A_1,A_2,B_1,B_2 \subseteq \A^*$ such that
$S = A_1 \times B_1 \cup B_2 \times A_2$.
Note that $S \cap \Id = \emptyset$ yields $A_i \cap B_i = \emptyset$ for each $i \in \{1,2\}$.

\begin{align*}
S \cap S^{-1} &
\bigl( A_1 \times B_1 \cup B_2 \times A_2 \bigr)
\cap \bigl( B_1 \times A_1 \cup A_2 \times B_2 \bigr) \\
\bigl( (A_1 \times B_1) \cap (B_1 \times A_1) \bigr)
\cup \bigl( (A_1 \times B_1) \cap (A_2 \times B_2) \bigr) \\
\hphantom{=\;} \cup \bigl( (B_2 \times A_2) \cap (B_1 \times A_1) \bigr)
\cup \bigl( (B_2 \times A_2) \cap (A_2 \times B_2) \bigr) \\
\bigl( \overbrace{(A_1 \cap B_1) \times (A_1 \cap B_1)}^{= \emptyset} \bigr)
\cup \bigl( (A_1 \cap A_2) \times (B_1 \cap B_2) \bigr) \\
\hphantom{=\;} \cup \bigl( (B_1 \cap B_2) \times (A_1 \cap A_2) \bigr)
\cup \bigl( \underbrace{(A_2 \cap B_2) \times (A_2 \cap B_2)}_{= \emptyset} \bigr)\\
= \bigl( (A_1 \cap A_2) \times (B_1 \cap B_2) \bigr)
\cup \bigl( (B_1 \cap B_2) \times (A_1 \cap A_2) \bigr).\qedhere
\end{align*}

We can then establish the following:

A symmetric "automatic relation" $R$ and $\Id$ are "separable" by a relation in $\kPROD[2]$ iff $\GraphR$ is "$2$-regular colorable".

By observing that for any symmetric relation $R \subseteq \A^* \times \A^*$, we have that $A,B \subseteq \A^*$ is a coloring of $\GraphR$ if, and only if, $(A \times B) \cup (B \times A)$ "separates" $R$ from $\Id$.

We can now easily show undecidability for the $\kPROD[2]$ "separability problem" by reduction from the "$2$-regular colorability problem".

The $\kPROD[2]$-"separability problem" is undecidable.

By reduction from the "$2$-regular colorability problem" on "automatic graphs", which is undecidable by <Ref>. Let $\GraphR$ be an "automatic graph" and $\GraphR[R']$ the symmetric closure of $\GraphR$. It follows that $\GraphR[R']$ is still "automatic" and that there is a "$2$-regular coloring" for $\GraphR[R']$ iff there is a "$2$-regular coloring" for $\GraphR$ (the same coloring in fact).
Thus, by <Ref>, $\GraphR$ is "$2$-regular colorable" iff
there is a $\kPROD[2]$ relation that "separates" $\GraphR[R']$ from $\Id$.

Further, this implies undecidability for every larger $k$:

Construction in the proof of <Ref> for $k = 5$. $S$ is depicted as the union of two (gray) rectangles since $S \in \kPROD[2]$.
The relation $R'_1$ is obtained from $R_1$ (blue shape) by adding all blue edges,
namely $(a_i, b_i)$ for $1\leq i \leq k-2$. The relation $R'_2$ is obtained from $R_2$ (red shape) by adding
all red edges, namely every other edge involving a vertex $a_i$ or $b_i$.
Finally, $S'$ (five gray rectangles) is obtained from $S$ by adding
each $\{a_i\} \times \{b_i\}$.

The case $k=2$ is shown in <Ref>, so suppose $k>2$.
The proof goes by reduction from the $\kPROD[2]$-"separability problem". Let $R_1,R_2$ be a pair of "automatic relations" over an alphabet $\A$. Consider the alphabet extended with $2(k-2)$ fresh symbols $\A' = \A \dcup \set{a_1, \dotsc, a_{k-2}, b_1, \dotsc, b_{k-2}}$. We build "automatic relations" $R'_1,R'_2$ over $\A'$ such that $(R_1,R_2)$ are $\kPROD[2]$ "separable" over $\A$ iff $(R'_1,R'_2)$ are $\kPROD$ "separable" over $\A'$.

Let $R'_1 = R_1 \dcup \set{ (a_i,b_i) : 1 \leq i \leq k-2}$ and

\begin{align*}
R'_2 =  R_2 \dcup {}&\set{(a_i,w) : w \in \A^*, 1 \leq i \leq k-2} \dcup {}\\
&\set{(w,b_i) : w \in \A^*, 1 \leq i \leq k-2} \dcup {}\\
&\set{(a_i,b_j) : 1 \leq i,j \leq k-2, i \neq j} \dcup {}\\
&\set{(b_i,a_j) : 1 \leq i,j \leq k-2}
\end{align*}

If $(R_1,R_2)$ has a $\kPROD[2]$ "separator" $S$, then $\tilde S \dcup \set{(a_i,b_i) : 1 \leq i \leq k-2}$ is a $\kPROD$ "separator" of $(R'_1,R'_2)$.

Conversely, if $S' = (A_1 \times B_1) \cup \dotsb \cup (A_k \times B_k)$ is a $\kPROD$ "separator" of $(R'_1,R'_2)$, then for every $i$ there must be some $j_i$ such that $A_{j_i} \times B_{j_i}$ contains $(a_i,b_i)$. Observe that

* $A_{j_i} \cup B_{j_i}$ cannot contain any $a_{i'}$ or $b_{i'}$ for $i' \neq i$, and

* $A_{j_i} \cup B_{j_i}$ cannot contain any $w \in \A^*$;

since otherwise we would have $(A_{j_i} \times B_{j_i}) \cap R'_2 \neq \emptyset$.
Hence, $\set{i \mapsto j_i}_i$ is injective, and thus $S'$ is of the form $S' = (A_1 \times B_1) \cup (A_2 \times B_2)  \cup (\set{a_1} \times \set{b_1}) \cup \dotsb \cup (\set{a_{k-2}} \times \set{b_{k-2}})$. We can further assume that $A_1,B_1,A_2,B_2$ do not contain any $a_i$ or $b_i$ since otherwise we can remove them preserving the property of being a $\kPROD$ "separator" of $R'_1$ and $R'_2$.
Hence, $S \defeq (A_1 \times B_1) \cup (A_2 \times B_2)$ must cover $R_1$ and be disjoint from $R_2$, obtaining that $S$ is a $\kPROD[2]$ "separator" of $R_1$ and $R_2$.

§ DEFINABILITY FOR BOUNDED RECOGNIZABLE RELATIONS

Up until now, we have examined two hierarchies of bounded recognizable relations, namely $\kPROD$ and $\kREC$.
Our previous analysis demonstrated that, for any element in these hierarchies (where $k>1$), the "separability problem" is undecidable. Nevertheless,
we will now establish that the "definability problem" is decidable.

Given an "automatic" relation $R \subseteq \A^* \times \A^*$, consider the "automatic" equivalence relation $\intro*\autequiv \subseteq \A^* \times \A^*$, defined as $w \mathrel{\autequiv} w'$ if for every $v \in \A^*$ we have

* $(w,v) \in R$ iff $(w',v) \in R$, and

* $(v,w) \in R$ iff $(v,w') \in R$.

It turns out that equivalence classes of $\autequiv$ define the coarsest partition onto which $R$ can be recognized in terms of $\kREC$:

For every "automatic" $R \subseteq \A^* \times \A^*$, $\autequiv$ has index at most $k$ if, and only if, $R$ is in $\kREC$.

Assume that $\autequiv$ has the equivalence classes $E_1, \dotsc, E_k$. Consider the set $P \subseteq \set{1, \dotsc, k}^2$ of all pairs $(i,j)$ such that there are $u_i \in E_i$ and $u_j \in E_j$ with $(u_i,u_j) \in R$. Define the $\kREC$ relation $R' = \bigcup_{(i,j) \in P} E_i \times E_j$. We claim that $R=R'$.
In fact, by definition of $\autequiv$, note that if there are $u_i \in E_i$ and $u_j \in E_j$ with $(u_i,u_j) \in R$, then $E_i \times E_j \subseteq R$. Hence, $R' \subseteq R$.
On the other hand, for every pair $(u,v) \in R$ there is $(i,j) \in P$ such that $u \in E_i$, $v \in E_j$ implying $(u,v) \in R'$.
Hence, $R \subseteq R'$.

If $R$ is a union of products of sets from the partition $E_1 \dcup \dotsb \dcup E_k = \A^*$, then every two elements of each $E_i$ are $\autequiv$-related, and thus $\autequiv$ has index at most $k$.

We can then conclude that the definability problem for $\kREC$ is decidable.

The $\kREC$-"definability problem" is decidable, for every $k > 0$.

An "automatic relation" $R$ is in $\kREC$ iff $\autequiv$ has at most $k$ equivalence classes by <Ref>.

In other words, an "automatic relation" $R$ is not in $\kREC$ iff the complement of $\autequiv$ contains a $(k+1)$-clique, which can be easily tested.

The relation $\autequiv$ can also be used to characterize which automatic relations are definable in the class $\kPROD$.

An "automatic relation" $R$ is in $\kPROD$ if, and only if, $R=(A_1 \times B_1) \cup \dotsb \cup (A_k \times B_k)$ where each $A_i$ and $B_i$ is a union of equivalence classes of $\autequiv$.

It suffices to show that for every equivalence class $E$ from $\autequiv$, if $A_1 \cap E \neq \emptyset$ then $R = ((A_1 \cup E) \times B_1) \cup \dotsb \cup (A_k \times B_k)$, and similarly for $B_1$. Assume $w \in A_1 \cap E$ and take any pair $(u,v) \in E \times B_1$. We show that $(u,v) \in R$. By definition of $\autequiv$, since $(w,v) \in R$ and $w \mathrel{\autequiv} u$, we have that $(u,v) \in R$.

Again, this characterization allows us to show that definability in the class $\kPROD$ is decidable.

By brute force testing whether the "automatic relation" $R$ is equivalent to $(A_1 \times B_1) \cup \dotsb \cup (A_k \times B_k)$ for every possible $A_i,B_i$ which is a union of equivalence classes of $\autequiv$.

§ DISCUSSION

In this paper, we establish among other things undecidability of the
"$k$-regular colorability problem" for $k \geq 2$. Yet, little is known about
the "regular colorability problem".

The $\REC$-"separability problem"—or, equivalently, the "regular colorability problem"—is undecidable.

Beyond its complexity status, the structural properties of "regular colorability" evades us:

Over "automatic graphs", the following notions are pairwise disjoint:

* to be finitely "regular colorable",

* to be finitely colorable,

* not to contain unbounded cliques.

Note that the implications (1) $\Rightarrow$ (2) $\Rightarrow$ (3) trivially hold.
Moreover, recall that while the "automatic tree" of <Ref>
is not "2-regular colorable", it is "3-regular colorable" (it suffices to color $\varepsilon$ with a new color, and then color $a^p b^q$ by looking at the parity of $p-q$). Hence,
it does not prove that (2) $\not\Rightarrow$ (1).
Likewise, on arbitrary infinite graphs, we know that
there exists triangle-free graphs that are not finitely
colorable <cit.>—but we believe these
graphs not to be "automatic", and hence they would not prove that (3) $\not\Rightarrow$ (2).

Finally, observe that it is decidable to test whether an "automatic graph" has infinite cliques <cit.>. We conjecture that this property generalizes to unbounded cliques.

The problem of whether an "automatic graph" has bounded cliques is decidable.

What about a fixed alphabet? Do all results hold already for a binary alphabet?
I think that "wf-RTM" with 2 letters and one tape are as expressive as Turing machines.
A configuration can be encoded using 3 letters (2 letters for the tape content, the same letters encode the current state, but we might need a special symbol for separating them).
Hence, I think that <Ref> already holds for only a fixed alphabet (3 letters using this argument, maybe we can do better).

§ MISSING PROOFS

By definition, the "incompatibility relation" $\incompGraph{R_1}{R_2}$ can be written as
$R_{\neg\compL} \cup R_{\neg\compLpr} \cup R_{\neg\compR} \cup R_{\neg\compRpr}$, where:

\begin{align*}
R_{\neg\compL} &\defeq \big\{ (u,u') \in \A^* \times \A^* \;\big\vert\; \exists v \in \A^*,\; (u,v) \in R_1 \land (u',v) \in R_2 \big\} \text{,}\\
R_{\neg\compLpr} &\defeq \big\{ (u,u') \in \A^* \times \A^* \;\big\vert\; \exists v \in \A^*,\; (u',v) \in R_1 \land (u,v) \in R_2 \big\} \text{,}\\
R_{\neg\compR} &\defeq \big\{ (u,u') \in \A^* \times \A^* \;\big\vert\; \exists v \in \A^*,\; (v,u) \in R_1 \land (v,u') \in R_2 \big\} \text{, and}\\
R_{\neg\compRpr} &\defeq \big\{ (u,u') \in \A^* \times \A^* \;\big\vert\; \exists v \in \A^*,\; (v,u') \in R_1 \land (v,u) \in R_2 \big\}
\end{align*}

Observe that starting from automata for $R_1$ and $R_2$, then for each
of the relation $R_{\neg\compL}$, $R_{\neg\compLpr}$, $R_{\neg\compR}$ or $R_{\neg\compRpr}$, we can build an automaton recognizing them
using a product construction, which can be implemented in polynomial time.

It then follows that we can build a polynomial automaton recognizing

Encoding of a single transition of the form
“when reading a blank in state $\color{cBlue} p$, write a
$1$, go in state $\color{cBlue} q$ and move right”
of the machine $T$ in the machine $T'$
in the proof of <Ref>.
Red unlabelled states represent states of $T'$
that are not originally present in $T$.

By reduction from the halting problem for deterministic and "reversible" TMs, which is undecidable by <Ref>. Given a deterministic and "reversible" TM $T$ (running on the empty input), consider the TM $T'$ where every time there is a transition $(u, p, v) \to (u', q, v')$ from configuration $c$ to configuration $c'$ in $T$,
simulate this transition in $T'$—$a$'s should be treated as blank symbols—,
and then rewritting $a^n b^n$ into $a^{n+1}b^{n+1}$.
When $T$ writes on a blank symbol that was actually a $a$ in $T'$,
we must also add an extra $a$ (to account for the one that was overwritten):
this case is depicted <Ref>.
Moreover, when $T$ deletes a symbol at the end of the tape,
we must shift the $a^n b^n$ prefix. This can be done by replacing the blank
with an $a$, the last $a$ with a $b$, and deleting the last $b$.

Observe that $T'$ is a "wf-RTM":

* the "initial configuration" $(\bot,q_0,\bot)$ has no predecessor;

* it is deterministic and co-deterministic:

* every configuration inside a path $(u, q, v a^n b^n) \xrightarrow{*} (u, q, v a^{n+1} b^{n+1})$
has, by definition, exactly in- and out-degree one;

* every configuration of the form $(u, p, v a^n b^n)$ has as many predecessors [resp.
successors] in $T'$ as $(u,q,v)$ in $T$, namely one since $T$ was assumed to be
deterministic and "reversible";

* it has no infinite descending chain since $\N$ is well-founded.

Moreover $T'$ has no cycle,
so if $T$ is halting (on an empty input) then the set of "reachable configurations" of $T'$ is finite (since it is a "wf-RTM") and thus regular. If $T$ is not halting, the set of "reachable configurations" of $T'$ is infinite and its projection onto $\set{a,b}$ is an infinite set of words of the form $a^{n} b^{n'}$ where $n-2 \leq n' \leq n+2$. Hence, since regular languages are closed under homomorphic images, the "reachable configurations" of $T'$ cannot be regular.

§ INCOMPATIBILITY GRAPH

Let $\A = \{a,b\}$, $R_1$ be the equal-length relation,

\[
R_2 = \{(u, ua) \mid u \in \A^*\} \cup \{(u, ub) \mid u \in \A^*\}.
\]

Then, $u$ is "incompatible" with $u'$ if $|u| = |u'|+1$ (this is given by  or ),
or if $|u'| = |u|+1$ (this is given by  or ).
$R_2$ and the "incompatibility graph" are depicted in <Ref>.

Note that $R_1$ and $R_2$ are separable by the "recognizable" relation
$S$ consisting of all pairs $(u,v)$ such that $|u|$ and $|v|$ have the same parity.
Moreover, $\incompGraph{R_1}{R_2}$ is "2-regular colorable", the two colors being
the words of even and odd length.

The relation $R_2$.

Incompatibility graph $\incompGraph{R_1}{R_2}$ and its "2-regular coloring".

Automatic graphs of <Ref>, restricted to words of length at most 2.