Loughborough University, United<EMAIL_ADDRESS>University of
Waterloo<EMAIL_ADDRESS>University of Waterloo,
<EMAIL_ADDRESS>Universität Göttingen,
<EMAIL_ADDRESS>Joel Day, Vijay Ganesh,
Nathan Grewal, and Florin Manea [100]Theory of computation $\rightarrow$
Formal languages and automata theory, Theory of computation $\rightarrow$
Logic John Q. Open and Joan R. Access 2 42nd Conference on Very Important
Topics (CVIT 2016) CVIT 2016 CVIT 2016 December 24–27, 2016 Little Whinging,
United Kingdom 42 23

# Formal Languages via Theories over Strings

Joel Day  Vijay Ganesh  Nathan Grewal  Florin Manea

###### Abstract

We investigate the properties of formal languages expressible in terms of
formulas over quantifier-free theories of word equations, arithmetic over
length constraints, and language membership predicates for the classes of
regular, visibly pushdown, and deterministic context-free languages. In total,
we consider 20 distinct theories and decidability questions for problems such
as emptiness and universality for formal languages over them. First, we
discuss their relative expressive power and observe a rough division into two
hierarchies based on whether or not word equations are present. Second, we
consider the decidability status of several important decision problems, such
as emptiness and universality. Note that the emptiness problem is equivalent
to the satisfiability problem over the corresponding theory. Third, we
consider the problem of whether a language in one theory is expressible in
another and show several negative results in which this problem is
undecidable. These results are particularly relevant in the context of normal
forms in both practical and theoretical aspects of string solving.

###### keywords:

String constraints, Word equations, Formal languages, Word Combinatorics

##  1 Introduction

Logical theories based on strings (or words) over a finite alphabet have been
an important topic of study for decades. Connections to arithmetic (see e.g.
Quine [39]) and fundamental questions about free (semi)groups underpinned
interest in logics involving concatenation and equality. Combining these two
things leads to word equations: expressions $\alpha=\beta$ where $\alpha$ and
$\beta$ are terms obtained by concatenating variables and concrete words over
a finite alphabet. For example, if $x$ and $y$ are variables, and our alphabet
is $\Sigma=\\{a,b\\}$, then $xaby=ybax$ is a word equation. Its solutions are
variable-substitutions unifying the two sides: $x\to bb,y\to b$ would be one
such solution in the previous example.

The existential theory of a finitely generated free semigroup consists of
formulas made up of Boolean combinations of word equations. In fact, the
problem of deciding whether such a formula is true is equivalent to
determining satisfiability of word equations, since any such formula can be
transformed into a single word equation without disrupting satisfiability (see
[33, 27]). Famously, Makanin showed in 1977 that satisfiability of word
equations is algorithmically decidable [35]. Since then, several improvements
to the algorithm proposed by Makanin have been discovered: Plandowski [38]
showed that the problem could be solved in PSPACE, which has later been
refined to nondeterministic linear space by Jeż [25]. Schulz [40] showed that
the problem remains decidable even when the variables are constrained by
regular languages, limiting the possible substitutions (see also Chapter 12 of
[33]). On the other hand, if length constraints (requiring that some pairs of
variables are substituted for words of the same length) are permitted, then
the (un)decidability of the problem is a long-standing open problem.

Word equations, and logics involving strings more generally, have remained a
topic of interest within the Theoretical Computer Science community, in
particular due to their fundamental role within Combinatorics on Words and
Formal Languages, and more recently due to interested from the Formal Methods
community. The latter can be attributed to increasing popularity and influence
of software tools called string-solvers, which seek to algorithmically solve
constraint problems involving strings [6, 22]. In this setting, a string
constraint is a property or piece of information about an unknown string, and
the string solvers try to determine whether strings exist which satisfy
combinations of string constraints of various types. Word equations, regular
language membership, and comparisons between lengths are all among the most
prominent building blocks of string constraints, and when combined are
sufficient to model several others. String-solvers are also useful in other
areas like Database Theory, particularly e.g. for evaluating path queries in
graph databases [7] and in connection with Document Spanners [18, 17, 19].

A wealth of string-solvers are now available [26, 10, 36, 28, 1, 42, 8, 2]
(see [6, 22] for an overview). However, the underlying task of determining the
satisfiability of string constraints remains a challenging problem and a
barrier to more effective implementations. Some results already exist
addressing the computability/ complexity and expressibility of combinations of
string constraints. [34, 20, 29, 31, 30] identify restrictions on word
equations which result in a decidable satisfiability problem even when length
constraints are present. Several further ways of augmenting word equations
(i.e., additional predicates or constraints on the variables), are shown to be
undecidable in [12, 15, 11, 23]. Moreover, Büchi and Senger [11] considered
definability in the theory of concatenation and showed, on the one hand, that
length is not definable using equality and concatenation alone, and, on the
other hand, that if predicates are present, which count occurrences of at
least two different letters, we obtain an undecidable theory. Karhumäki,
Plandowski and Mignosi [27] considered explicitly the question of which formal
languages are expressible as the set of solutions to a word equation,
projected onto a single variable. They show that several simple languages are
not expressible, including some simple regular languages. However, they do not
consider the case when word equations may be augmented with additional
constraints, which can drastically change the languages expressed.

Nevertheless, despite results such as those mentioned above, little is known
about the true expressive power of word equations and of string logics
involving word equations in conjunction with other common types of string
constraints. A greater understanding in this regard would help in settling
open problems (such as for whether satisfiability for word equations with
length constraints is decidable), and also with devising string solving
strategies: often simply finding a solution to one constraint is not enough
and the set of solutions must be considered more generally in order to account
for other constraints which might be present, or to determine that no solution
exists. Moreover, a common tactic is to rewrite constraints into some normal
form before solving and understanding when and how this can be done also
requires knowledge of the relative expressive power of subsets of constraints.

This work aims to fill gaps in the understanding of the properties and
expressivity of some of the most important combinations of string constraints
by considering languages expressible in the sense of [27]. In this regard, our
results can be seen as extending [27] to a more general (and more practical)
setting. As such, our wider context requires a range of new approaches and
leads to new questions and insights not considered in previous works.

Our framework: We consider a landscape of string-based logics incorporating
various types of atoms inspired by and strongly related to prominent varieties
of string-constraints. In particular, we consider logics with different
combinations of: equality between strings, concatenations of strings,
membership of formal languages, and linear arithmetic over string-lengths.

In total, we consider 20 distinct families of logical theories (each family
containing a different theory for each possible underlying alphabet $\Sigma$),
which are introduced in detail in Section 3. Taking inspiration from [27] (and
partly from [9], where relation-definability by logics over strings was
studied in a database-theory centered framework), we study these logics from a
formal languages perspective by looking at the set of values a variable may
take while preserving satisfiability of a formula. Specifically, given a
formula $f$ from a quantifier-free logical theory $\mathfrak{T}$, we say that
the language expressed by a variable $x$ occurring in $f$ is the set of
concrete values $w$ such that substituting $x$ for $w$ in $f$ yields a
satisfiable formula. In the general case, we can think of the property that
the formula $f$ defines via the variable $x$. However, since we consider
logics in which $x$ is substituted for finite strings, we get a formal
language.

We are interested both in the expressive power of the logical theories w.r.t.
what languages they can express, and in their computational properties with
respect to canonical decision problems within formal languages such as
emptiness, universality, equivalence and inclusion.

Together, the 4 types of atoms we allow cover many of the most prominent types
of string constraints, as listed in [6]. While predicates related to equality
between strings, concatenations of strings, and linear arithmetic over string-
lengths do not need more explanations, a discussion is in order w.r.t. our
choice of language membership predicates. In this case, they are considered
for the classes of regular, deterministic context-free, or as an intermediary
between the two, visibly pushdown languages. While there are many classes of
languages we might choose to consider between regular and deterministic
context-free, there are several advantages to choosing the visibly pushdown
languages in particular. Firstly, they exhibit an attractive balance of being
computationally reasonable (they have many of the desirable closure and
algorithmic properties of the regular languages) while simultaneously being
powerful enough to provide a reasonable model in many verification and
software analysis applications, in line with our motivations from string-
solving. Moreover, since they directly generalise the regular languages, but
with sufficient memory capabilities to model certain types of length
comparisons, the combination of word equations and visibly pushdown language
constraints generalise the combination of word equations with both length and
regular constraints. The latter is of particular interest in the context of
string-solving, but is a case for which the decidability of satisfiability
remains open and is likely to be difficult to resolve. We show that
satisfiability for the former is undecidable and thus that already a very
limited extension to regular and length constraints is enough to reach this
negative result.

Our results: Firstly, in Section 4, we compare the relative expressive power
of the different theories. On the one hand, we manage to group certain
families together, where they express the same class of languages. In the
technical Lemma 4.11, we show that adding linear arithmetic over string-
lengths to a theory allowing only language membership predicates for a class
of languages with good language theoretic properties does not alter its
expressive power. Thus, the theories in which only regular language (or
visibly pushdown language) membership predicates are allowed and the theories
in which length comparison is added to those membership predicates are
equivalent. While in the case of theories based on regular language membership
predicates we can also add concatenation without changing the expressive
power, we show in Theorem 4.5 that adding this operation to theories based on
visibly pushdown language membership predicates strictly increases their
expressive power, as they can express all recursively enumerable languages.
Moreover, we also provide several separation results between the classes of
language expressed by various theories. One of the ways we achieve this is by
non-trivially extending pumping-lemma style tools for word equations from [27]
to our more general settings. The overall hierarchy of classes of languages
expressible in our theories is depicted in Figure 1.

While our results from Section 4 are already interesting from a language-
theoretic point of view, they are also relevant for the emptiness problem for
classes of languages expressed by our theories, which is equivalent to the
satisfiability problem for formulas over those theories. As such, our results
allow us to non-trivially extend the state-of-the-art related to the
satisfiability of string constraints. In particular, we settle the previously
mentioned interesting case in which word equations (in fact, even
concatenation without explicit string-equality is sufficient) are combined
with visibly pushdown language membership constraints. When combined with
existing results, our results establish a relatively complete description of
when the emptiness problem is decidable/undecidable (see the left part of
Figure 1). The cases left open are the combinations of word equations with
length constraints with or without regular constraints, which are long-
standing open problems.

Further, in Section 5, we consider the universality problem and a related
variant, namely the subset universality problem in which we want to test
whether a language is exactly $S^{*}$ for a subset $S$ of the underlying
alphabet. Again, our results fill in gaps in the knowledge and allow us to
paint a comprehensive picture of the decidability status of these problems for
our theories (see the right part of Figure 1). Since the universal language is
expressible in all our theories, in combination with results from Section 4
and from the literature, we obtain a complete picture for the equivalence and
inclusion problems. However, a substantial further benefit (and a large part
of our motivation for studying this problem) is that it allows us to use
Greibach’s theorem in many cases (as stated in Theorem 5.6) to establish
further undecidability results (e.g., Theorems 6.1 and 5.9). In particular,
Theorem 6.1 is part of a larger line of thought, developed in Section 6, in
which we consider the question of when it is (un)decidable if a language
expressed in one theory can be expressed in another. Such problems are
particularly interesting in the context of practical string solving, because
they essentially ask whether a property defined by one kind of string
constraint can be algorithmically converted to another. Often, it is the
combinations of different kinds of string constraints which lead to high
complexities in solving, so being able to rewrite constraints in different
forms can be a powerful pre-processing technique. We also identify some
interesting cases where Greibach’s theorem is not applicable, and thus where
other approaches are needed (e.g. Theorem 6.3).

Summary: Our aim in this contribution is to obtain a more complete
understanding of the computational properties and expressivity of languages
expressed by various combinations of commonly occurring types of string
constraints. Naturally, we are able to account for several cases by recalling,
or extending existing results from literature, so at the beginning of each
section, we give a single theorem that summarizes existing results and discuss
their consequences. This allows us to subsequently focus on the most
interesting remaining cases, many of which we are able to resolve by drawing
on a range of techniques rooted in formal languages, automata theory,
combinatorics on words and computability theory. Our contributed results are a
substantial improvement the state of understanding of the theories considered,
particularly with respect to their expressive power. In those cases we are
unable to resolve, we identify several interesting new open problems and a
need for novel techniques for tackling them.

##  2 Preliminaries

Let $\mathbb{N}=\\{1,2,3,\ldots\\}$ and
$\mathbb{N}_{0}=\\{0\\}\cup\mathbb{N}$. Let $\mathbb{Z}$ denote the set of
integers. Let $\Sigma=\\{a_{1},a_{2},\ldots,a_{n}\\}$ be an alphabet. We
denote by $\Sigma^{*}$ the set of all words over $\Sigma$ including the empty
word, which we denote $\varepsilon$. In other words, $\Sigma^{*}$ is the free
monoid generated by $\Sigma$ under the operation of concatenation. For words
$u,v\in\Sigma^{*}$ we denote their concatenation either by $u\cdot v$ or
simply as $uv$. Given a set of variables
$\mathcal{X}=\\{x_{1},x_{2},\ldots\\}$ and an alphabet $\Sigma$, a word
equation is a pair
$(\alpha,\beta)\in(X\cup\Sigma)^{*}\times(X\cup\Sigma)^{*}$, usually written
as $\alpha=\beta$. A solution to a word equation is a substitution of the
variables for words in $\Sigma^{*}$ such that both sides of the equation
become identical. Formally, we model solutions as morphisms. That is, we say a
substitution is a (homo)morphism $h:(X\cup\Sigma)^{*}\to\Sigma^{*}$ satisfying
$h(a)=a$ for all $a\in\Sigma$, and a solution to a word equation
$\alpha=\beta$ is a substitution $h$ such that $h(\alpha)=h(\beta)$.

We refer to [24] for standard definitions and well known results from formal
language theory regarding e.g. recursively enumerable languages
($\operatorname{RE}$), regular languages ($\operatorname{REGLang}$), context
free languages ($\operatorname{CFLang}$), deterministic context-free languages
($\operatorname{DCFLang}$), finite and pushdown automata, etc.

In addition, we refer to [3, 4, 5] for background on visibly pushdown automata
and visibly pushdown languages ($\operatorname{VPLang}$) but also give here
the main definitions. More precisely, a pushdown alphabet $\widetilde{\Sigma}$
is a triple $(\Sigma_{c},\Sigma_{i},\Sigma_{r})$ of pairwise-disjoint
alphabets known as the call, internal and return alphabets respectively. A
visibly pushdown automaton (VPA) is a pushdown automaton for which the stack
operations (i.e. whether a push, pop or neither is performed) are determined
by the input symbol which is read. In particular, any transition for which the
input symbol $a$ belongs to the call alphabet $\Sigma_{c}$, must push a symbol
to the stack while any transition for which $a\in\Sigma_{r}$ must pop a symbol
from the stack unless the stack is empty and any transition for which
$a\in\Sigma_{i}$ must leave the stack unchanged. Acceptance of a word is
determined by the state the automaton is in after reading the whole word. The
stack does not need to be empty for a word to be accepted. A
$\widetilde{\Sigma}$-visibly pushdown language is the set of words accepted by
a visibly pushdown automaton with pushdown alphabet $\widetilde{\Sigma}$. A
language $L$ is a visibly pushdown language (and is part of the class
$\operatorname{VPLang}$) if there exists a pushdown alphabet
$\widetilde{\Sigma}$ such that $L$ is a $\widetilde{\Sigma}$-visibly pushdown
language. The class $\operatorname{VPLang}$ is a strict superset of the class
of regular languages and a strict subset of the class of deterministic
context-free languages, which retains many of the nice decidability and
closure properties of regular languages. In particular, it is shown in [3]
that $\operatorname{VPLang}$ is closed under union, intersection and
complement and moreover that the emptiness, universality, inclusion and
equivalence probelms are all decidable for $\operatorname{VPLang}$.

By a theory, we mean a set $\mathfrak{T}=\\{f_{1},f_{2},\ldots\\}$ of formulas
adhering to given syntax and to which we associate a particular semantics. The
theories we consider (introduced in Section 3) consist of quantifier-free
formulas. The typical computational questions one might consider with respect
to a given theory $\mathfrak{T}$ are Satisfiability: given formula
$f\in\mathfrak{T}$, does there exist an assignment of the variables in $f$
such that $f$ becomes true under the associated semantics? and Validity: given
formula $f\in\mathfrak{T}$, is $f$ true under all assignments of the variables
occurring in $f$?

The questions we address have a slightly different flavour: given formula
$f\in\mathfrak{T}$ and variable $x$ occurring in $f$, we are interested in
properties of the set of all values $w$ for which there is an assignment
mapping $x$ to $w$ which makes the formula true. Thus, we consider the set of
concrete values $w$ for which $f$ remains satisfiable once the variable $x$
has been replaced by $w$. Since we shall focus on theories in which variables
represent words, we refer to the set of all such values $w$ as the language
expressed by the variable $x$ in the formula $f$. In this respect, we extend
the notion of languages expressible by word equations [27] to arbitrary
string-based logical theories. We say a language $L$ is expressed  by a
formula if it contains a variable $x$ such that $L$ is the language expressed
by $x$ in $f$. We say that $L$ is expressible in a theory $\mathfrak{T}$ if
there exists a formula $f\in\mathfrak{T}$ and variable $x$ occurring in $f$
such that $L$ is expressed by $x$ in $f$.

We shall consider typical decision problems such as emptiness and universality
for languages expressed by formulas in a given theory $\mathfrak{T}$. In this
context, the input is a formula $f\in\mathfrak{T}$ and a variable $x$
occurring in $f$. So, e.g, in the case of emptiness, we might be given a
formula $x=aba\land x\cdot y=ababba$ along with the variable $y$, and we must
decide whether the language $L_{y}$ expressed by $y$ in that formula is the
empty set or not. In this case, $L_{y}=\\{bba\\}\not=\emptyset$ so the answer
is no. Clearly, for any formula $f$ and variable $x$, the emptiness problem
for the language expressed by $x$ in $f$ is equivalent to the satisfiability
problem for $f$. Thus, we consider a set of problems which directly generalise
the satisfiability problem.

For theories containing word equations, we shall use notions and results from
[27] to reason about (in)expressibility of languages, such as the notion of a
synchronising $\mathfrak{F}$-factorisation.

######  Definition 2.1 ([27]).

Let $\mathfrak{F}$ be a property of words. An $\mathfrak{F}$-factorisation of
a word $w$ is a factorisation $w=w_{1}\ldots w_{n}$ such that each $w_{i}$ has
the property $\mathfrak{F}$. Moreover $\mathfrak{F}$ is synchronising if every
word has exactly one $\mathfrak{F}$-factorisation and additionally there exist
$l,r\in\mathbb{N}$ such that for any words $x,y$ with
$\mathfrak{F}$-factorisations $x=x_{1}x_{2}\ldots x_{s}$ and
$y=y_{1}y_{2}\ldots y_{k}$ where $k>l+r$ and $y$ is a factor of $x$, the
following hold:

  1. 1.

there exist $l^{\prime}\leq l,r^{\prime}\leq r$ and $p,q$ with $1\leq p\leq
q\leq s$ such that $q-1-p=k-r^{\prime}-l^{\prime}$ and
$x_{p}=y_{l^{\prime}+1}$, $x_{p+1}=y_{l^{\prime}+1}$…
$x_{q}=y_{k-r^{\prime}+1}$;

  2. 2.

$y_{1}y_{2}\ldots y_{l^{\prime}}$ is a suffix of $x_{\max(1,p-l)}\ldots
x_{p-1}$;

  3. 3.

$y_{k-r^{\prime}+1}\ldots y_{k}$ is a prefix of $x_{q}\ldots
x_{\min(s,q+r-1)}$.

Intuitively, $\mathfrak{F}$ is synchronising for some parameters $l,r$ if the
$\mathfrak{F}$-factorisations of a word $x$ and a factor $y$ of $x$
synchronise (or coincide) except for the first $l$ parts and the last $r$
parts.

######  Remark 2.2.

[27] provides several examples of synchronising factorisations, including
splitting a word into blocks of a single letter which is clearly
synchronising.

##  3 Logical Theories Over Strings Constraints

In this section, we introduce a variety of logical theories encompassing the
most common kinds of string constraints (as overviewed in [6]). We define
three sets of terms as follows. Let $\mathcal{X}=\\{x_{1},x_{2},\ldots\\}$ be
an infinite set of string variables. Let $\Sigma$ be a finite alphabet. Let
$\mathcal{T}_{str}^{\Sigma}=\mathcal{X}\cup\Sigma^{*}$ be the set of basic
string terms. Let $\mathcal{T}_{str,con}^{\Sigma}=(\mathcal{X}\cup\Sigma)^{*}$
be the set of extended string terms. Note that
$\mathcal{T}_{str,con}^{\Sigma}$ is the closure of
$\mathcal{T}_{str}^{\Sigma}$ under the concatenation $(\cdot)$ operation. Let
$\mathcal{T}_{arith}^{\Sigma}=\\{k_{0}+k_{1}|s_{1}|+k_{2}|s_{2}|+\ldots+k_{n}|s_{n}|\mid
n\in\mathbb{N}_{0},k_{i}\in\mathbb{Z},\text{ and
}s_{i}\in\mathcal{T}_{str}^{\Sigma}\\}$ be the set of length terms. We
interpret $|s|$ as the length of the string term $s$, so
$\mathcal{T}_{arith}^{\Sigma}$ is the set of linear combinations of lengths of
string terms. Note that since we can express the length of a concatenation of
string terms as a linear combination of lengths of basic string terms, it is
no restriction that $s_{i}\in\mathcal{T}_{str}^{\Sigma}$ rather than
$\mathcal{T}_{str,con}^{\Sigma}$ (this allows us to consider theories
containing length terms both with and without concatenation). We construct
three types of atoms from terms as follows:

(A1) Language membership constraints of the form $s\in L$ where
$s\in\mathcal{T}_{str(,con)}^{\Sigma}$ and $L\subseteq\Sigma^{*}$ is a formal
language,
(A2) Length constraints of the form $\ell_{1}=\ell_{2}$ where
$\ell_{1},\ell_{2}\in\mathcal{T}_{arith}^{\Sigma}$,
(A3) Word equations (string-equality constraints) of the form $s_{1}=s_{2}$
where $s_{1},s_{2}\in\mathcal{T}_{str,con}^{\Sigma}$.

Formulas in our theories are constructed in general as follows:
(F1) Any atom is a well-formed formula,
(F2) If $f_{1},f_{2}$ are well-formed formulas then $\neg f_{1}$ is a well-
formed formula and $f_{1}\oplus f_{2}$ is a well-formed formula for each
$\oplus\in\\{\land,\lor,\implies,\iff\\}$.

Note that all formulas are quantifier-free. The semantics associated with
these formulas are defined in the natural way: given a substitution for the
variables $x_{1},x_{2},\ldots$ for words in $\Sigma^{*}$, each string term
evaluates to a word in $\Sigma^{*}$ (possibly as the result of concatenating
several smaller words in the case of extended string terms). Each length term
is a linear combination of lengths of strings and evaluates to an integer.
Atoms of type A1 evaluate to “true” if the string term $s$ evaluates to a word
in the language $L$ and false otherwise. Atoms of type A2 evaluate to true if
the two length terms $\ell_{1},\ell_{2}$ evaluate to the same integer and
false otherwise. Atoms of type A3 evaluate to true if the string terms $s_{1}$
and $s_{2}$ evaluate to the same word and false otherwise. Finally, Boolean
combinations of the form F2 are evaluated in the canonical way.

The most general logical theory we consider includes all of the above and we
consider language membership constraints $s\in L$ where $L$ is a deterministic
context-free language, given e.g. as a deterministic push-down automaton or a
context-free grammar. However, we are not just interested in this theory
alone, rather we want to consider various sub-theories in order to compare
their expressive power and computability-related properties.

We have two ways of restricting expressive power. The first is to restrict the
types of terms/atoms we allow, while the second is to restrict the kind of
languages we allow in the language membership constraints (atoms of type A1).
For the latter, we focus on three main possibilities: regular languages,
visibly push-down languages, and deterministic context-free languages. For
technical completeness, we can assume that all language constraints are given
as automata (NFA, Visibly-PDA, or Deterministic-PDA respectively), however,
since we do not focus on precise complexity-related issues, equivalent
language descriptors such as grammars could equally be used. In particular, we
might use simpler descriptors where convenient to do so and where it is
obvious that an equivalent automaton could be constructed.

We consider all combinations of atom-types A1, A2 and A3, and in each case
define versions in which only basic string terms from
$\mathcal{T}_{str}^{\Sigma}$ are allowed and versions in which concatenations
of string terms (i.e. terms from $\mathcal{T}_{str,con}^{\Sigma}$) are
allowed. Note that whenever we allow word equations (so, atoms of type A3), we
might as well allow concatenations of string terms. If we allow concatenations
in word equation terms, then we can model concatenation in all string terms
anyway and if we were to restrict equality between string terms to basic
string terms only, then we could easily eliminate all string equalities by
direct substitution.

Moreover, we are not going to consider explicitly the case that only length
constraints (atoms of type A2) are allowed, since this reduces to the
existential fragment of Presburger arithmetic and is therefore not really a
string-based logic. With these exclusions, we are left with a total of 20
theories to consider. In fact, since the theories themselves depend on the
underlying alphabet $\Sigma$, we have 20 families of theories. As such, it is
convenient to introduce a naming convention for these (families of) theories.

If atoms of type A1 are allowed, we add either $\operatorname{REG}$,
$\operatorname{VPL}$, or $\operatorname{DCF}$ to the name of the theory-family
depending on the class of languages permitted: $\operatorname{REGLang}$,
$\operatorname{VPLang}$, or $\operatorname{DCFLang}$, respectively. If atoms
of type A2 are allowed, we add the abbreviation $\operatorname{LEN}$,
separated if necessary by a "$\operatorname{+}$". Likewise, if atoms of type
A3 are allowed, we add the abbreviation $\operatorname{WE}$. Finally, if atoms
of type A3 are not allowed, but extended string terms are (so we have
concatenation but not equality between string terms), then we add the
abbreviation $\operatorname{CON}$. Note that $\operatorname{CON}$ is
superseded by $\operatorname{WE}$ due to reasons explained above. For example,
the most general theory which allows all three atom types (with deterministic
context-free languages for atoms of type A1) is denoted by
$\operatorname{WE}\operatorname{+}\operatorname{DCF}\operatorname{+}\operatorname{LEN}$.
Similarly,
$\operatorname{REG}\operatorname{+}\operatorname{LEN}\operatorname{+}\operatorname{CON}$
describes the theory in which atoms of type A1 (where $L$ is a regular
language and $s$ is an extended string term) and A2 are allowed.

For theories allowing $\operatorname{VPLang}$ membership constraints (i.e.
belonging to families of the form $\operatorname{VPL}+\ldots$), we assume a
fixed partition of the alphabet $\Sigma$ into the call, return and internal
alphabets $\Sigma_{c},\Sigma_{r},\Sigma_{i}$. We conclude this section with
the following remark.

######  Remark 3.1.

Since $\operatorname{REGLang}$ (respectively, $\operatorname{VPLang}$) is
closed under union, intersection and complement, the set of languages
expressible in $\operatorname{REG}$ (respectively, $\operatorname{VPL}$) is
exactly $\operatorname{REGLang}$ (respectively, $\operatorname{VPLang}$).
However, the same is not true for $\operatorname{DCF}$ and
$\operatorname{DCFLang}$, since that class is not closed e.g. under
intersection. For $\operatorname{DCF}$ the expressible languages are exactly
the Boolean closure of the deterministic context-free languages. Moreover, it
can be inferred from well-known results on word equations (see e.g. [27, 33])
that the languages expressed by $\operatorname{WE}$ are exactly those
expressible by a single word equation in the sense of [27].

##  4 Separation and Grouping of Theories

Figure 1: Visual representations of all 20 families of string-based logical
theories considered. Theory-families are depicted in solid square boxes
containing their names (see Section 3). Dashed square-boxes around multiple
theory-families show equivalence w.r.t. the class of expressible languages (so
equivalence under $\sim$). The arrows between theory-families and their
transitive closure represent inclusion w.r.t. the class of expressible
languages. Solid arrows indicate that the inclusion is known to be strict,
while dashed arrows indicate that we do not know whether the inclusion is
strict or not. The most expressive group of theories (i.e. those equivalent to
$\operatorname{VPL}\operatorname{+}\operatorname{CON}$) are able to express
$\operatorname{RE}$. The left figure indicates for which (families of)
theories the emptiness and finiteness problems are decidable or undecidable.
Our contribution includes undecidability for
$\operatorname{VPL}\operatorname{+}\operatorname{CON}$. This is a particularly
interesting case because it is only a slight generalisation of important cases
which remain open, namely
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$
and $\operatorname{WE}\operatorname{+}\operatorname{LEN}$ (shaded). We also
show decidability for $\operatorname{VPL}\operatorname{+}\operatorname{LEN}$,
$\operatorname{REG}\operatorname{+}\operatorname{CON}\operatorname{+}\operatorname{LEN}$
etc. by showing equivalence to families for which decidability is known
($\operatorname{REG}$ and $\operatorname{VPL}$). The right figure depictes
(families) of theories for which the universality ($=\Sigma^{*}$) and subset-
universality ($=S^{*}$) problems are decidable/undecidable. Equivalence and
inclusion (where the two languages might come from different theories) are
decidable if and only if both theories fall into cases where universality
($=\Sigma^{*}$) decidable.

We are interested primarily in whether we can decide properties of a language
expressed by a given formula and variable. Therefore, the first thing we
consider is the relative expressive power of the various theories defined in
the previous section. In particular, we want to understand how the classes of
languages which may be expressed by a formula/variable from a given theory
relate to each other. To make these comparisons formally, we define the
following relation(s) on two logical theories
$\mathfrak{T}_{1},\mathfrak{T}_{2}$ whose formulas contain string variables.

######  Definition 4.1.

Let $\mathfrak{T}_{1},\mathfrak{T}_{2}$ be theories whose formulas contain
string-variables. We say that $\mathfrak{T}_{1}\preceq\mathfrak{T}_{2}$ if,
for every formula $f\in\mathfrak{T}_{1}$ and every (string) variable $x$
occurring in $f$, there exists a formula $f^{\prime}\in\mathfrak{T}_{2}$ and
variable $x^{\prime}$ in $f^{\prime}$ such that the languages expressed by $x$
in $f$ and $x^{\prime}$ in $f^{\prime}$ are identical. Moreover, we say that
$\mathfrak{T}_{1}\sim\mathfrak{T}_{2}$ if both
$\mathfrak{T}_{1}\preceq\mathfrak{T}_{2}$ and
$\mathfrak{T}_{2}\preceq\mathfrak{T}_{1}$ hold. We write
$\mathfrak{T}_{1}\prec\mathfrak{T}_{2}$ if
$\mathfrak{T}_{1}\preceq\mathfrak{T}_{2}$ and
$\mathfrak{T}_{1}\not\sim\mathfrak{T}_{2}$.

Hence, $\mathfrak{T}_{1}\preceq\mathfrak{T}_{2}$ if the class of languages
expressible in $\mathfrak{T}_{1}$ is a subset of the class of languages
expressible in $\mathfrak{T}_{2}$, and $\mathfrak{T}_{1}\sim\mathfrak{T}_{2}$
if the two classes are equal. Note that the relation $\sim$ is an equivalence
relation that is a weaker notion of equivalence than being isomorphic. That
is, two theories need not be isomorphic to satisfy the equivalence $\sim$.

We extend Definition 4.1 for the families of theories defined in Section 3 as
follows. Recall that each family contains all the theories consisting of a
particular set of formulas, but whose underlying alphabet $\Sigma$ may vary.

######  Definition 4.2.

Let $\mathfrak{F}_{1},\mathfrak{F}_{2}$ be families of theories as defined in
Section 3. We say that $\mathfrak{F}_{1}\preceq\mathfrak{F}_{2}$ if, for every
theory $\mathfrak{T}_{1}\in\mathfrak{F}_{1}$, there is a theory
$\mathfrak{T}_{2}\in\mathfrak{F}_{2}$ such that
$\mathfrak{T}_{1}\preceq\mathfrak{T}_{2}$. The relations $\sim$ and $\prec$
are then defined analogously,

Before moving on, let us make some remarks. It will often be the case that
there exist formulas such that the language expressed by a variable $x$
occurring in both formulas is the same, but the sets of satisfying
assignments, when considered as a whole, are not identical (see Remark 4.3
below). This has an important implication for what conclusions we can and
cannot draw from a statement of the form e.g.
$\mathfrak{T}_{1}\sim\mathfrak{T}_{2}$. E.g., while we will later show that
$\operatorname{REG}\sim\operatorname{REG}\operatorname{+}\operatorname{LEN}$,
this does not imply that
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}\sim\operatorname{WE}\operatorname{+}\operatorname{REG}$.
Indeed we shall also show explicitly that the latter does not hold.

######  Remark 4.3.

Consider the $\operatorname{LEN}$ formula $|x|=2|y|$ where $x,y$ are string
variables. Then the language expressed by $x$ is the set of all even-length
words over the underlying alphabet $\Sigma$, and the language expressed by $y$
is simply $\Sigma^{*}$. Both of these languages are regular, and can be
expressed in $\operatorname{REG}$. However, if we were to consider e.g. a
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ formula
$x=yyy\land|x|=2|y|$, then we cannot replace the condition $|x|=2|y|$ with
constraints based on the aforementioned regular languages. The problem with
doing so would be that it allows us to decouple the sets of values for $x$ and
$y$ satisfying the length constraint (so we get an $x$, $y$, $x^{\prime}$,
$y^{\prime}$ such that $|x|=|y^{\prime}|$ and $|x^{\prime}|=|y|$ and $x=yyy$
holds, but where $x^{\prime}$ might be different from $x$ and $y^{\prime}$
might be different from $y$.

In [27] the authors consider expressibility of languages (and relations) by
word equations and show that a language is expressible by $\operatorname{WE}$
if and only if it is expressible by a single word equation. The authors of
[27] also show that, for $\Sigma\supseteq\\{a,b,c\\}$, the regular language
$\\{a,b\\}^{*}$ is not expressible by a single word equation, and thus not in
$\operatorname{WE}$. The same holds for the language $\\{a^{n}b^{n}\mid
n\in\mathbb{N}_{0}\\}$. Since these languages are clearly expressible in
$\operatorname{WE}+\operatorname{REG}$ and
$\operatorname{WE}+\operatorname{LEN}$ respectively, we may immediately
conclude the following.

######  Theorem 4.4 ([27]).

The following hold:
$\operatorname{WE}\,\prec\,\operatorname{WE}\operatorname{+}\operatorname{REG}$
and
$\operatorname{WE}\,\prec\,\operatorname{WE}\operatorname{+}\operatorname{LEN}$.

On the one hand, all languages expressed in our theories are clearly
recursively enumerable. On the other hand, in our first main result, we show
that, in fact, all recursively enumerable languages can be expressed with only
concatenation and $\operatorname{VPL}$-membership.

######  Theorem 4.5.

The class of languages expressible in the familiy
$\operatorname{VPL}\operatorname{+}\operatorname{CON}$ is exactly
$\operatorname{RE}$.

######  Proof 4.6.

Let $L\subset\Sigma^{*}$ be a recursively enumerable language. It is not hard
to show that there exists a 1-Tape deterministic Turing machine $M$ accepting
$L$, which additionally has the following properties:

  * •

$M$ has the set of states $Q$, including a final state $q_{f}$ and an initial
state $q_{0}$, the input alphabet $\Sigma$, the working alphabet $\Gamma$
which includes $\Sigma$ as well as the blank symbol $B$ and a special
delimiter-symbol $\$$. The transition function of $M$ is
$\delta:Q\times\Gamma\operatorname{\rightarrow}Q\times(\Gamma\setminus\\{B\\})\times\\{R,L\\}$
(where $R$ and $L$ are symbols denoting a left and, respectively, right
movement of the tape-head of $M$).

  * •

$M$ has a semi-infinite tape (bounded to the left). We assume that the
delimiter-symbol $\$$ marks the left end of the tape.

  * •

$M$ accepts the input word or goes in an infinite loop. Moreover, $M$ accepts
only after making at least one step, and in the last (i.e., accepting)
configuration the tape-head scans the leftmost blank cell of the tape, and the
state of $M$ is $q_{f}$.

  * •

The delimiter $\$$ cannot be modified, and $\$$ cannot be written on any other
cell of the tape, than the leftmost one (i.e., at a certain step, $M$ can only
write $\$$ in the cell that already contains $\$$).

  * •

In the initial configuration of $M$, the tape-head scans the cell containing
the delimiter $\$$.

The configurations of $M$ (i.e., snapshots of the tape of $M$ during the
computation) are described by strings $u(q,a)vB^{k}$, where $a\in\Gamma$,
$uv\in\$(\Gamma\setminus\\{B\\})^{*}$ such that $uavB^{\omega}$ is the the
current content of the tape of the machine (where $B^{\omega}$ means a right-
infinite string containing only blanks), $q$ is the current state of the
machine, the tape-head scans the cell containing $a$, and $k\geq 1$. Note that
$uavB^{k}$ is a prefix of the content of the tape, read left to right,
including one or more $B$ symbols. Note also that the pairs $(q,a)$, for all
$q\in Q$ and $a\in\Gamma$, will be part of the call-alphabet for the VPAs we
construct in the rest of the proof. At this point, it is very important to
remark that there might be more than one string describing the same
configuration of the machine.

Now, given $C_{1}$ and $C_{2}$ two strings describing configurations of $M$,
we say that there is a transition from $C_{1}$ to $C_{2}$, denoted
$C_{1}\vdash C_{2}$, if $C_{2}$ is a string describing the configuration in
which $M$ transitions from the configuration described by $C_{1}$ and,
moreover, $|C_{1}|=|C_{2}|$.

Indeed, as the strings encoding configurations contain an arbitrary large
number of blank symbols, if $C$ describes a configuration of $M$ reachable in
a finite, greater or equal to one number of steps by $M$ on the input $w$,
then there exists a sequence of strings $C_{0},\ldots,C_{k}$ describing
configurations of $M$ such that $C_{0}$ describes the initial configuration of
$M$ for the input $w$ and $C_{0}\vdash C_{1}\vdash\ldots\vdash C_{k}=C$
(meaning that $|C_{i}|=|C_{j}|$ for all $i,j\in\\{0,\ldots,k\\}$, as well).
Intuitively, $C_{0}$ already contains all the blanks which will be scanned by
the tape-head during the computation of $M$ on $w$, until $C$ is reached.

A direct consequence of the observation made above is that if $C$ is a string
which describes the final configuration of $M$ for the input $w\in L$, then
there exists a sequence of strings $C_{0},\ldots,C_{k}$ describing
configurations of $M$ such that $C_{0}$ describes the initial configuration of
$M$ for the input $w$ and $C_{0}\vdash C_{1}\vdash\ldots\vdash C_{k}=C$. This
also means that $|C_{i}|=|C_{j}|$ for all $i,j\in\\{0,\ldots,k\\}$. So, an
accepting computation of $M$ can be described by a sequence of strings
encoding configurations, all having the same length. This length equality
between the Turing machine’s configurations in our setting is a point of the
novelty in our proof, and it is crucial for the ”simulation" of its
computations by visibly pushdown automata.

We now define an alphabet $\widetilde{\Delta}$ as the triple
$(\Delta_{c},\Delta_{i},\Delta_{r})$ of pairwise-disjoint alphabets, which
stand for the call, internal and return alphabets, respectively, for the VPAs
which we will construct from now on. We define
$\Delta_{c}=\Gamma\cup\\{\\#,@\\}\cup\\{(q,a)\mid q\in Q,a\in\Gamma\\}$ and
$\Delta_{r}=\\{a^{\prime}\mid a\in\Delta_{c}\\}$; that is, $\Delta_{r}$
consists in copies of the letters of the alphabet $\Delta_{c}$. Finally,
$\Delta_{i}=\\{\blacksquare\\}$. Let
$f:\Delta_{c}^{*}\operatorname{\rightarrow}\Delta_{r}^{*}$ be the antimorphism
defined by $f(a)=a^{\prime}$ for all $a\in\Delta_{c}$ (here antimorphism means
that $f(wu)=f(u)f(w)$ for all $u,w\in\Delta_{c}^{*}$).

Let us now define the language

$L_{1}=\\{@C_{1}\\#C_{2}\\#\cdots\\#C_{k}\\#\blacksquare\\#^{\prime}C^{\prime}_{k}\\#^{\prime}\cdots\\#^{\prime}C^{\prime}_{1}@^{\prime}\\}$

where:

  * •

For $i\leq k-1$, $C_{i}$ is a configuration of $M$ and
$C^{\prime}_{i}=f(D_{i})$, where $C_{i}\vdash D_{i}$. In other words,
$C^{\prime}_{i}$ is the image under $f$ of the string describing the
configuration which follows the configuration described by $C_{i}$ in a
computation of $M$.

  * •

$C_{k}$ describes a final configuration of $M$, and we have that $D_{k}=C_{k}$
and $C^{\prime}_{k}=f(C_{k})$.

We can show that $L_{1}$ is accepted by a nondeterministic VPA $E$. This VPA
functions according to the following algorithm.

  1. 1.

$E$ uses a stack, which is represented as a word and the top of the stack is
the rightmost symbol of the respective word.

  2. 2.

In the first move, $E$ reads $@$ and writes $@^{\prime}$ on the stack.

  3. 3.

$E$ computes and writes the strings $D_{1}\\#$, $\ldots$, $D_{k}\\#$ on the
stack (by pushing the symbols of these strings in order left to right), while
reading the strings $C_{1}\\#,$ $\ldots$, $\\#C_{k}\\#$, respectively. Then
$E$ checks whether $f(D_{1}\\#\cdots
D_{k}\\#)=\\#^{\prime}C^{\prime}_{k}\\#^{\prime}\cdots\\#^{\prime}C^{\prime}_{1}$
by iteratively popping a symbol from the top of the stack if and only if it
matches the current symbol read on the input tape. $E$ accepts the input if,
when the input tape was completely read, the stack is empty (this can be
checked using the fact that the last symbol popped must be $@^{\prime}$).

  4. 4.

When reading any of the strings $C_{i}=u(q,a)vB^{k}$ (which basically occurs
either at the very beginning of the computation or after reading a $\\#$
symbol) the automaton $E$ works as follows:

     * •

$E$ non-deterministically guesses if $C_{i}$ is the final configuration. If
$C_{i}$ is the final configuration, then $E$ reads the symbols $d$ of $C_{i}$
and pushes $d^{\prime}$ on the stack, until it reaches a symbol $(q,B)$. If
$q$ is not final or $E$ met a $B$ symbol before reaching $(q,B)$, then $E$
goes into an error state. Otherwise, it writes $(q,B)^{\prime}$ on the stack.
It then reads the remaining $B$ symbols and $\\#$ and pushes corresponding
$B^{\prime}$ symbols and $\\#^{\prime}$, respectively, in the stack. Then it
checks if $\blacksquare$ follows on the input tape. If yes, it simply switches
to the part where symbols are popped from the stack. If not, then $E$ goes to
an error state. If $C_{i}$ is not a final configuration, then the following
computation is implemented.

     * •

$E$ non-deterministically chooses the transition that $M$ makes in this
configuration, and keeps track of this choice in the state.

     * •

Assume first that the respective transition is $\delta(q,a)=(q_{1},b,L)$. This
means that $u$ is non-empty. In this case, $E$ reads the symbols
$d\in\Gamma\setminus\\{B\\}$ of $C_{i}$ and pushes $d^{\prime}$ on the stack,
until it non-deterministically decides that it has reached the last symbol $c$
of $u$. It then reads $c$ and pushes $(q_{1},c)^{\prime}$ on the stack. The
next symbol read on the tape should now be $(q,a)$; otherwise $E$ goes in an
error state. If $E$ reads $(q,a)$, it pushes $b^{\prime}$ on the stack, and it
then continues reading the symbols $d$ of $C_{i}$ and pushing $d^{\prime}$ on
the stack, until it reaches $\\#$. It then reads $\\#$, pushes $\\#^{\prime}$
on the stack, and moves to the next configuration.

     * •

Assume now that the respective transition is $\delta(q,a)=(q_{1},b,R)$. In
this case, $E$ reads the symbols $d$ of $C_{i}$ and pushes $d^{\prime}$ on the
stack, until it reads the symbol $(q,a)$; otherwise, if it goes all the way to
the first $B$ symbol without finding $(q,a)$, $E$ goes into an error state.
Now, if $E$ reads $(q,a)$, it pushes $b$ on the stack. Then, $E$ reads the
next symbol on the tape. If this symbol is $\\#$, then $E$ goes into an error
state (intuitively, we cannot compute $D_{i}$ because it is longer than
$C_{i}$). Otherwise, if this symbol is $d\neq\\#$, then $E$ writes
$(q_{1},d)^{\prime}$ on the stack. Further, $E$ continues reading the symbols
$e$ of $C_{i}$ and pushing $e^{\prime}$ on the stack, until it reaches $\\#$.
It then reads $\\#$, pushes $\\#^{\prime}$ on the stack, and moves to the next
configuration.

It is not hard to see that $E$ accepts $L_{1}$.

Intuitively, $E$ accepts those strings consisting in correctly matched (in a
palindromic fashion) pairs of consecutive configurations of the Turing machine
$M$. Very importantly, there is no connection between different pairs of
matching configurations. This type of connection, ultimately leading to a way
of expressing the valid computations of $M$, is something that we now need to
achieve.

To the end, we define $L_{2}=\\{w\blacksquare f(w)\mid x\in\Delta_{c}\\}$. It
is immediate that $L_{2}$ can be accepted by a VPA. Similarly, all regular
languages can be accepted by VPAs (as
$\operatorname{REGLang}\subseteq\operatorname{VPLang}$).

So, to achieve our goal, we define the following formula
$\phi=(x\in\Sigma^{*})\land(v\in\\{B\\}^{+})\land(z\in(\Delta_{r}\setminus\\{\\#^{\prime}\\})^{*})\land(@(q_{0},\$)xv\\#y\blacksquare\\#^{\prime}z\\#u@^{\prime}\in
L_{1})\land(y\blacksquare\\#u\in L_{2})$.

We claim that the language expressed by $x$ is $L$.

Firstly, from
$@(q_{0},\$)xv\\#y\blacksquare\\#^{\prime}z\\#^{\prime}u@^{\prime}\in L_{1}$
we get that

$@(q_{0},\$)xv\\#y\blacksquare\\#^{\prime}z\\#^{\prime}u@^{\prime}=@C_{1}\\#C_{2}\\#...\\#C_{k}\\#\blacksquare\\#^{\prime}C^{\prime}_{k}\\#^{\prime}....\\#^{\prime}C^{\prime}_{1}@^{\prime},$

for some configurations $C_{1},\ldots,C_{k}$. Moreover, $C_{1}$ starts with
$(q_{0},\$)$ and $x$ is the string contained between $(q_{0},\$)$ and the
first occurrence of $B$ in $C_{1}$, so $C_{1}$ must be an initial
configuration of $M$ from which $x$ extracts the input string. Also,
$y=C_{2}\\#\cdots C_{k}\\#$. Finally, we obtain that $z=C^{\prime}_{k}$ and
$u=C^{\prime}_{k-1}\\#^{\prime}\cdots\\#^{\prime}C^{\prime}_{1}$.

Secondly, from $y\blacksquare\\#^{\prime}u\in L_{2}$, we get that
$C^{\prime}_{i-1}=f(C_{i})$, for all $i\in\\{2,\ldots,k\\}$. This means that
$C_{i-1}\vdash C_{i}$, for all $i\in\\{2,\ldots,k\\}$. Therefore,
$C_{1}\vdash\ldots\vdash C_{k}$ is an accepting computation of $M$. In
conclusion, the word expressed by $x$ is in $L$.

The converse implication is immediate. If $w\in L$, then there exists a
sequence of strings $C_{0},\ldots,C_{k}$ (all having the same length)
describing configurations of $M$ such that $C_{0}$ describes an initial
configuration of $M$ for the input $w$, $C_{k}$ describes a final
configuration, and $C_{0}\vdash C_{1}\vdash\ldots\vdash C_{k}$. From this, we
can easily derive an assignment of the string variables $v,z,y,u$ with $x=w$
for which $\phi$ is satisfiable.

Our claim now follows, and we have shown that any recursively enumerable
language can be expressed in
$\operatorname{VPL}\operatorname{+}\operatorname{CON}$.

Consequently, the class of languages expressible in each of
$\operatorname{VPL}\operatorname{+}\operatorname{CON}\operatorname{+}\operatorname{LEN}$,
$\operatorname{WE}\operatorname{+}\operatorname{VPL}$,
$\operatorname{WE}\operatorname{+}\operatorname{VPL}\operatorname{+}\operatorname{LEN}$,
$\operatorname{DCF}\operatorname{+}\operatorname{CON}$,
$\operatorname{DCF}\operatorname{+}\operatorname{CON}\operatorname{+}\operatorname{LEN}$,
$\operatorname{WE}\operatorname{+}\operatorname{DCF}$, and
$\operatorname{WE}\operatorname{+}\operatorname{DCF}\operatorname{+}\operatorname{LEN}$
is the class of recursively enumerable languages $\operatorname{RE}$. Thus,
all these theories are equivalent under $\sim$.

We therefore get a natural hierarchy of theories which extend the syntax and
expressive power of $\operatorname{WE}$,
$\operatorname{WE}\operatorname{+}\operatorname{REG}$, and
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$. Next, we show some
cases where this hierarchy does not collapse by providing some
inexpressibility results.

We need the following technical lemma, which non-trivially extends a similar
one from [27] to accommodate the addition of other types of constraints to
word equations.

######  Lemma 4.7.

Let $\mathfrak{F}$ be a property on words defining a synchronising
factorisation.

Let $\mathfrak{T}$ be a theory belonging to
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ or to
$\operatorname{WE}\operatorname{+}\operatorname{REG}$, and let $f$ be a
formula from $\mathfrak{T}$ and $x$ a variable occurring in $f$. Suppose that
$w$ belongs to the language $L$ expressed by $x$ in $f$ and let
$w=w_{1}w_{2}\ldots w_{n}$ be its $\mathfrak{F}$-factorisation. Then, the
following holds:
(1) if $\mathfrak{T}$ belongs to
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$, there exists
$d\in\mathbb{N}$ such that if the number of distinct factors $w_{i}$ is
greater than $d$, then there exists at least one $i$ such that, for every word
$u$ with $|u|=|w_{i}|$, the word $w^{\prime}$ obtained by replacing each
occurrence of $w_{i}$ in $w$ with $u$ also belongs to $L$;
(2) if $\mathfrak{T}$ belongs to
$\operatorname{WE}\operatorname{+}\operatorname{REG}$, there exist
$d,e\in\mathbb{N}$ such that if the number of distinct factors $w_{i}$ with
$|w_{i}|>e$ is greater than $d$, then there exists at least one $i$ and a word
$u$ with $|u|<|w_{i}|$ such that the word $w^{\prime}$ obtained by replacing
each occurrence of $w_{i}$ in $w$ with $u$ also belongs to $L$.

######  Proof 4.8.

Proof of Part (1): Firstly, we write the formula $f$ in Disjunctive Normal
Form (DNF). We can then separate each clause into conjunctions of word
equation literals and length constraint literals. By canonical constructions
(see e.g. [27]), we can replace the word equation literals with a single word
equation atom (i.e. a positive occurrence of a word equation) without
affecting the language expressed by $x$. Thus the language expressed by $x$ is
a finite union of languages, each given by the solutions to a single word
equation which adhere to the length constraint literals (projected onto the
variable $x$).

Suppose that $w\in L$. Then we must have that $w$ is the value of $x$ of some
solution to one of the word equations corresponding to one of the DNF clauses
as described above.

The proof of Theorem 16 in [27] directly establishes the fact that under the
conditions of the lemma, we may replace all occurrences of some $w_{i}$
consistently with any other word $u$ and still have a solution to the word
equation. By ensuring that we swap $w_{i}$ for a word $u$ of the same length,
we ensure that the new solution satisfies the length constraints whenever the
old one does. It follows that the new word also belongs to $L$ so the
statement of the lemma holds.

Proof of Part (2): This is the more complicated part of this proof. Just like
in the previous case, we start by writing the formula $f$ in Disjunctive
Normal Form (DNF). We can then separate each clause into conjunctions of word
equation literals and regular language membership literals. By closure
properties of regular languages, we can remove negations of regular language
membership constraints and by canonical constructions (see e.g. [27]), we can
replace the word equation literals with a single word equation atom (i.e. a
positive occurrence of a word equation) without affecting the language
expressed by $x$. Thus the language expressed by $x$ is a finite union of
languages, each given by the solutions to a single word equation which adhere
to the (positive) regular language membership constraints (and projected onto
the variable $x$).

Suppose that $w\in L$ satisfies the conditions of the lemma. Then we must have
that $w$ is the value of $x$ of some solution to one of the word equations
corresponding to one of the DNF clauses as described above. Let
$x_{1},x_{2},\ldots,x_{m}$ be the variables occurring in that clause, and for
each $j,1\leq j\leq m$, let $A_{j}$ be the minimal DFAs describing the
intersection of all regular language membership constraints acting on the
variable $x_{j}$ and let $Q_{j}$ be the set of states of $A_{j}$. For $1\leq
j\leq m$, let $w_{j}=w_{j,1}w_{j,2}\ldots w_{j,k_{j}}$ be the
$\mathfrak{F}$-factorisation of the value of $x_{j}$ in the aforementioned
solution from which we get $w$.

Now, the proof of Theorem 16 in [27] directly establishes the fact that under
the conditions of the lemma, we may replace all occurrences of some $w_{i}$
with $|w_{i}|>e$ consistently with any other word $u$ and still have a
solution to the word equation. We need to ensure that this replacement also
respects the regular language membership constraints, and this is the novel
part of this proof. In particular, while in part (1) a similar replacement was
done while preserving the length of the replaced strings, here we need to
change the length of the solution.

To see how this can be achieved, for each position $p$ of $w_{i}$ (that is for
each number $p$ with $1\leq p\leq|w_{i}|$), and for each $j$, $1\leq j\leq m$
we associate a function $g_{p,j}:Q_{j}\to Q_{j}$ such that
$g_{p,j}(q)=q^{\prime}$ if the automaton $A_{j}$ finishes in state
$q^{\prime}$ when reading the first $p$ letters of $w_{i}$ starting in state
$q$.

Note that if $g_{p,j}(q)=g_{p^{\prime},j}(q)$, and when the automaton reads
$w_{j}$ it begins reading an occurrence of $w_{i}$ in state $q$, then the
factor of that occurrence of $w_{i}$ between positions $p$ and $p^{\prime}$
can be removed without affecting acceptance. Thus, if
$g_{p,j}=g_{p^{\prime},j}$, then the factor between positions $p$ and
$p^{\prime}$ can be removed from all occurrences of $w_{i}$ in $w_{j}$ without
affecting the acceptance w.r.t. $A_{j}$. Finally, if there exist
$p,p^{\prime}$ such that $g_{p,j}=g_{p^{\prime}j}$ for all $j,1\leq j\leq m$,
then the factor between positions $p$ and $p^{\prime}$ of $w_{i}$ can be
removed from all occurrences of $w_{i}$ in all words $w_{j}$ without affecting
the satisfaction of any of the regular membership constraints.

Once the formula $f$ is fixed, the cardinalities of the sets of states $Q_{j}$
are also fixed. Moreover, the number of possible values for $j\leq m$ is
fixed. Thus the number of distinct functions $g_{p,j}$ is bounded and so is
the number of combinations of functions $(g_{p,j})_{1\leq j\leq m}$. Let $e$
be the number of possible combinations of these functions. Then, if
$|w_{i}|>e$, we must necessarily be able to find $p,p^{\prime}$ with
$p\not=p^{\prime}$ such that $g_{p,j}=g_{p^{\prime},j}$ for all $j$. By taking
$u$ to be the word obtained by removing the factor between positions $p$ and
$p^{\prime}$ in $w_{i}$, we therefore obtain $|u|<|w_{i}|$ and still satisfy
all regular language membership constraints as required.

Using Lemma 4.7(1), we can show that there is a language expressible in
$\operatorname{WE}\operatorname{+}\operatorname{REG}$ (thus, in
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$
as well) which is not expressible in
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$. Similarly, using Lemma
4.7(2) we can show that there is a language expressible in
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ (and thus in
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$)
which is not expressible in
$\operatorname{WE}\operatorname{+}\operatorname{REG}$.

######  Lemma 4.9.

Let $a,b,c$ be distinct letters. (1) The language $L=\\{vc\mid
v\in\\{a,b\\}^{*}\\}$ is expressible in
$\operatorname{WE}\operatorname{+}\operatorname{REG}$ but not expressible in
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$. (2) The language
$L=\\{ucv\mid u,v\in\\{a,b,c\\}^{*}\land|u|=|v|\\}$ is expressible in
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ but not expressible in
$\operatorname{WE}\operatorname{+}\operatorname{REG}$.

######  Proof 4.10.

Proof of Part (1): Suppose to the contrary that $L$ is expressible in a theory
from $\operatorname{WE}\operatorname{+}\operatorname{LEN}$. Let
$\Sigma\supseteq\\{a,b,c\\}$ be the underlying alphabet of that theory. Let
$f$ be a formula from that theory and $x$ a variable in $f$ such that $L$ is
the language expressed by $x$ in $f$. Let $d$ be the constant from Lemma 4.7.

Now, clearly $w=aba^{2}ba^{3}b\ldots a^{d}bc$ belongs to the language $L$.
Moreover, recall that the factorisation $\mathfrak{F}$ of words into blocks of
single letters is a synchronising factorisation. Now, the
$\mathfrak{F}$-factorisation of $w$ consists of at least $d+2$ distinct
factors (namely $a^{i}$ for $1\leq i\leq d$, $b$ and $c$), so by Lemma 4.7 we
may swap all occurrences of at least one of these factors for any word of the
same length and we will get another word in the language $L$. However,
whichever block of letters we swap, we can always choose a word of equal
length which violates membership in $L$. If we have a block consisting of
$a$’s or of a $b$, we can swap it for a word in $c*$ and the resulting word
will not be in $L$. Likewise, if we swap the block $c$, we could swap it e.g.
for an $a$ and again the resulting word will not be in $L$. In all cases we
get a contradiction, so $L$ cannot be expressible in $\mathfrak{T}$ as
required.

Proof of Part (2). The fact that $L$ is expressible in
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ is straightforward. To
see that it is not expressible in
$\operatorname{WE}\operatorname{+}\operatorname{REG}$, suppose to the contrary
that it is. Then there exists a theory $\mathfrak{T}$ from
$\operatorname{WE}\operatorname{+}\operatorname{REG}$ containing a formula $f$
such that $L$ is expressed by a variable $x$ in $f$. Let $d,e$ be the
constants from Lemma 4.7. Then there exist pairwise distinct numbers
$p_{1},p_{2},\ldots,p_{d},q_{1},q_{2},\ldots,q_{d}>e$ such that $\sum
p_{i}=\sum q_{i}$ and thus such that
$w=a^{p_{1}}b^{p_{1}}a^{p_{2}}b^{p_{2}}\ldots
a^{p_{d}}b^{p_{d}}ca^{q_{1}}b^{q_{1}}a^{q_{2}}b^{q_{2}}\ldots
a^{q_{d}}b^{q_{d}}$ belongs to $w$.

Recall that the factorisation $\mathfrak{F}$ of words into blocks of single
letters is a synchronising factorisation. Now, the
$\mathfrak{F}$-factorisation of $w$ consists of $4d$ distinct factors having
length greater than $e$ (namely $a^{p+i},b^{p_{i}},a^{q_{i}},b^{q_{i}}$ for
$1\leq i\leq d$), so by Lemma 4.7 we may swap all occurrences of at least one
block of letters for a strictly shorter block. However, since each block of
letters occurs only once (by the fact that the $p_{i}$s and $q_{i}$s are all
pairwise distinct), this would result in a word for which one side of the
central $c$ is shorter than the other, and thus not belonging to $L$, a
contradiction. Thus $L$ cannot be expressible as required.

Summarising, we get that
$\operatorname{WE}\operatorname{+}\operatorname{LEN},\operatorname{WE}\operatorname{+}\operatorname{REG}\,\prec\,\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$,
while the classes of languages expressible in
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ and
$\operatorname{WE}\operatorname{+}\operatorname{REG}$ are incomparable.

Next, we turn our attention to the remaining theories which do not extend the
expressive power of word equations. Since we have already seen that
concatenation together with visibly pushdown (or deterministic context-free)
membership constraints is enough to model recursively enumerable languages,
and therefore word equations, the remaining theories consist of language
membership without concatenation (but possibly with length constraints) and
all combinations consisting of regular language membership constraints without
word equations (so including either concatenation, length constraints, both,
or neither).

In the following lemma, we state another important result. For this, let
${\mathcal{C}}$ be a class of formal languages which contains
$\operatorname{REGLang}$, is contained in $\operatorname{CFLang}$, and is
effectively closed under intersection and complement. We assume that the
languages of ${\mathcal{C}}$ are specified by an accepting or generating
mechanism which allows the construction of a context-free grammar generating
that language. Let ${\mathcal{C}}_{t}$ be the theory defined as in Section 2
which allows only language membership predicates (of type A1) for the class of
languages ${\mathcal{C}}$. Let
${\mathcal{C}}_{t}\operatorname{+}\operatorname{LEN}$ be the theory which also
allows length constraints. In this framework, the following holds.

######  Lemma 4.11.

${\mathcal{C}}_{t}\operatorname{+}\operatorname{LEN}\sim{\mathcal{C}}_{t}$.

######  Proof 4.12.

Let $f$ be a formula in ${\mathcal{C}}_{t}\operatorname{+}\operatorname{LEN}$
and let $\alpha_{1},\ldots,\alpha_{r}$ be the atoms appearing in this formula.
We can compute all the assignments of truth values to the atoms
$\alpha_{1},\ldots,\alpha_{r}$ which make $f$ true. That is, each such
assignment $\sigma$ simply maps each $\alpha_{i}$ to a true or false, such
that at the end $f$ evaluates to true according to the values assigned by
$\sigma$ to its atoms. Now, for each assignment $\sigma$ as above, we
construct a formula $f_{\sigma}$ as the conjunction of the formulae
$\beta_{\ell}$, for $\ell\in\\{1,\ldots,r\\}$, where
$\beta_{\ell}=\alpha_{\ell}$ if $\alpha_{\ell}$ is true in $\sigma$ and
$\beta_{\ell}=\neg\alpha_{\ell}$, otherwise. Moreover, in $f_{\sigma}$ we
replace each language constraint $\neg{(x\in L)}$ by the constraint ${x\in
L^{C}}$, where $L^{C}$ is the complement of the language $L$. Let $f^{\prime}$
be the disjunction of all the fomulae $f_{\sigma}$. It is not hard to see that
$f^{\prime}$ is equivalent to $f$, i.e., the assignments of the variables
which satisfy $f$ are exactly the same as the assignments of the variables
which satisfy $f^{\prime}$.

Consider now a formula $f_{\sigma}$. Let $f_{1}$ be the sub-formula of
$f_{\sigma}$ consisting in all the arithmetic constraints.

Let $x$ be a string variable occurring in $f_{\sigma}$. Let $x\in L^{x}_{i}$,
for $i\in\\{1,\ldots,k_{x}\\}$ and some positive integer $k_{x}$, be all the
language membership constraints involving the variable $x$ occurring in
$f_{\sigma}$. According to our hypotheses regarding the class of languages
${\mathcal{C}}$, we can compute a representation of the language
$L_{x}=\cap_{i=1,k_{x}}L^{x}_{i}$, and the context-free grammar generating
$L_{x}$.

By Parikh’s theorem [37], we can compute a regular language $R_{x}$ (and a DFA
$A_{x}$ accepting it) such that the set of Parikh vectors of the words in
$R_{x}$ is equal to the set of Parikh vectors of the words in $L_{x}$. In
particular, this means that $L_{x}$ contains a word of length $\ell$ if and
only if $R_{x}$ contains a word of length $\ell$, for all $\ell\geq 0$.

Further, let $B_{x}$ be the unary NFA with $m_{x}$ states obtained by re-
labelling all transitions in $A_{x}$ with a single letter $a$. It is clear
that the paths of $A_{x}$ correspond bijectively to the paths of $B_{x}$.
Further, we compute the NFA $B^{\prime}_{x}$, the Chrobak normal form of the
unary automata $B_{x}$ (see [13, 21]). As such, $B^{\prime}_{x}$ consists of a
path of length $O(m_{x}^{2})$ ending in a state $q$, followed by a single
nondeterministic choice from $q$ to a set of disjoint cycles of lengths
$c_{1},c_{2},\ldots,c_{h}$, with $c_{i}\leq m_{x}$ for all $i\leq h$. It
follows that there exists a finite set of arithmetic progressions which
describe exactly the length of accepted words for $B^{\prime}_{x}$. Let
$\ell^{x}_{p,i}+\ell^{x}_{c,i}\operatorname{\mathbb{N}}$, for
$i\in\\{1,\ldots,d_{x}\\}$, be these progressions corresponding to
$B^{\prime}_{x}$. Note that for each of these lengths (and, accordingly, for
each of the accepting paths of $B^{\prime}_{x}$), there exists a word of
corresponding length accepted by $B_{x}$, so there also exists a word of this
length in $R_{x}$, and, ultimately, a word of this length in $L_{x}$.

Consequently, for each string variable $x$ we now get a series of new
arithmetic constraints on the length of each variable $x$: in a satisfying
assignment of $x$, we must have that $|x|$ has the form
$\ell^{x}_{p,i}+\alpha^{x}_{i}\ell^{x}_{c,i}$, for some $i\leq d_{x}$; here
$\alpha^{x}_{i}$ is a positive integer variable. So, we define a new formula
$f_{x}$ of length constraints: $f_{x}=\lor_{i\leq
d_{x}}|x|=\ell^{x}_{p,i}+\alpha^{x}_{i}\ell^{x}_{c,i}$.

We now define $f_{ar}=f_{1}\land(\land_{x\mbox{ string variable}}f_{x})$.

At this point, it is worth noting that a satisfying assignment for $f_{ar}$,
which assigns to $|x|$ the integer $\ell_{x}$, induces an assignment for the
lengths of all the string variables occurring in $f_{\sigma}$. Moreover, due
to the construction of the formulae $f_{x}$, we have that for each such
variable $x$ there exists (at least) an accepting path of length $\ell_{x}$ in
$B^{\prime}_{x}$. As explained above, this means that for each such variable
$x$ there exists (at least) a word of length $\ell_{x}$ in $L_{x}$. Thus, a
satisfying assignment for $f_{ar}$ induces (at least) one assignment of both
the string and the integer variables occurring in $f_{\sigma}$ which satisfies
$f_{\sigma}$.

Further, by standard methods, the arithmetic formula $f_{ar}$ can be
transformed in a linear system $A\mathbf{y}\geq\mathbf{b}$, where $A$ is a
matrix of integers, $\mathbf{y}$ is the vector of integer variables (including
the lengths of string variables), and $\mathbf{b}$ is a vector of integers. By
the results in [14], we get that for a system of inequalities
$A\mathbf{y}\geq\mathbf{b}$ we can compute two finite sets of vectors, $H_{0}$
and $H_{1}$, such that each integral solution $v$ of the system (i.e.,
assignment of the ${\mathbf{y}}\leftarrow v$ of the integer and length
variables which satisfies $A\mathbf{y}\geq\mathbf{b}$) can be expressed as the
sum $v_{0}+v_{1}$ where $v_{0}$ is a linear combination (with integral non-
negative coefficients) of vectors from $H_{0}$, and $v_{1}$ is a vector from
$H_{1}$. Therefore, the length $|x|$ of each string variable $x$ has the form
$\lambda_{1}a_{x,1}+...+\lambda_{d}a_{x,d}+b_{x}$, where $d$ is the number of
vectors in $H_{0}$, the integers $a_{x,j}$ are determined by the vectors of
$H_{0}$, and $b_{x}$ is determined by the vectors of $H_{1}$. The parameters
$\lambda_{j}$ are positive integers. Moreover, we can assume that all
$a_{x,j}$ are positive; otherwise, if some $a_{x,t}$ would be negative, it is
enough to note that when $\lambda_{t}$ grows to infinity, and all other
$\lambda_{x,j}$ are set to $1$, the length $|x|$ would become negative, a
contradiction.

Now, it is not hard to note that the set of strings $w$ whose length has the
form $\lambda_{1}a_{x,1}+...+\lambda_{d}a_{x,d}+b_{x}$, for any fixed positive
integers $a_{x,j}$ and integer $b_{x}$, is a regular language $D_{x}$.

Let us now define $g_{\sigma}=\land_{x\mbox{ string variable}}(x\in L_{x}\cap
D_{x})$. We analyse the sets of strings which can be expressed by $x$ in
$f_{\sigma}$ and $g_{\sigma}$, respectively.

Let $w$ be a string which can be expressed by a string variable $x$ in
$f_{\sigma}$. Then, by the construction of the set $D_{x}$, it is clear that
$w\in D_{x}$. Also, there exists an assignment, which satisfies $f_{\sigma}$,
where $x$ is mapped to $w$ and, for other each variable $y$, the string
assigned to $y$ is in $D_{y}$ (simply because the formula $f_{ar}$ is
satisfied in a satisfying assignment of $f_{\sigma}$). Therefore, the
respective assignment for the variables in $f_{\sigma}$ is also a satisfying
assignment for $g_{\sigma}$, and $w$ can be expressed by $x$ also in
$g_{\sigma}$.

For the converse, let $u_{x}$ be a string which can be expressed by $x$ in
$g_{\sigma}$, and let $\ell_{x}=|u_{x}|$. This means that $u_{x}\in D_{x}\cap
L_{x}$. By definition, $u_{x}$ is part of at least one satisfying assignment
for $g_{\sigma}$. Note, however, that this initial assignment is not
necessarily satisfying $f_{ar}$: it simply consists in an assignment
$y=u^{\prime}_{y}\in D_{y}\cap L_{y}$ for each variable $y$ of $g_{\sigma}$
other than $x$, and the lengths of these strings are not synchronized in such
a way that they form (together with $\ell_{x}$) a solution for $f_{ar}$.
However, because $u_{x}\in D_{x}$, we obtain that $f_{ar}$ has a solution with
$|x|=\ell_{x}$. So, there exists an assignment $|y|=\ell_{y}$, for all the
other string variables $y$ occurring in $g_{\sigma}$, which, together with
$\ell_{x}$, satisfies $f_{ar}$. By the explanations we gave during the
construction, it follows that there exists for each variable $y\neq x$ a
string $u_{y}$ (not necessarily the same from the satisfying assignment of
$g_{\sigma}$ considered above) such that the numbers $\ell_{y}=|u_{y}|$, for
$y$ such that $y\neq x$, and $\ell_{x}$ are part of a satisfying assignment
for $f_{ar}$. Clearly, $u_{z}\in L_{z}\cap D_{z}$, for all string variables
$z$ (including $x$). Note that the assignment $z=u_{z}$, for all string
variables $z$ occurring in $g_{\sigma}$, is still a satisfying assignment of
$g_{\sigma}$, although not necessarily the one we started with. Thus, as
$u_{z}\in L_{z}$, for all string variables $z$ of $f_{\sigma}$, and the tuple
defined by the numbers $\ell_{z}$ (together with an assignment of the integer
variables) satisfies $f_{1}$, it follows that the assignment $z=u_{z}$, for
all string variables $z$ occurring in $f_{\sigma}$, is part of a satisfying
assignment for $f_{\sigma}$. In conclusion, if $u_{x}$ is a string expressed
by $x$ in $g_{\sigma}$, we can construct a satisfying assignment for the
variables of $g_{\sigma}$, which is part of a satisfying assignment of the
variables of $f_{\sigma}$. Therefore, $u_{x}$ can be expressed by $x$ in
$f_{\sigma}$ too.

Now, it is easy to see that the following statements are equivalent:

  * •

$w$ is a string which can be expressed by $x$ in $f$;

  * •

$w$ is a string which can be expressed by $x$ in $f^{\prime}$;

  * •

there exists an assignment $\sigma$ of the atoms of $f^{\prime}$ which
satisfies $f^{\prime}$ and $w$ is a string which can be expressed by $x$ in
$f_{\sigma}$;

  * •

there exists an assignment $\sigma$ of the atoms of $f^{\prime}$ which
satisfies $f^{\prime}$ and $w$ is a string which can be expressed by $x$ in
$g_{\sigma}$;

  * •

$w$ is a string which can be expressed by $x$ in $g^{\prime}$, the disjunction
of all the formulae $g_{\sigma}$.

Because the class of languages ${\mathcal{C}}$ includes all the regular
languages and is effectively closed under intersection and complementation, we
obtain that $g^{\prime}$ is a ${\mathcal{C}}_{t}$-formula. This concludes our
proof.

As $\operatorname{VPLang}$ is a class which fulfills the properties of the
class ${\mathcal{C}}$ from the above lemma, and is strictly included in
$\operatorname{RE}$, we immediately get the first claim of the following
theorem. The second claim can also be shown with some additional effort.

######  Theorem 4.13.

(1)
$\operatorname{VPL}\,\sim\,\operatorname{VPL}\operatorname{+}\operatorname{LEN}\prec\,\operatorname{VPL}\operatorname{+}\operatorname{CON}$.
(2)
$\operatorname{REG}\,\sim\,\operatorname{REG}\operatorname{+}\operatorname{LEN}\,\sim\,\operatorname{REG}\operatorname{+}\operatorname{LEN}\operatorname{+}\operatorname{CON}$.

######  Proof 4.14.

Proof of Part (1): This is straightforward, as $\operatorname{VPL}$ fulfils
the requirements of Lemma 4.11.

Proof of Part (2): Firstly, we need to introduce a notation.

If $A=(Q,q_{0},F,\delta)$ is a finite automaton with the set of states $Q$,
initial state $q_{0}$, set of final states $F$, and transition function
$\delta$, and $q_{1},q_{2}\in Q$, then $A_{q_{1},q_{2}}$ is the finite
automaton $A_{q_{1},q_{2}}=(Q,q_{1},\\{q_{2}\\},\delta)$. In other words,
$A_{q_{1},q_{2}}$ is a finite automaton with the same underlying graph as $A$,
but with a different initial state ($q_{1}$ instead of $q_{0}$) and a
different set of final states ($\\{q_{2}\\}$ instead of $F$).

We now move to the actual proof.
$\operatorname{REG}\,\sim\,\operatorname{REG}\operatorname{+}\operatorname{LEN}$
follows from Lemma 4.11, as $\operatorname{REGLang}$ clearly fulfils all
properties of the class ${\mathcal{C}}$ from the respective lemma.

Let us now consider a formula $f$ from
$\operatorname{REG}\operatorname{+}\operatorname{LEN}\operatorname{+}\operatorname{CON}$.
We construct a formula $f^{\prime\prime}$ from
$\operatorname{REG}\operatorname{+}\operatorname{LEN}$ which is equivalent to
$f$.

Let $\alpha_{1},\ldots,\alpha_{r}$ be the atoms appearing in $f$. Similarly to
Lemma 4.11, we can compute all the assignments of truth values to the atoms
$\alpha_{1},\ldots,\alpha_{r}$ which make $f$ true. For each such assignment
$\sigma$ we construct a formula $f_{\sigma}$ as the conjunction of the
formulae $\beta_{\ell}$, for $\ell\in\\{1,\ldots,r\\}$, where
$\beta_{\ell}=\alpha_{\ell}$ if $\alpha_{\ell}$ is true under $\sigma$ and
$\beta_{\ell}=\neg\alpha_{\ell}$, otherwise. Moreover, in $f_{\sigma}$ we
replace each language constraint $\neg{(\beta\in L)}$ by the constraint
${\beta\in L^{C}}$, where $L^{C}$ is the complement of the language $L$. Let
$f^{\prime}$ be the disjunction of all the formulae $f_{\sigma}$. It is clear
that $f^{\prime}$ is equivalent to $f$, i.e., the satisfying assignments (of
the variables) for $f$ are exactly the same as the satisfying assignments (of
the variables) for $f^{\prime}$.

Consider now a conjunction $g$ of language membership atoms from
$\operatorname{REG}\operatorname{+}\operatorname{CON}$ and arithmetic atoms.
We define a consistent language assignment of $g$ as a mapping $\pi$ which
leaves every arithmetic atom unchanged and maps every membership atom
$\beta=w_{0}x_{1}w_{1}\cdots x_{k}w_{k}\in L$ of $g$, where $x_{i}$ is a
string variable for $i\in\\{1,\ldots,k\\}$, $w_{i}$ is a constant string for
$i\in\\{0,\ldots,k\\}$, and $L$ is a regular language accepted by a DFA
$A=(Q,q_{0},F,\delta)$, to the formula $\pi(\beta)=\land_{i=1,k}(x_{i}\in
L(A_{q_{2i-1},q_{2i}}))$, where

  * •

$q_{1}=\delta(q_{0},w_{0})$,

  * •

$q_{2i+1}=\delta(q_{2i},w_{i})$, for $i=1,k-1$,

  * •

$\delta(q_{2k},w_{k})\in F$.

It is clear that the formula $g_{\pi}$, obtained by replacing each atom
$\beta$ of $g$ by $\pi(\beta)$, is now a formula over
$\operatorname{REG}+\operatorname{LEN}$. Moreover, it is immediate that the
formula $rl(g)$ defined as the disjunction of the formulae $g_{\pi}$, for all
consistent language assignments $\pi$ of $g$, is a formula over
$\operatorname{REG}\operatorname{+}\operatorname{LEN}$. Clearly, $rl(g)$ is
equivalent to $g$, i.e., the satisfying assignments for $g$ are exactly the
same as the satisfying assignments for $rl(g)$.

Coming back to the formula $f^{\prime}$ which we have constructed above
starting from $f$, we further define a formula $f^{\prime\prime}$ as the
disjunction of all the formulae $rl(f_{\sigma})$. It is clear that
$f^{\prime\prime}$ is a formula from
$\operatorname{REG}\operatorname{+}\operatorname{LEN}$, and that
$f^{\prime\prime}$ is equivalent to $f$, i.e., the satisfying assignments for
$f$ are exactly the same as the satisfying assignments for $f^{\prime\prime}$.

This shows that
$\operatorname{REG}\operatorname{+}\operatorname{CON}\operatorname{+}\operatorname{LEN}\sim\operatorname{REG}\operatorname{+}\operatorname{LEN}$.

Recall that the languages expressible in $\operatorname{REG}$ (and in
$\operatorname{REG}\operatorname{+}\operatorname{LEN}$ and
$\operatorname{REG}\operatorname{+}\operatorname{CON}\operatorname{+}\operatorname{LEN}$)
and $\operatorname{VPL}$ (as well as
$\operatorname{VPL}\operatorname{+}\operatorname{LEN}$) are exactly the
classes $\operatorname{REGLang}$ and, respectively, $\operatorname{VPLang}$,
and for each formula in one of these theories we can effectively construct a
corresponding automaton accepting the language expressed by a given variable.
See Remark 4.15 below.

######  Remark 4.15.

In fact, for a formula $f$ in the theory
$\operatorname{VPL}\operatorname{+}\operatorname{LEN}$ (which includes the
theories $\operatorname{REG}$,
$\operatorname{REG}\operatorname{+}\operatorname{LEN}\operatorname{+}\operatorname{CON}$,
and $\operatorname{VPL}$) we can effectively construct a formula $g^{\prime}$
which is a disjunction of conjunctions $g_{\sigma}$ involving at most one
membership predicate $x\in S_{x}$ per variable, where each language $S_{x}$ is
in $\operatorname{VPLang}$. We can remove from $g^{\prime}$ the conjunctions
$g_{\sigma}$ which contain at least one membership predicate $x\in S_{x}$ with
$S_{x}=\emptyset$. Now, it is easy to see that for the language expressed by
$x$ is exactly the union of the languages $S_{x}$ for all membership
predicates $x\in S_{x}$ occurring in $g^{\prime}$. Therefore, this language is
in the class $\operatorname{VPLang}$, and we can effectively compute an
automaton accepting it. Therefore, we can easily conclude that for two given
formulae $f$ and $\phi$ from
$\operatorname{VPL}\operatorname{+}\operatorname{LEN}$ and a variable $x$
occurring in $f$ and a variable $\phi$ occurring in $\phi$, we can decide
whether the language expressed by $x$ is the same as (respectively, included
in) the language expressed by $y$.

Let us now consider the theory $\operatorname{DCF}$. The result of Lemma 4.11
does not apply in this case, as the class of languages
$\operatorname{DCFLang}$ is not closed under intersection. In fact, for Lemma
4.11 to work, it would be enough to have that if $L$ is a finite intersection
of languages from the class ${\mathcal{C}}$ then the set $S=\\{|w|\mid w\in
L\\}$ is semi-linear. However, this still does not hold for
$\operatorname{DCFLang}$. See Example 4.16 below.

######  Example 4.16.

Let $U_{1}=\\{a^{n}b^{2n}\mid n\geq 1\\}$ and $L_{1}=U_{1}^{+}$. Let
$U_{2}=\\{b^{n}a^{n}\mid n\geq 1\\}$ and $L_{2}=aU_{2}^{+}b^{+}$. It is clear
that $L_{1}$ and $L_{2}$ are in $\operatorname{DCF}$. Let $L=L_{1}\cap L_{2}$.
It is not hard to observe that $L=\\{ab^{2}a^{2}b^{4}a^{4}b^{8}\cdots
a^{2^{k}}b^{2^{k+1}}\mid k\geq 1\\}$. Further, let $S=\\{|w|\mid w\in L\\}$.
We have that $S=\\{2^{k+2}+2^{k+1}-3\mid k\geq 1\\}$. Clearly, $S$ is not a
semi-linear set (and it is not a deterministic context-free language either).

We now show an additional lemma.

######  Lemma 4.17.

$L=\\{wcw\mid w\in\\{a,b\\}^{*}\\}$ is expressible in
$\operatorname{WE}\operatorname{+}\operatorname{REG}$ and not in
$\operatorname{DCF}$.

######  Proof 4.18.

Recall that the languages expressible in a theory belonging to the family
$\operatorname{DCF}$ are exactly the closure of the deterministic context-free
languages under the Boolean operations: intersection, complement and union. It
was shown in [44] that this closure is strictly contained in the intersection-
closure of the context-free languages. Moreover, it was also shown in [44]
that $L$ in question does not belong to the intersection closure of context-
free languages. Thus, we may conclude that it is not expressible in any theory
belonging to $\operatorname{DCF}$.

By Theorem 4.5 and the existence $\operatorname{RE}$-languages which are not
expressible in $\operatorname{DCF}$ (see [44], as well as Lemma 4.17 or
Example 4.16), we may infer the following relations:
$\operatorname{DCF}\preceq\operatorname{DCF}\operatorname{+}\operatorname{LEN}\preceq\operatorname{DCF}+\operatorname{CON}$
and $\operatorname{DCF}\prec\operatorname{DCF}+\operatorname{CON}$. This also
shows that at least one of the relations
$\operatorname{DCF}\preceq\operatorname{DCF}\operatorname{+}\operatorname{LEN}$
and
$\operatorname{DCF}\operatorname{+}\operatorname{LEN}\preceq\operatorname{DCF}+\operatorname{CON}$
is strict. In fact, there are some indications (see Remark 4.19 below) that
the separation might occur between
$\operatorname{DCF}\operatorname{+}\operatorname{LEN}$ and
$\operatorname{DCF}\operatorname{+}\operatorname{CON}$.

######  Remark 4.19.

We observe that the language $L=\\{wcw\mid w\in\\{a,b\\}^{*}\\}$, which is
expressible in $\operatorname{DCF}\operatorname{+}\operatorname{CON}$ and not
$\operatorname{DCF}$, is not expressible by a restricted set of formulas in
$\operatorname{DCF}\operatorname{+}\operatorname{LEN}$.

Assume that there exists a formula $\phi$ in
$\operatorname{DCF}\operatorname{+}\operatorname{LEN}$, over the variables
$x,y_{1},\ldots,y_{k}$, such that $\phi$ is a conjunction of language
membership atoms and arithmetic atoms, and the language expressed by $x$ is
$L$. In this case, for each odd number $2k+1$ there exists
$(w_{x},w_{y_{1}},\ldots,w_{y_{k}})$, an assignment of the variables
$(x,y_{1},\ldots,y_{k})$ which satisfies $\phi$, with $|w_{x}|=2k+1$. Also, if
there is an assignment $w^{\prime}_{x}$ of $x$ which satisfies all the
language membership atoms involving $x$ and also $|w^{\prime}_{x}|=2k+1$, then
it is not hard to see that $(w^{\prime}_{x},w_{y_{1}},\ldots,w_{y_{k}})$ is
also a satisfying assignment for $\phi$ (as the membership atoms involving
various variables are independent). So, we can now observe that, in this
framework, $L$ would be expressed by $x$ in a conjunction of membership atoms:
the ones describing $x$ in $\phi$ and a new one, stating that the length of
$x$ is odd. This new formula would clearly be in $\operatorname{DCF}$, which
leads to a contradiction. A similar argument would also work for slightly more
complicated formulae $\phi$, but seems to need a nontrivial extension to cover
the entire theory $\operatorname{DCF}\operatorname{+}\operatorname{LEN}$.
However, based on this observation, we conjecture that the relation
$\operatorname{DCF}\operatorname{+}\operatorname{LEN}\preceq\operatorname{DCF}+\operatorname{CON}$
is, in fact, strict.

As said above,
$\operatorname{REG}\operatorname{+}\operatorname{LEN}\operatorname{+}\operatorname{CON}$
and $\operatorname{VPL}\operatorname{+}\operatorname{LEN}$ express exactly the
classes of regular languages and VPL languages, respectively. Since the
regular languages are a strict subset of the VPL languages, which in turn are
a strict subset of the deterministic context-free languages, we may conclude
the following strict inclusions in terms of expressibility:
$\operatorname{REG}\operatorname{+}\operatorname{LEN}\operatorname{+}\operatorname{CON}\,\prec\,\operatorname{VPL}\operatorname{+}\operatorname{LEN}\,\prec\,\operatorname{DCF}$.

Note that there are languages expressible in $\operatorname{WE}$ (such as
$\\{xx\mid x\in\Sigma^{*}\\}$) which are not regular nor visibly pushdown, and
thus not expressible in $\operatorname{REG}$ or $\operatorname{VPL}$ or
theories with equivalent expressibility. So,
$\operatorname{REG}\prec\operatorname{WE}\operatorname{+}\operatorname{REG}$
holds. Moreover, we have already seen examples of regular languages which are
not expressible in $\operatorname{WE}$ or
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$. In this context, we
leave open the following particularly interesting problem:

######  Open Problem 1.

Which recursively enumerable languages (if any) can be shown not to be
expressible by a formula from
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$?

Based on the previous results, we can now also discuss the emptiness problem,
and the closely related finiteness problem. This is particularly interesting
since emptiness for a language expressed by a formula $f$ and variable $x$
corresponds exactly to the satisfiability problem for $f$. Based on existing
literature [3, 24, 40, 33], it is not hard to show that emptiness and
finiteness are decidable for $\operatorname{VPL}$ and
$\operatorname{WE}\operatorname{+}\operatorname{REG}$ but undecidable for
$\operatorname{DCF}$.

On the other hand, two cases where it seems particularly difficult to settle
the decidability status of the satisfiability and, therefore, emptiness
problems are $\operatorname{WE}\operatorname{+}\operatorname{LEN}$ and
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$.
Emptiness for the former in particular is equivalent to the satisfiability
problem for word equations with length constraints which is a long-standing
and important open problem in the field. Similarly, the latter is prominent in
the context of string-solving and as such satisfiability/emptiness also
presents an important open problem which is likely to be closely related to
that of $\operatorname{WE}\operatorname{+}\operatorname{LEN}$. Consequently,
$\operatorname{WE}\operatorname{+}\operatorname{VPL}$ presents a particularly
interesting case as a “reasonable” generalisation of
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$
and, in the absence of answers regarding this theory, it makes sense to
consider the same problems for theories with slightly more or slightly less
expressive power. If we extend the expressive power as far as
$\operatorname{WE}+\operatorname{DCF}$, then undecidability is inherited
directly from $\operatorname{DCF}$. However, satisfiability and emptiness
remain decidable for $\operatorname{VPL}$. Moreover, visibly pushdown
languages share many of the desirable computational properties of regular
languages, meaning that we can view
$\operatorname{WE}\operatorname{+}\operatorname{VPL}$ as a slighter
generalisation of
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$.
Nevertheless, due to our result from Theorem 4.5 of the previous section, we
know that $\operatorname{VPL}\operatorname{+}\operatorname{CON}$ expresses
already $\operatorname{RE}$, so emptiness and finiteness are undecidable for
$\operatorname{VPL}\operatorname{+}\operatorname{CON}$, and consequently for
$\operatorname{WE}\operatorname{+}\operatorname{VPL}$ and other families
$\mathfrak{F}$ of theories satisfying
$\operatorname{VPL}\operatorname{+}\operatorname{CON}\preceq\mathfrak{F}$. The
left part of Figure 1 summarizes the understanding of the emptiness and
finiteness problems, as resulting from our results.

##  5 Universality, Greibach’s Theorem, and Expressibility Problems

Universality is an important problem for a number of reasons. Firstly,
undecidability of universality implies undecidability of equivalence and
inclusion for any theory in which the universal language $\Sigma^{*}$ is
expressible (which is true in any string-based theory containing at least one
tautology). Secondly, an undecidable universality problem is the foundation
for Greibach’s theorem, which is helpful for proving that many other problems
are undecidable. E.g., we shall make use of Greibach’s theorem to show several
problems concerning expressibility of languages in different theories are
undecidable. We recall Greibach’s theorem below.

######  Theorem 5.1 ([24]).

Let $\mathcal{C}$ be a class of formal languages over an alphabet
$\Sigma\cup\\{\\#\\}$ such that each language in $\mathcal{C}$ has some
associated finite description. Suppose $\mathcal{P}\subsetneq\mathcal{C}$ with
$\mathcal{P}\not=\emptyset$ and suppose that all the following hold:

  1. 1.

$\mathcal{C}$ and $\mathcal{P}$ both contain all regular languages over
$\Sigma\cup\\{\\#\\}$,

  2. 2.

$\mathcal{P}$ is closed under quotient by a single letter,

  3. 3.

Given (descriptions of) $L_{1},L_{2}\in\mathcal{C}$ descriptions of $L_{1}\cup
L_{2}$, $L_{1}R$ and $RL_{1}$ can be computed for any regular language
$R\in\mathcal{C}$,

  4. 4.

It is undecidable whether, given $L\in\mathcal{C}$, $L=\Sigma^{*}$.

Then the problem of determining, for a language $L\in\mathcal{C}$, whether
$L\in\mathcal{P}$ is undecidable.

Note that in order to apply Greibach’s theorem, we need a variant of the
universality problem to be undecidable which refers to a sub-alphabet, rather
than the whole alphabet.

######  Definition 5.2.

Let $\mathcal{T}$ be a theory defined in Section 3 with underlying alphabet
$\Sigma$ and such that $|\Sigma|\geq 3$. The subset-universality problem is:
given a formula $f\in\mathcal{T}$, variable $x$ occurring in $f$ and
$S\subset\Sigma$ with $|S|>1$, is the language expressed by $x$ in $f$ equal
to $S^{*}$?

We can infer the following results already from the literature:

######  Theorem 5.3 ([20, 16, 3, 24]).

Universality is undecidable for $\operatorname{WE}$ and $\operatorname{DCF}$,
and decidable for $\operatorname{VPL}$. Subset-universality is decidable for
$\operatorname{VPL}$ but not $\operatorname{DCF}$.

To discuss the equivalence and inclusion problems, it makes sense to consider
them in a general setting where the two languages may be taken from different
theories. We therefore consider equivalence and inclusion problems for pairs
of theories $(\mathfrak{T}_{1},\mathfrak{T}_{2})$. Combining the known results
above with the constructive equivalences pointed out in Remark 4.15, we easily
get that equivalence and inclusion for $(\mathfrak{T}_{1},\mathfrak{T}_{2})$
are undecidable whenever at least one of $\mathfrak{T}_{1},\mathfrak{T}_{2}$
contains $\operatorname{WE}$ or $\operatorname{DCF}$, but they are decidable
for all other pairs of theories. In a similar way, one can show that
cofiniteness is undecidable for $\operatorname{WE}$.

We may, clearly, propagate undecidability of universality and related problems
upwards through families of theories containing $\operatorname{WE}$ (or
$\operatorname{DCF}$) as a syntactic subset, or apply Rice’s theorem to get
such results for all theories expressing $\operatorname{RE}$. We can also show
the following.

######  Theorem 5.4.

Subset-universality is decidable for
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ and undecidable for
$\operatorname{WE}+\operatorname{REG}$. In particular, for $S$ large enough,
for any theory $\mathfrak{T}$ from
$\operatorname{WE}\operatorname{+}\operatorname{REG}$ with underlying alphabet
$\Sigma\supset S$, the problem of whether a language expressed in
$\mathfrak{T}$ is exactly $S^{*}$ is undecidable.

######  Proof 5.5.

The undecidability result can be obtained as follows. Recall from Theorem 5.3
that the standard universality problem for $\operatorname{WE}$ is undecidable.
In particular, there is an alphabet $S$ and theory $\mathfrak{T}^{\prime}$
from $\operatorname{WE}$ whose underlying alphabet is $S$ such that the
universality problem for $\mathfrak{T}^{\prime}$ is undecidable. Let
$\Sigma\supset S$. We reduce the universality problem for
$\mathfrak{T}^{\prime}$ to the subset universality problem for the the theory
$\mathfrak{T}$ from $\operatorname{WE}\operatorname{+}\operatorname{REG}$
whose underlying alphabet is $\Sigma$. In particular, for a formula
$f^{\prime}$ from $\mathfrak{T}^{\prime}$ with variables
$x_{1},x_{2},\ldots,x_{n}$, we construct the formula
$f=f^{\prime}\land\bigwedge\limits_{1\leq i\leq n}x_{i}\in S^{*}$. Clearly,
$f$ and $f^{\prime}$ have exactly the same set of satisfying assignments, and
so the language expressed by a variable $x_{i}$ is unchanged. Consequently,
the language expressed by $x_{i}$ in $f^{\prime}$ (in $\mathfrak{T}^{\prime}$)
is universal if and only if the language expressed by $x_{i}$ in $f$ satisfies
the subset-universality problem for the subset $S$ of $\Sigma$. Hence the
subset universality problem is undecidable for
$\operatorname{WE}\operatorname{+}\operatorname{REG}$.

Next we consider the same problem for $\operatorname{WE}$ and
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$. Note firstly that, for
any theory $\mathfrak{T}$ from
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ whose underlying
alphabet is $\Sigma$, if $1<|S|<|\Sigma|$, then it follows from the same
construction as in the proof of Lemma 4.9 that $S^{*}$ is not expressible by
any formula/variable from $\mathfrak{T}$. Thus in any such case we can simply
automatically answer “no”.

Theorem 5.4 allows us to apply Greibach’s Theorem to many theories defined in
Section 3.

######  Theorem 5.6.

Let $\mathfrak{F}$ be a family of theories defined in Section 3 containing
$\operatorname{WE}\operatorname{+}\operatorname{REG}$. For large enough
alphabets $\Sigma$, if $\mathcal{C}$ is the class of languages expressible by
the theory $\mathfrak{T}\in\mathfrak{F}$ with underlying alphabet $\Sigma$,
then the conditions of Greibach’s theorem are satisfied by $\mathcal{C}$.

######  Proof 5.7.

Recall that we consider descriptions of languages expressible in a theory to
be a formula $f$ together with a variable $x$ occurring in $f$. If
$f_{1},x_{1}$ and $f_{2},x_{2}$ describe languages $L_{1}$ and $L_{2}$
respectively, then $L_{1}\cup L_{2}$ is described by the formula $f_{1}\lor
f_{2}^{\prime}$ where $f_{2}^{\prime}$ is obtained by renaming the variables
in $f_{2}$ such that $x_{2}$ is renamed to $x_{1}$ and all other variables in
$f_{2}$ do not occur in $f_{1}$.

Now, suppose we have a family of theories $\mathfrak{F}$ which includes
$\operatorname{WE}\operatorname{+}\operatorname{REG}$. Let
$\mathfrak{T}\in\mathfrak{F}$ have underlying alphabet $\Sigma\cup\\{\\#\\}$
for “large” $\Sigma$. Then every regular language $R$ over
$\Sigma\cup\\{\\#\\}$ is expressible via the variable $x$ in the formula $x\in
R$. Moreover for any language $L$ expressible by a formula $f$ and variable
$x$, we may express the languages $LR$ and $RL$ through the variable $y$ in
the formulas $f\land y=xz\land z\in R$ and $y=f\land zx\land z\in R$
respectively where $y,z$ are new variables not in $f$.

Finally, we note that by Theorem 5.4, the problem of whether a given language
expressible in $\mathfrak{T}$ is exactly $\Sigma^{*}$ is undecidable. Thus, we
have shown all the conditions of Greibach’s theorem applicable to
$\mathcal{C}$ hold when $\mathcal{C}$ is the class of languages expressible in
$\mathfrak{T}$.

In the following, we give an example application of Theorem 5.6 with respect
to the pumping lemma for regular languages (see e.g. [24]). Aside from
defining an interesting superclass of the regular languages itself, there are
many reasons to be interested in notions of pumping. For example, when
considering (in)expressibility questions (even beyond the regular languages),
as well as part of a strategy for producing satisfiability results in the
context of length constraints or other restrictions. We use the pumping lemma
for regular languages because it is well known, but the ideas are easily
adapted to other useful notions of pumping and closure properties more
generally. We recall first this lemma.

######  Lemma 5.8 ([24]).

Let $L$ be a regular language. Then there exists a constant $c$ such that for
every $w\in L$ with $|w|>c$, there exist $x,y,z$ such that (i) $|xy|<c$, and
(ii) $w=xyz$, and (iii) $xy^{n}z\in L$ for all $n\in\mathbb{N}_{0}$.

Now, we can show how Theorem 5.6 can be applied in this context.

######  Theorem 5.9.

It is undecidable whether a language expressed by a formula in a theory from
$\operatorname{WE}+\operatorname{REG}$ satisfies the pumping lemma for regular
languages.

######  Proof 5.10.

By Theorem 5.6, there exist theories $\mathfrak{T}$ from
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$
such that the class $\mathcal{C}$ of languages expressible in $\mathfrak{T}$
satisfy the conditions of Greibach’s theorem. It remains to observe that the
property $\mathcal{P}$ of being a language which is expressible in
$\mathfrak{T}$ which also satisfies the pumping lemma for regular languages
also satisfies the conditions of Greibach’s theorem. In particular, we note
that all regular languages over the underlying alphabet belong to
$\mathcal{P}$ since all regular languages satisfy the pumping lemma for
regular languages. Moreover, it is straightforward to show that given a letter
$a$, and a language $L$ satisfying the pumping lemma, that the quotient of $L$
by $a$ also satisfies the pumping lemma. Since we can express the same
quotient in $\operatorname{WE}\operatorname{+}\operatorname{REG}$ with the
formula $f\land ya=x$ where $f$ and $x$ are the formula and variable
expressing $L$ respectively, we conclude that $\mathcal{P}$ is closed under
quotient by a single letter. Thus for an appropriate choice of underlying
alphabet for $\mathfrak{T}$, we may apply Greibach’s theorem to get the
claimed result.

Theorem 5.4 also tells us that we cannot use Greibach’s theorem as stated to
show that properties of languages expressible in
$\operatorname{WE}\operatorname{+}\operatorname{LEN}$ are undecidable. We
leave as an open problem whether an equivalent of Greibach’s theorem can be
adapted to this context:

######  Open Problem 2.

Is there an equivalent of Theorem 5.1 for the classes of languages expressible
in $\operatorname{WE}\operatorname{+}\operatorname{LEN}$ or
$\operatorname{WE}$?

##  6 Expressivity Problems

Further, we consider decision problems related to expressivity. These problems
have the general form: given a language $L$ expressed by a formula in a theory
$\mathfrak{T}_{1}$ and given a second theory $\mathfrak{T}_{2}$, can we decide
whether or not $L$ can be expressed by a formula in $\mathfrak{T}_{2}$?

We begin by noting that since it is decidable whether or not a deterministic
context-free language is regular (see [41, 43]), the same holds true for
visibly pushdown languages, and hence whether a language expressed in
$\operatorname{VPL}$ can be expressed in $\operatorname{REG}$. Therefore, it
is clearly decidable whether a language expressed in $\operatorname{VPL}$ is
expressible in $\operatorname{REG}$. The same holds for theories from families
equivalent to $\operatorname{VPL}$ and $\operatorname{REG}$ under the relation
$\sim$.

Naturally, since we have already seen that
$\operatorname{VPL}\operatorname{+}\operatorname{CON}$ is capable of
expressing all $\operatorname{RE}$-languages, it is undecidable whether a
language expressed in a theory from
$\operatorname{VPL}\operatorname{+}\operatorname{CON}$ is expressible in a
theory from any of the families which have strictly less expressive power.

The separation results from Section 4 and Theorem 5.6 together mean we can get
the following negative results as a consequence of Greibach’s theorem. They
have a particularly relevant interpretation in the context of string solving
in practice. Specifically, it is often the case that string-solvers will
perform some pre-processing of string constraints in order to put them in some
sort of normal form which will make them easier to solve. One natural thing to
want to do in this process is to reduce the number of combinations of sub-
constraints of differing types by converting constraints of one type to
another. This is useful particularly in cases where the combinations are
difficult to deal with together in general. Word equations, regular
constraints and length constraints are one such combination (recall from
Section 4 that satisfiability for the corresponding theory including all three
types of constraint is an open problem, but if length constraints are removed
then satisfiability becomes decidable). Unfortunately, the following theorem
reveals that we cannot in general decide whether length constraints can be
eliminated by rewriting them using only regular membership constraints and
word equations.

######  Theorem 6.1.

It is undecidable whether a language expressed in
$\operatorname{WE}+\operatorname{REG}+\operatorname{LEN}$ can be expressed in
$\operatorname{WE}+\operatorname{REG}$.

######  Proof 6.2.

Theorem 5.6 tells us that there exist theories $\mathfrak{T}$ from
$\operatorname{WE}\operatorname{+}\operatorname{REG}\operatorname{+}\operatorname{LEN}$
such that the class $\mathcal{C}$ of languages expressible in $\mathfrak{T}$
satisfy the conditions of Greibach’s theorem. It remains to observe that there
exist theories $\mathfrak{T}^{\prime}$ from
$\operatorname{WE}\operatorname{+}\operatorname{REG}$ such that the property
$\mathcal{P}$ of being a language expressible in $\mathfrak{T}^{\prime}$ also
satisfies the conditions of Greibach’s theorem.

In particular, we note that all regular languages over the underlying alphabet
belong to $\mathcal{P}$ trivially through the use of regular language
membership constraints. Moreover, it is straightforward that given a letter
$a$, and a language $L$ expressible in $\mathfrak{T}^{\prime}$, we can express
the quotient of $L$ by $a$ in $\mathfrak{T}^{\prime}$ with the formula $f\land
ya=x$ where $f$ and $x$ are the formula and variable expressing $L$
respectively and where $y$ is a new variable. Thus $\mathcal{P}$ is closed
under quotient by a single letter. For an appropriate choice of
$\mathfrak{T}^{\prime}$ (i.e. for the appropriate underlying alphabet), we may
hence apply Greibach’s theorem to get the claimed result.

The same undecidability result holds if, instead of removing length
constraints by rewriting them as regular membership constraints and word
equations, we want to remove word equations constraints by rewriting them as
regular language membership constraints (possibly also with length constraints
which, in the absence of word equations, do not increase the expressive power
due to Theorem 4.13). While this result can also be obtained via Greibach’s
theorem, we can, in fact, state a stronger version for which we need a novel
approach. In particular, we show that it is already undecidable whether a
language expressible by word equations (without additional constraints) is a
regular language (i.e., can be expressed in $\operatorname{REG}$).

######  Theorem 6.3.

It is undecidable whether a language expressed in $\operatorname{WE}$ is
regular. In other words, it is undecidable whether a language expressed by a
formula from $\operatorname{WE}$ is regular.

######  Proof 6.4.

We shall prove the statement by giving a reduction from the problem of
determining whether or not the set of words belonging to $0^{+}$ accepted by a
2-Counter Machine (2CM) is finite. Since we shall use word equations to model
computations of 2CMs, our proof has a similar flavour to the one in [20], but
since our aims and setting are different, the details and our construction is
also necessarily different.

A 2CM $M$ is a deterministic finite state machine with 3 semi-infinite storage
tapes, each with a leftmost cell but no rightmost cell. One is the input tape,
on which the input is initially placed. There is a read-only head which can
move along the input tape in both directions but cannot move beyond the input
word and cannot overwrite it. The other two tapes represent counters. They
each store a non-negative integer represented by the position of a head which
can move to the left or right. If the head is in the leftmost position, the
number represented is 0, and increments of one are achieved by moving the head
one position to the right.

$M$ can test if each counter is empty but cannot compare directly the stored
numbers for equality. It accepts a word if the computation with that word as
input terminates in an accepting state and such that all tape heads (input and
both counters) are at the leftmost position. Formally, a 2CM is a tuple
$(Q,\Delta,\delta,q_{0},F)$ where:

  1. 1.

$Q$ is a finite set of states, $q_{0}\in Q$ is an initial state and
$F\subseteq Q$ is a set of final or accepting states.

  2. 2.

$\Delta$ is a finite input tape alphabet.

  3. 3.

$\delta:Q\times\Delta\times\\{T,F\\}\times\\{T,F\\}\to
Q\times\\{1,2,3\\}\times\\{L,R\\}$ is a transition function.

The interpretation of the transition function is as follows:
$\delta(q,a,Z_{1},Z_{2})=(q^{\prime},i,D)$ if before the transition $M$ is in
state $q$ and currently reads letter $a$ on the input tape, and $Z_{1}$ and
$Z_{2}$ are $T$ if the first and second counters are $0$ respectively and $F$
otherwise, and after the transition $M$ is in state $q^{\prime}$, $D$
indicates the direction in which one of the tape heads moves (L for left and R
for right), and $i$ determines which tape head moves (1 for input head and 2
and 3 for the first and second counters respectively).

We can represent a configuration of a 2CM at any point in a computation as a
word belonging to $Q\Delta^{*}a^{+}b^{+}c^{+}$ (assuming $a,b,c$ are new
letters such that $Q,\Delta,\\{a,b,c\\}$ are pairwise disjoint) where the
leftmost letter (from $Q$ is the current state, the part from $\Delta^{*}$
stores the contents of the input tape (so, the input), and the a’s b’s and c’s
denote in unary notation the position of the input tape head and the values of
the two counters. For convenience, we add one to all these values so that the
sequences of a’s, b’s and c’s are all non-empty.

An initial configuration on input $w\in\Delta^{*}$ has the form $q_{0}wabc$,
and a final configuration has the form $q_{f}wabc$ where $q_{f}\in F$.

A valid computation history of a 2CM $M$ on input word $w$ is a finite word
$C=C_{1}C_{2}C_{3}\ldots C_{n}$ such that each $C_{i}$ is a configuration,
$C_{1}$ is the initial configuration for the input $w$, $C_{n}$ is a final
configuration, and such that each successive pair of configurations
$C_{i},C_{i+1}$ respects the transition function $\delta$ of $M$.

Now we can explain the first main step of our proof.

It is well known that 2CMs can simulate the computations of Turing Machines,
and therefore that they accept the class of recursively enumerable languages.
Hence, we obtain from Rice’s theorem that it is undecidable whether the
language accepted by a 2CM contains infinitely many words from $\\{0\\}^{+}$
or not, where $0\in\Delta$. Moreover, since 2CMs are deterministic, each word
accepted by a given 2CM has exactly one valid computation history. So, it
follows that the set of words from $\\{0\\}^{+}$ accepted by a 2CM $M$ is
finite if and only if the set $S_{M}=\\{C\mid C$ is a valid computation
history for $M$ on some input word $w\in\\{0\\}^{+}\\}$ is finite.

Moreover, it is easily seen that the set $S_{M}$ is finite if and only if it
is regular. Clearly, if it is finite, it is regular. To see the converse,
suppose for contradiction that it is both infinite and regular. Then there is
a DFA accepting $S_{M}$, and moreover, there exist arbitrarily long words in
$S_{M}$. If we choose a word which is sufficiently long, then there must exist
distinct positions in that word which occur after the initial configuration
and such that the DFA accepting $S_{M}$ must be in the same state after
reading the prefix up to those positions. It follows that the part between
these two positions can be pumped any number of times without affecting
acceptance (and hence membership in $S_{M}$). However, this would either
disrupt the correct form of a valid computation history for the particular
input word (which is fixed by the first configuration), or it would result in
infinitely many valid computation histories for the same input word, which
contradicts the fact that $M$ is deterministic. In both cases, we get a
contradiction, so if $S_{M}$ is infinite, it is not regular.

We can now proceed with the second main part of our proof, which is
essentially a computation-simulation. Interestingly, our tools for this part
of the proof are fundamentally different from those used in Theorem 4.5, as we
now have to rely on techniques rooted in combinatorics on words (and word
equations) rather than on techniques related to (visibly pushdown) automata.

Next, we note that $S_{M}$ is regular if and only if its complement is
regular. In what remains, we shall construct, for any given 2CM $M$, a
$\operatorname{WE}$ formula $f$ containing a variable $x$ such that the
language expressed by $x$ in $f$ is exactly the complement of $S_{M}$. This
construction facilitates a reduction from the finiteness problem described at
the beginning of the proof to the problem of whether or not the language
expressed by a variable in a $\operatorname{WE}$ formula is regular.

Let us fix a 2CM $M$. We construct the formula $f$ as the disjunction of 4
subformulas, each of which accounts for a particular way in which a word
substituted for $x$ could violate the definition of a valid computation
history of $M$ on an input of the form $0^{+}$. Let
$x,y_{1},y_{2},y_{3},y_{4},z_{1},z_{2},z_{3},z_{4},u,u^{\prime},v,v^{\prime},w,w^{\prime}$
be variables.

Throughout the construction we shall repeatedly use the well-known fact (see
the Defect Theorem in [32] that for two words $w_{1},w_{2}$, we have
$w_{1}w_{2}=w_{2}w_{1}$ if and only if they are repetitions of the same word,
that is there exists a word $w_{3}$ and $p,q\in\mathbb{N}$ such that
$w_{1}=w_{3}^{p}$ and $w_{2}=w_{3}^{q}$.

Now, $f$ is the formula

$w0=0w\land w=0w^{\prime}\land(f_{1}\lor f_{2}\lor f_{3}\lor f_{4})$

where $f_{1},f_{2},f_{3},f_{4}$ are defined below. The first two conjuncts
enforce that $w\in 0^{+}$. This allows us to use $w$ to represent the input
word in the rest of the formula. $f_{1}$ will be satisfiable for a given value
of $x$ if $x$ does not belong to
$q_{0}0^{+}a^{+}b^{+}c^{+}(Q0^{+}a^{+}b^{+}c^{+})^{*}$, and thus that it is
not a sequence of configurations of $M$ starting in an initial state. $f_{2}$
and $f_{3}$ will cover the cases when $x$ does not start with the initial
configuration for $M,w$ and when $x$ does not end with a final configuration
respectively. Finally $f_{4}$ will cover the case that two consecutive
configurations in $x$ do not respect the transition relation $\delta$.

Let $P$ be the set of pairs of letters which may not occur consecutively in
$(Q0^{+}a^{+}b^{+}c^{+})^{+}$. That is, $P$ is the complement of $Q0\cup
cQ\cup\\{00,0a,aa,ab,bb,bc,cc\\}$. Note that $x$ is not in the language
$q_{0}0^{+}a^{+}b^{+}c^{+}(Q0^{+}a^{+}b^{+}c^{+})^{*}$ if and only if it
contains consecutive letters included in $P$ or it starts with a letter other
than $q_{0}$ or it ends with a letter other than $c$. Note that $P$ is finite.
Thus the subformula $f_{1}$ is given by

$\bigvee\limits_{AB\in
P}x=uABv\lor\bigvee\limits_{A\in\Sigma\backslash\\{q_{0}\\}}x=Au\lor\bigvee\limits_{A\in\Sigma\backslash
F}x=uA\lor x=\varepsilon.$

With $f_{2}$, we want to enforce that it is true only if $x$ has a prefix
other than the initial configuration, namely $q_{0}wabc$. We only need to
cover cases when $f_{1}$ is not satisfied (so we may assume that $x$ belongs
to $q_{0}0^{+}a^{+}b^{+}c^{+}(Q0^{+}a^{+}b^{+}c^{+})^{*}$. Thus $f_{2}$ is
given as:

$\displaystyle u0=0u$
$\displaystyle\land(\bigvee\limits_{A_{1}A_{2}A_{3}\not=abc\land
A_{1}\not=0}x=q_{0}uA_{1}A_{2}A_{3}v$
$\displaystyle\lor(x=q_{0}uav\land(w=u0u^{\prime}\lor w0u^{\prime}=u))).$

In the above formula, $u$ must be the complete sequence of $0$s occurring
after $q_{0}$. The cases when the next three letters after $u$ are not $abc$
and when $u\not=w$ are then covered by the second and third lines.

$f_{2}$ can be constructed similarly as follows:

$u0=0u\land\left(\bigvee\limits_{A_{0}A_{1}A_{2}A_{3}\not=0abc}x=vA_{0}A_{1}A_{2}A_{3}\lor\bigvee\limits_{q\in
Q\backslash F}x=vquabc\right).$

The first of the two disjuncts inside the brackets covers all cases when $x$
does not end with a configuration of the form $q0^{*}abc$, or in other words
when all tape heads have not returned to their leftmost positions. The second
disjunct covers the cases when tape heads are in their leftmost positions but
the state is not final.

Finally we construct $f_{4}$ as

$\displaystyle\bigvee\limits_{q,q^{\prime}\in Q}$
$\displaystyle(x=uqy_{1}y_{2}y_{3}y_{4}q^{\prime}z_{1}z_{2}z_{3}z_{4}v\land$
$\displaystyle y_{1}0=0y_{1}\land$ $\displaystyle y_{2}a=ay_{2}\land$
$\displaystyle y_{3}b=by_{3}\land$ $\displaystyle y_{4}c=cy_{4}\land$
$\displaystyle z_{1}0=0y_{1}\land$ $\displaystyle z_{2}a=az_{2}\land$
$\displaystyle z_{3}b=bz_{3}\land$ $\displaystyle z_{4}c=cz_{4}\land$
$\displaystyle(y_{1}0u^{\prime}=z_{1}\lor y_{1}=z_{1}0u^{\prime}\lor$
$\displaystyle y_{2}aau^{\prime}=z_{2}\lor y_{2}=z_{2}aau^{\prime}\lor$
$\displaystyle y_{3}bbu^{\prime}=z_{3}\lor y_{3}=z_{3}bbu^{\prime}\lor$
$\displaystyle y_{4}ccu^{\prime}=z_{4}\lor y_{4}=z_{4}ccu^{\prime})\lor$
$\displaystyle\bigvee\limits_{f^{\prime}\in D}f^{\prime})$

where $D$ is a set of formulas describing transitions which are not possible
in $M$, which is again given below. Essentially the first 9 lines of $f_{4}$
enforces that $qy_{1}y_{2}y_{3}y_{4}$ and $q^{\prime}z_{1}z_{2}z_{3}z_{4}$ are
consecutive configurations in $x$ and that $q,q^{\prime}$ represent states,
while $y_{1},z_{1}$ are the part containing $0$’s, $y_{2},z_{2}$ contain the
$a$’s $y_{3},z_{3}$ contain the $b$’s and $y_{4}z_{4}$ contain the $c$’s. The
10th line accounts for when the input word is not correctly copied from the
first configuration to the next, while the 11th, 12th and 13th lines account
for when one of the tape heads moves two or more positions.

Thus the formulas from $D$ must cover the cases when the input is copied
correctly and all tape heads move at most one position, but the transition is
still not valid. Thus $D$ contains the following formula where
$B_{2}=a,B_{3}=b,B_{4}=c$, which covers the case that two tape heads move at
the same time.

$\displaystyle\bigvee\limits_{i,j\in\\{2,3,4\\}\land
i\not=j}((y_{i}B_{i}=z_{i}\lor y_{i}=z_{i}B_{i})\land(y_{j}B_{j}=z_{j}\lor
y_{j}=z_{j}B_{j}))$

Moreover, for every "legal" transition not specified by $\delta$ (so every
transition having the correct form but not allowed in the specific 2CM $M$),
$D$ contains a formula describing this transition. We provide an example in
the case that the transition $\delta(q_{1},0,T,F)=(q_{2},2,L)$ is present in
$M$. The example can easily be adapted for other combinations. The formula
will enforce that if the current state in the first configuration is $q_{1}$,
and the first counter is $0$ while the second is not (we only need to consider
cases where the input letter is $0$), then the next configuration should not
have state $q_{2}$, or should increment the second counter or leave it
unchanged, or should change either the first counter or the input tape head
position. This covers all possible ways the transition
$\delta(q_{1},0,T,F)=(q_{2},2,L)$ is not respected. Formally the formula is
given as:

$\displaystyle q=q_{1}\land y_{3}=b\land y_{4}=bbv^{\prime}\land$
$\displaystyle(\bigvee\limits_{q_{2}^{\prime}\in
Q\backslash\\{q_{2}\\}}q^{\prime}=q_{2}^{\prime}\lor$ $\displaystyle
y_{2}=z_{2}a\lor y_{2}a=z_{2}\lor$ $\displaystyle y_{4}=z_{4}c\lor
y_{4}c=z_{4}\lor$ $\displaystyle y_{3}=z_{3}\lor y_{3}=z_{3}b).$

The first line establishes the appropriate conditions of the first
configuration, while the second line covers cases where the second
configuration has the wrong state, the third and fourth lines covers the case
that one of the wrong tape heads moves while the final line covers the case
that the correct tape head moves in the wrong direction or not at all.
Inclusion of similar formulas in $D$ for other transitions completes the
construction of $f$.

All together, we have shown a construction for a formula $f$ which can be
satisfied for a particular value of $x$ if and only if $x$ is not a valid
computation history for $M$ on input word of the form $0^{+}$. In other words,
the language expressed by $x$ in $f$ is exactly the complement of $S_{M}$.
Thus it is regular if and only if $M$ accepts only finitely many words from
$0^{+}$. This completes the reduction and we may conclude that the problem of
deciding whether a formula and variable from $\operatorname{WE}$ express a
regular language is undecidable as claimed.

Although a trivial consequence of Theorem 6.3, is is somehow surprising that
it remains undecidable if a word equation combined with regular constraints
expresses a regular language.

Finally, we note the remaining cases which correspond to removing regular
language membership constraints in the presence of word equations, and
removing length constraints in the presence of word equations but without
regular constraints. Thus, we leave the following questions open:

######  Open Problem 3.

Is it decidable whether a language expressed in
$\operatorname{WE}+\operatorname{REG}$ (respectively,
$\operatorname{WE}+\operatorname{REG}+\operatorname{LEN}$) can be expressed in
$\operatorname{WE}$ (respectively, $\operatorname{WE}+\operatorname{LEN}$)? Is
it decidable whether a language expressed in
$\operatorname{WE}+\operatorname{LEN}$ can be expressed in
$\operatorname{WE}$?

## References

  * [1] P. A. Abdulla, M. F. Atig, Y. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman.  Norn: An SMT solver for string constraints.  In Proc. Computer Aided Verification (CAV), volume 9206 of Lecture Notes in Computer Science (LNCS), pages 462–469, 2015.
  * [2] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Jankŭ, Hsin-Hung Lin, Lukáš Holík, and Wei-Cheng Wu.  Efficient handling of string-number conversion.  In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 943–957, 2020.
  * [3] R. Alur and P. Madhusudan.  Visibly pushdown languages.  In Proc. 36th ACM Symposium on Theory of Computing (STOC), STOC ’04, pages 202–211, 2004.
  * [4] Rajeev Alur, Viraj Kumar, P. Madhusudan, and Mahesh Viswanathan.  Congruences for visibly pushdown languages.  In ICALP, volume 3580 of Lecture Notes in Computer Science, pages 1102–1114. Springer, 2005.
  * [5] Rajeev Alur and P. Madhusudan.  Adding nesting structure to words.  J. ACM, 56(3):16:1–16:43, 2009.
  * [6] Roberto Amadini.  A survey on string constraint solving.  ACM Computing Surveys (CSUR), 55(1):1–38, 2021.
  * [7] P. Barceló Baeza and P. Muñoz.  Graph logics with rational relations: the role of word combinatorics.  ACM Trans. Comput. Logic, 18(2), 2017.
  * [8] C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, and C. Tinelli.  CVC4.  In Proc. Computer Aided Verification (CAV), volume 6806 of Lecture Notes in Computer Science (LNCS), pages 171–177, 2011.
  * [9] Michael Benedikt, Leonid Libkin, Thomas Schwentick, and Luc Segoufin.  Definable relations and first-order query languages over strings.  J. ACM, 50(5):694–751, 2003.
  * [10] Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D Day, Dirk Nowotka, and Vijay Ganesh.  An smt solver for regular expressions and linear arithmetic over string length.  In International Conference on Computer Aided Verification, pages 289–312. Springer, 2021.
  * [11] J. R. Büchi and S. Senger.  Definability in the existential theory of concatenation and undecidable extensions of this theory.  In The Collected Works of J. Richard Büchi, pages 671–683. Springer, 1990.
  * [12] Taolue Chen, Yan Chen, Matthew Hague, Anthony W Lin, and Zhilin Wu.  What is decidable about string constraints with the replaceall function.  Proceedings of the ACM on Programming Languages, 2(POPL):1–29, 2018\.
  * [13] Marek Chrobak.  Finite automata and unary languages.  Theor. Comput. Sci., 47(3):149–158, 1986.
  * [14] Dimitri Chubarov and Andrei Voronkov.  Basis of solutions for a system of linear inequalities in integers: Computation and applications.  In MFCS, volume 3618 of Lecture Notes in Computer Science, pages 260–270. Springer, 2005.
  * [15] J. D. Day, V. Ganesh, P. He, F. Manea, and D. Nowotka.  The satisfiability of word equations: Decidable and undecidable theories.  In I. Potapov and P. Reynier, editors, In Proc. 12th International Conference on Reachability Problems, RP 2018, volume 11123 of Lecture Notes in Computer Science (LNCS), pages 15–29, 2018.
  * [16] V. G. Durnev.  Undecidability of the positive $\forall\exists^{3}$-theory of a free semigroup.  Siberian Mathematical Journal, 36(5):917–929, 1995.
  * [17] D. D. Freydenberger.  A logic for document spanners.  Theory of Computing Systems, 63(7):1679–1754, 2019.
  * [18] D. D. Freydenberger and M. Holldack.  Document spanners: From expressive power to decision problems.  Theory of Computing Systems, 62(4):854–898, 2018.
  * [19] D. D. Freydenberger and L. Peterfreund.  The theory of concatenation over finite models.  In 48th International Colloquium on Automata, Languages, and Programming, ICALP, volume 198 of LIPIcs, pages 130:1–130:17, 2021.
  * [20] V. Ganesh, M. Minnes, A. Solar-Lezama, and M. C. Rinard.  Word equations with length constraints: What’s decidable?  In Haifa Verification Conference, 2012.
  * [21] Pawel Gawrychowski.  Chrobak normal form revisited, with applications.  In Implementation and Application of Automata - 16th International Conference, CIAA 2011. Proceedings, volume 6807 of Lecture Notes in Computer Science, pages 142–153. Springer, 2011.
  * [22] Matthew Hague.  Strings at mosca.  ACM SIGLOG News, 6(4):4–22, 2019.
  * [23] Simon Halfon, Philippe Schnoebelen, and Georg Zetzsche.  Decidability, complexity, and expressiveness of first-order logic over the subword ordering.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12. IEEE, 2017.
  * [24] John E. Hopcroft and Jeffrey D. Ullman.  Introduction to Automata Theory, Languages and Computation.  Addison-Wesley, 1979.
  * [25] A. Jeż.  Word equations in nondeterministic linear space.  In Proc. International Colloquium on Automata, Languages and Programming (ICALP), volume 80 of LIPIcs, pages 95:1–95:13, 2017.
  * [26] Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Micha Schrader.  Certistr: a certified string solver.  In CPP ’22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 210–224. ACM, 2022.
  * [27] J. Karhumäki, F. Mignosi, and W. Plandowski.  The expressibility of languages and relations by word equations.  Journal of the ACM, 47:483–505, 2000.
  * [28] A. Kiezun, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Ernst.  HAMPI: a solver for string constraints.  In Proc. ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pages 105–116. ACM, 2009.
  * [29] Quang Loc Le and Mengda He.  A decision procedure for string logic with quadratic equations, regular expressions and length constraints.  In Asian Symposium on Programming Languages and Systems, pages 350–372. Springer, 2018.
  * [30] Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett.  A decision procedure for regular membership and length constraints over unbounded strings.  In International Symposium on Frontiers of Combining Systems, pages 135–150. Springer, 2015.
  * [31] Anthony W Lin and Pablo Barceló.  String solving with word equations and transducers: towards a logic for analysing mutation xss.  In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 123–136, 2016.
  * [32] M_ Lothaire.  Combinatorics on words, volume 17.  Cambridge university press, 1997.
  * [33] M. Lothaire.  Algebraic Combinatorics on Words.  Cambridge University Press, Cambridge, New York, 2002.
  * [34] Rupak Majumdar and Anthony W Lin.  Quadratic word equations with length constraints, counter systems, and presburger arithmetic with divisibility.  Logical Methods in Computer Science, 17, 2021.
  * [35] G. S. Makanin.  The problem of solvability of equations in a free semigroup.  Sbornik: Mathematics, 32(2):129–198, 1977.
  * [36] Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka, and Vijay Ganesh.  Z3str4: A multi-armed string solver.  In Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan, editors, Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 389–406. Springer, 2021.  URL: https://doi.org/10.1007/978-3-030-90870-6_21, doi:10.1007/978-3-030-90870-6\\_21.
  * [37] Rohit J. Parikh.  On context-free languages.  J. ACM, 13(4):570–581, oct 1966.  URL: https://doi.org/10.1145/321356.321364, doi:10.1145/321356.321364.
  * [38] W. Plandowski.  Satisfiability of word equations with constants is in PSPACE.  In Proc. Foundations of Computer Science (FOCS), pages 495–500. IEEE, 1999.