Georg Zetzsche

# The complexity of downward closure comparisons

Georg Zetzsche111This work is supported by a fellowship within the Postdoc-
Program of the German Academic Exchange Service (DAAD). LSV, CNRS & ENS
Cachan, Université Paris-Saclay, France
<EMAIL_ADDRESS>
###### Abstract

The downward closure of a language is the set of all (not necessarily
contiguous) subwords of its members. It is well-known that the downward
closure of every language is regular. Moreover, recent results show that
downward closures are computable for quite powerful system models.

One advantage of abstracting a language by its downward closure is that then
equivalence and inclusion become decidable. In this work, we study the
complexity of these two problems. More precisely, we consider the following
decision problems: Given languages $K$ and $L$ from classes $\mathcal{C}$ and
$\mathcal{D}$, respectively, does the downward closure of $K$ include (equal)
that of $L$?

These problems are investigated for finite automata, one-counter automata,
context-free grammars, and reversal-bounded counter automata. For each
combination, we prove a completeness result either for fixed or for arbitrary
alphabets. Moreover, for Petri net languages, we show that both problems are
Ackermann-hard and for higher-order pushdown automata of order $k$, we prove
hardness for complements of nondeterministic $k$-fold exponential time.

##  1 Introduction

The downward closure of a language is the set of (not necessarily contiguous)
subwords of its members. It is a well-known result of [17] [17] that the
downward closure of _every_ language is regular. Of course, it is not always
possible to compute the downward closure of a given language, but oftentimes
it is. For example, it has been shown to be computable for such powerful
models as _Petri net languages_ by [14] [14] and _higher-order pushdown
automata_ by [15] [15]. A sufficient condition for computability can be found
in [34].

Moreover, not only are downward closures often computable, they are also a
meaningful abstraction of infinite-state systems. In a complex system, one can
abstract a component by the downward closure of the messages it sends to its
environment. This corresponds to the assumption that messages can be dropped
on the way. Furthermore, recent work of [25] [25] shows that among other mild
conditions, computing downward closures is sufficient for verifying safety
conditions of parametrized asynchronous shared-memory systems.

The advantage of having an abstraction of an infinite-state systems as regular
languages is that the latter offer an abundance of methods for analysis. An
important example is deciding behavioral equivalence or inclusion. This is
notoriously hard to do and for nondeterministic infinite-state systems,
language equivalence and inclusion are usually undecidable. Using downward
closures, such behavioral comparisons can be made in an approximative manner.

Despite these facts, results about the complexity of deciding whether the
downward closure of one language includes or equals that of another mainly
considered regular languages. [4] [4] have shown that the equivalence problem
for downward closures of two given NFAs is $\mathsf{coNP}$-complete. [22] [22]
strengthened $\mathsf{coNP}$-hardness to the case of DFAs over binary
alphabets and proved $\mathsf{coNP}$-completeness for the inclusion variant.
They also obtained $\mathsf{NL}$-completeness of inclusion in the case of NFAs
over a unary alphabet. Together with exponential-time downward closure
constructions [26, 7, 29, 10, 4], these results imply that equivalence and
inclusion are in $\mathsf{coNEXP}$ for context-free grammars. [33] [33] proved
that one can decide in linear time whether the downward closure of a given NFA
contains all words. Subsequently, [22] [22] showed that this problem is
$\mathsf{NL}$-complete. Similar questions have been studied for upward
closures [4, 22].

Previous work on downward closures of infinite-state systems has mainly
focused on mere computability [7, 26, 14, 15, 34, 35, 2, 1] or on
descriptional complexity [3, 11, 10, 29, 22]. This work studies the complexity
of the inclusion and the equivalence problem of downward closures between some
prominent types of system models—finite automata, one-counter automata,
reversal-bounded counter automata [19], and context-free grammars. More
precisely, we are interested in the following questions: For two system models
$\mathcal{M}$ and $\mathcal{N}$ and languages $L$ and $K$ generated by some
device in $\mathcal{M}$ and $\mathcal{N}$, respectively, what is the
complexity of  (i) deciding whether $K\mathord{\downarrow}\subseteq
L\mathord{\downarrow}$ (_downward closure inclusion problem_) or  (ii)
deciding whether $K\mathord{\downarrow}=L\mathord{\downarrow}$ (_downward
closure equivalence problem_)?

### Contribution

We determine the complexity of the downward closure inclusion problem and the
downward closure equivalence problem among finite automata, one-counter
automata, reversal-bounded counter automata (either with a fixed number of
counters and reversals or without), and context-free grammars.

For the inclusion problem, we prove completeness results in all cases except
for two. The complexities range from $\mathsf{coNP}$ over
$\Pi_{2}^{\mathsf{P}}$ to $\mathsf{coNEXP}$ (see Table 1). The two cases for
which we provide no completeness compare context-free grammars or general
reversal-bounded counter automata on the one side with reversal-bounded
counter automata with a fixed number of counters and reversals on the other
side. However, we prove that both of these problems are
$\mathsf{coNP}$-complete for each fixed input alphabet. For the equivalence
problem, the situation is similar. We prove completeness for each of the cases
except for the combination above. Again, fixing the alphabet leads to
$\mathsf{coNP}$-completeness.

The tools developed to achieve these results fall into three categories.
First, there are several generic results guaranteeing small witnesses to yield
upper bounds. Second, we prove model-specific results about downward closures
that yield the upper bounds in each case. Third, we have a general method to
prove lower bounds for downward closure comparisons. In fact, it applies to
more models than the above: We prove that for Petri net languages, the two
comparison problems are Ackermann-hard. For higher-order pushdown automata of
order $k$, we show $\mathsf{co}\mathchar 45\relax{}k\mathchar
45\relax\mathsf{NEXP}$-hardness.

### Related work

Another abstraction of formal languages is the well-known Parikh image [30].
The Parikh image of a language $L\subseteq X^{*}$ contains for each word $w\in
L$ a vector in $\mathbb{N}^{|X|}$ that counts the number of occurrences of
each letter. For some language classes, it is known that their Parikh image is
effectively semilinear, which implies decidability of the inclusion and
equivalence problem for Parikh images. The investigation of these problems’
complexity has been initiated by [18] [18] in 1985, who showed that this
problem is $\Pi_{2}^{\mathsf{P}}$-hard and in $\mathsf{coNEXP}$ for regular
and context-free languages. [24] [23, 24] have then shown that these problems
are $\Pi_{2}^{\mathsf{P}}$-complete for fixed alphabets. Only very recently,
[13] [13] have shown that the case of general alphabets is
$\mathsf{coNEXP}$-complete.

##  2 Concepts and Results

| $\mathsf{Ideal}$ | $\mathsf{NFA}$ | $\mathsf{OCA}$ | $\mathsf{RBC}_{k,r}$ | $\mathsf{CFG}$ | $\mathsf{RBC}$
---|---|---|---|---|---|---
$\mathsf{Ideal}$ | $\in\mathsf{L}$ | $\mathsf{NL}$ | $\mathsf{NL}$ | $\mathsf{NL}$ | $\mathsf{P}$ | $\mathsf{NP}$
$\mathsf{NFA}$ | $\mathsf{NL}$ |  $\mathsf{coNP}$ [4, 22] |  $\mathsf{coNP}$ [4, 22, 3] | $\mathsf{coNP}$ | $\mathsf{coNP}$ | $\Pi_{2}^{\mathsf{P}}$
$\mathsf{OCA}$ | $\mathsf{NL}$ |  $\mathsf{coNP}$ [4, 22, 3] |  $\mathsf{coNP}$ [4, 22, 3] | $\mathsf{coNP}$ | $\mathsf{coNP}$ | $\Pi_{2}^{\mathsf{P}}$
$\mathsf{RBC}_{k,r}$ | $\mathsf{NL}$ | $\mathsf{coNP}$ | $\mathsf{coNP}$ | $\mathsf{coNP}$ | $\mathsf{coNP}$ | $\Pi_{2}^{\mathsf{P}}$
$\mathsf{CFG}$ | $\mathsf{P}$ | $\mathsf{coNP}$ | $\mathsf{coNP}$ | $\mathsf{coNP}^{\dagger}$ | $\mathsf{coNEXP}$ | $\mathsf{coNEXP}$
$\mathsf{RBC}$ | $\mathsf{coNP}$ | $\mathsf{coNP}$ | $\mathsf{coNP}$ | $\mathsf{coNP}^{\dagger}$ | $\mathsf{coNEXP}$ | $\mathsf{coNEXP}$
Table 1: Complexity of the inclusion problem. The entry in row $\mathcal{M}$
and column $\mathcal{N}$ is the complexity of
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathcal{N}$. Except in the case
$\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{Ideal}$, all entries
indicate completeness. A $\dagger$ means that the entry refers to the fixed
alphabet case (for at least two letters).

If $X$ is an alphabet, $X^{*}$ ($X^{\leq n}$) denotes the set of all words (of
length $\leq n$) over $X$. The empty word is denoted by $\varepsilon\in
X^{*}$. For words $u,v\in X^{*}$, we write $u\preceq v$ if $u=u_{1}\cdots
u_{n}$ and $v=v_{0}u_{1}v_{1}\cdots u_{n}v_{n}$ for some
$u_{1},\ldots,u_{n},v_{0},\ldots,v_{n}\in X^{*}$. It is well-known that
$\preceq$ is a well-quasi-order on $X^{*}$ and that therefore the _downward
closure_ $L\mathord{\downarrow}=\\{u\in X^{*}\mid\exists v\in L\colon u\preceq
v\\}$ is regular for every $L\subseteq X^{*}$ [17]. An _ideal_ is a set of the
form
$Y_{0}^{*}\\{x_{1},\varepsilon\\}Y_{1}^{*}\cdots\\{x_{n},\varepsilon\\}Y_{n}^{*}$,
where $Y_{0},\ldots,Y_{n}$ are alphabets and $x_{1},\ldots,x_{n}$ are letters.
We will make heavy use of the fact that every downward closed language can be
written as a finite union of ideals, which was first discovered by [21] [21].
By $\mathbb{P}(S)$, we denote the powerset of the set $S$.

A _finite automaton_ is a tuple $\mathcal{A}=(Q,X,\Delta,q_{0},Q_{f})$, where
$Q$ is a finite set of _states_ , $X$ is its input alphabet, $\Delta\subseteq
Q\times X^{*}\times Q$ is a finite set of _edges_ , $q_{0}\in Q$ is its
_initial state_ , and $Q_{f}\subseteq Q$ is the set of its _final states_. The
language accepted by $\mathcal{A}$ is denoted $L(\mathcal{A})$. Sometimes, we
write $|\mathcal{A}|$ for the number of states of $\mathcal{A}$.

A _context-free grammar_ is a tuple $\mathcal{G}=(N,T,P,S)$ where $N$ and $T$
are pairwise disjoint alphabets, whose members are called the _nonterminals_
and _terminals_ , respectively. $S\in N$ is the _start symbol_ and $P$ is the
finite set of _productions_ of the form $A\to w$ with $A\in N$ and $w\in
T^{*}$. The language generated by $\mathcal{G}$ is defined as usual.

### One-counter Automata

A _one-counter automaton (OCA)_ is a nondeterministic finite automaton that
has access to one counter that assumes natural numbers as values. The possible
operations are _increment_ , _decrement_ , and _test for zero_. We will not
require a formal definition, since in fact, all we need is the well-known fact
that membership and emptiness are $\mathsf{NL}$-complete and the recent result
that given an OCA $\mathcal{A}$, one can compute in polynomial time an NFA
$\mathcal{B}$ with $L(\mathcal{B})=L(\mathcal{A})\mathord{\downarrow}$ [3].

### Reversal-bounded counter automata

Intuitively, an _$r$ -reversal-bounded $k$-counter automaton_ [19] (short
$(k,r)$-RBCA) is a nondeterministic finite automaton with $k$ counters that
can store natural numbers. For each counter, it has operations _increment_ ,
_decrement_ , and _zero test_. Moreover, a computation is only valid if each
counter _reverses_ at most $r$ times. Here, a computation _reverses_ a counter
$c$ if on $c$, it first executes a sequence of increments and then a decrement
command or vice versa. See [19] for details.

Instead of working directly with RBCA, we will work here with the model of
_blind counter automata_ [9]. It is not as well-known as RBCA, but simpler and
directly amenable to linear algebraic methods. A _blind $k$-counter automaton_
is a tuple $\mathcal{A}=(Q,X,q_{0},\Delta,Q_{f})$, where $Q$, $X$, $q_{0}$,
and $Q_{f}$ are defined as in NFAs, but $\Delta$ is a finite subset of
$Q\times(X\cup\\{\varepsilon\\})\times\\{-1,0,1\\}^{k}\times Q$. A _walk_ is a
word $\delta_{1}\cdots\delta_{m}\in\Delta^{*}$ where
$\delta_{i}=(p_{i},x_{i},d_{i},p^{\prime}_{i})$ for $i\in[1,m]$ and
$p^{\prime}_{j}=p_{j+1}$ for $j\in[1,m-1]$. The _effect_ of the walk is
$d_{1}+\cdots+d_{m}$. Its _input_ is $x_{1}\cdots x_{m}\in X^{*}$. If the walk
has effect $0$ and $p_{0}=q_{0}$ and $p_{m}\in Q_{f}$, then the walk is
_accepting_. The _language accepted by $\mathcal{A}$_ is the set of all inputs
of accepting walks.

Using blind counter automata is justified because to each $(k,r)$-RBCA, one
can construct in logarithmic space a language-equivalent $(kr,1)$-RBCA [5],
which is essentially a blind $kr$-counter automaton. On the other hand, every
blind $k$-counter automaton can be turned in logarithmic space into a
$(k+1,1)$-RBCA [20]. Hence, decision problems about $(k,r)$-RBCA for fixed $k$
and $r$ correspond to problems about blind $k$-counter automata for fixed $k$.

In the following, by a _model_ , we mean a way of specifying a language. In
order to succinctly refer to the different decision problems, we use symbols
for the models above. By $\mathsf{Ideal}$, $\mathsf{NFA}$, $\mathsf{OCA}$,
$\mathsf{RBC}_{k,r}$, $\mathsf{RBC}$, $\mathsf{CFG}$, we mean ideals, finite
automata, OCA, RBCA with a fixed number of counters and reversals, general
RBCA, and context-free grammars, respectively. Then, for
$\mathcal{M},\mathcal{N}\in\\{\mathsf{Ideal},\mathsf{NFA},\mathsf{OCA},\mathsf{RBC}_{k,r},\mathsf{RBC},\mathsf{CFG}\\}$,
we consider the following problems. In the _downward closure inclusion
problem_ $\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathcal{N}$, we are
given a language $K$ in $\mathcal{M}$ and a language $L$ in $\mathcal{N}$ and
are asked whether $K\mathord{\downarrow}\subseteq L\mathord{\downarrow}$. For
the _downward closure equivalence problem_
$\mathcal{M}=_{\mathord{\downarrow}}\mathcal{N}$, the input is the same, but
we are asked whether $K\mathord{\downarrow}=L\mathord{\downarrow}$.

### Results

The complexity results for the inclusion problem are summarized in Table 1.
For the equivalence problem, we will see that every hardness result for
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathcal{N}$ also holds for
$\mathcal{M}=_{\mathord{\downarrow}}\mathcal{N}$. Since for non-ideal models,
the appearing complexity classes are pairwise comparable, this implies that
the complexity for $\mathcal{M}=_{\mathord{\downarrow}}\mathcal{N}$ is then
the harder of the two classes for
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathcal{N}$ and
$\mathcal{N}\subseteq_{\mathord{\downarrow}}\mathcal{M}$. For example, the
problem $\mathsf{NFA}=_{\mathord{\downarrow}}\mathsf{RBC}$ is
$\Pi_{2}^{\mathsf{P}}$-complete and for fixed alphabets,
$\mathsf{RBC}_{k,r}=_{\mathord{\downarrow}}\mathsf{CFG}$ is
$\mathsf{coNP}$-complete.

##  3 Ideals and Witnesses

Our algorithms for inclusion use three types of witnesses. The first type is a
slight variation of a result of [4]. The latter authors were interested in
equivalence problems, which caused their bound to depend on both input
languages. The proof is essentially the same.

######  Proposition 3.1 (Short witness).

If $\mathcal{A}$ is an NFA and $K\mathord{\downarrow}\not\subseteq
L(\mathcal{A})\mathord{\downarrow}$, then there exists a $w\in
K\mathord{\downarrow}\setminus L(\mathcal{A})\mathord{\downarrow}$ with
$|w|\leq|\mathcal{A}|+1$.

The other types of witnesses strongly rely on ideals, which requires some
notation. An ideal is a product
$I=Y_{0}^{*}\\{x_{1},\varepsilon\\}Y_{1}^{*}\cdots\\{x_{n},\varepsilon\\}Y_{n}^{*}$
where the $Y_{i}$ are alphabets and the $x_{i}$ are letters. Its _length_
$|I|_{\mathsf{I}}$ is the smallest $n$ such that $I$ can be written in this
form. Since every downward closed language can be written as a finite union of
ideals, we can extend this definition to languages: $|L|_{\mathsf{I}}$ is the
smallest $n$ such that $L\mathord{\downarrow}$ is a union of ideals of length
$\leq n$.

Sometimes, it will be convenient to work with a different length measure of
ideals. An _ideal expression (of length $n$)_ is a product $L_{1}\cdots
L_{n}$, where each $L_{i}$ is of the form $Y^{*}$ or $\\{x,\varepsilon\\}$,
where $Y$ is an alphabet and $x$ is a letter. Note that
$Y^{*}=Y^{*}\\{x,\varepsilon\\}$ if $x\in Y$ and
$\\{x,\varepsilon\\}=\emptyset^{*}\\{x,\varepsilon\\}$. Therefore, an ideal
expression of length $n$ defines an ideal of length $\leq n$. In analogy to
$|\cdot|_{\mathsf{I}}$, for a language $L$, we define its _expression length_
$|L|_{\mathsf{E}}$ to be the smallest $n$ such that $L\mathord{\downarrow}$
can be written as a finite union of ideal expressions of length $\leq n$. The
expression length has the advantage of being subadditive: For languages $K,L$
we have $|KL|_{\mathsf{E}}\leq|K|_{\mathsf{E}}+|L|_{\mathsf{E}}$. Moreover, we
have $|L|_{\mathsf{I}}\leq|L|_{\mathsf{E}}\leq 2|L|_{\mathsf{I}}+1$.

The measure $|\cdot|_{\mathsf{I}}$ turns out to be instrumental for the
inclusion problem. Note that $K\mathord{\downarrow}\not\subseteq
L\mathord{\downarrow}$ if and only if there is an ideal $I\subseteq
K\mathord{\downarrow}$ of length $\leq|K|_{\mathsf{I}}$ with $I\not\subseteq
L\mathord{\downarrow}$. We can therefore guess ideals and check inclusion for
them. From now on, we assume alphabets to come linearly ordered. This means
for every alphabet $Y$, there is a canonical word $w_{Y}$ in which every
letter from $Y$ occurs exactly once.

######  Proposition 3.2 (Ideal witness).

Let
$I=Y_{0}^{*}\\{x_{1},\varepsilon\\}Y_{1}^{*}\cdots\\{x_{n},\varepsilon\\}Y_{n}^{*}$.
Then the following are equivalent:  (i) $I\subseteq L\mathord{\downarrow}$.
(ii) $w_{Y_{0}}^{m}x_{1}w_{Y_{1}}^{m}\cdots x_{n}w_{Y_{n}}^{m}\in
L\mathord{\downarrow}$for every $m\geq|L|_{\mathsf{I}}+1$.  (iii)
$w_{Y_{0}}^{m}x_{1}w_{Y_{1}}^{m}\cdots x_{n}w_{Y_{n}}^{m}\in
L\mathord{\downarrow}$for some $m\geq|L|_{\mathsf{I}}+1$.

A word of the form $w_{Y_{0}}^{m}x_{1}w_{Y_{1}}^{m}\cdots
x_{n}w_{Y_{n}}^{m}\in L\mathord{\downarrow}$ with $m\geq|L|_{\mathsf{I}}+1$ is
therefore called an _ideal witness for $I$ and $L$_. The proof of Proposition
3.2 is a simple pumping argument based on the fact that an ideal of length
$\leq m$ admits an NFA with $\leq m+1$ states. Ideal witnesses are useful when
we have a small bound on $|K|_{\mathsf{I}}$ and $|L|_{\mathsf{I}}$ but only a
large bound on the NFA size of $L\mathord{\downarrow}$. Observe that putting a
bound on $|L|_{\mathsf{I}}$ amounts to proving a pumping lemma: We have
$|L|_{\mathsf{I}}\leq n$ if and only if for every $w\in L$, there is an ideal
$I$ with $|I|_{\mathsf{I}}\leq n$ and $x\in I\subseteq L\mathord{\downarrow}$.

However even if, say, $|K|_{\mathsf{I}}$ is polynomial and $|L|_{\mathsf{I}}$
is exponential, ideal witnesses can be stored succinctly in polynomial space,
by keeping a binary representation of the power $m$. For instance, this will
be used in the case
$\mathsf{NFA}\subseteq_{\mathord{\downarrow}}\mathsf{RBC}$.

Sometimes, we have a small bound on $|L|_{\mathsf{I}}$, but $|K|_{\mathsf{I}}$
may be large. Then, ideal witnesses are too large to achieve an optimal
algorithm. In these situations, we can guarantee smaller witnesses if we fix
the alphabet.

######  Proposition 3.3 (Small alphabet witness).

Let $K,L\subseteq X^{*}$. If $K\mathord{\downarrow}\not\subseteq
L\mathord{\downarrow}$, then there exists a $w\in
K\mathord{\downarrow}\setminus L\mathord{\downarrow}$ with
$|w|\leq|X|\cdot(|L|_{\mathsf{I}}+1)^{|X|}$.

The proof of Proposition 3.3 is more involved than Propositions 3.2 and 3.1.
Note that a naive bound can be obtained by intersecting exponentially (in
$|L|_{\mathsf{I}}$) many automata for the ideals of $L\mathord{\downarrow}$
and complementing the result. This would yield a doubly exponential (in
$|L|_{\mathsf{I}}$) bound, even considering the fact that ideals have linear-
sized DFAs. We can, however, use the latter fact in a different way.

A DFA is _ordered_ if its states can be partially ordered so that for every
transition $p\xrightarrow{x}q$, we have $p\leq q$. In other words, the
automaton is acyclic except for loop transitions. The following Lemma is easy
to see: In order to check membership in an ideal, one just has to keep a
pointer into the expression that never moves left.

######  Lemma 3.4.

Given an ideal representation of length $n$, one can construct in logarithmic
space an equivalent ordered DFA with $n+2$ states.

An ordered DFA _cycles_ at a position of an input word if that position is
read using a loop. The following Lemma is the key idea behind Proposition 3.3.
Together with Lemma 3.4, it clearly implies Proposition 3.3. For unary
alphabets, it is easy to see. We use induction on $|X|$ and show, roughly
speaking, that without such a position, no strict subalphabet can be used for
too long. Then, all letters have to appear often, meaning a state has to
repeat after seeing the whole alphabet. Hence, the automaton stays in this
state until the end.

######  Lemma 3.5.

If $w\in X^{*}$ with $|w|>|X|\cdot(n-1)^{|X|}$, then $w$ has a position at
which every ordered $n$-state DFA cycles.

##  4 Insertion trees

In Section 5, we will show upper bounds for the size of downward closure NFAs
and for ideal lengths for counter automata. These results employ certain
decompositions of NFA runs into trees, which we discuss here.

Let $\mathcal{A}=(Q,X,\Delta,q_{0},Q_{f})$ be a finite automaton. A _walk_ is
a word $w=\delta_{1}\cdots\delta_{m}\in\Delta^{*}$ where
$\delta_{i}=(p_{i},x_{i},p^{\prime}_{i})$ for $i\in[1,m]$ and
$p^{\prime}_{j}=p_{j+1}$ for $j\in[1,m-1]$. The walk is a _( $p_{1}$-)cycle_
if $p_{1}=p^{\prime}_{m}$. In this case, we define $\sigma(w):=p_{1}$. A cycle
is _prime_ if $p_{i}=p_{1}$ implies $i=1$. A cycle is _simple_ if
$p_{i}=p_{j}$ implies $i=j$. A state $q$ _occurs_ on the cycle if $p_{i}=q$
for some $i$. If $i\neq 1$, then $q$ occurs _properly_.

A common operation in automata theory is to take a run and delete cycles until
the run has length at most $|Q|$. The idea behind an insertion tree is to
record where we deleted which cycles. This naturally leads to a tree.

For our purposes, trees are finite, unranked and ordered. An _insertion tree_
is a tree $t=(V,E)$ together with a map $\gamma\colon V\to\Delta^{*}$ that
assigns to each vertex $v\in V$ a simple cycle $\gamma(v)$ such that if $u$ is
the parent of $v$, then $\sigma(\gamma(v))$ properly occurs in $\gamma(u)$.
Note that we allow multiple children for a state that occurs in $\gamma(u)$.

Since $t$ is ordered and in every simple cycle there is at most one proper
occurrence of each state, an insertion tree defines a unique (typically not
simple) cycle $\alpha(t)$. Formally, if $t$ is a single vertex $v$, then
$\alpha(t):=\gamma(v)$. If $t$ consists of a root $r$ and subtrees
$t_{1},\ldots,t_{s}$, then $\alpha(t)$ is obtained by inserting each
$\alpha(t_{i})$ in $\gamma(r)$ at the (unique) occurrence of
$\sigma(\alpha(t_{i}))$. The _height_ of an insertion tree is the height of
its tree.

######  Lemma 4.1.

Every prime cycle of $\mathcal{A}$ admits an insertion tree of height at most
$|Q|$.

The idea is to pick a cycle $c$ strictly contained in the prime cycle, but of
maximal length. Then, after removing $c$, no state occurs both before and
after the old position of $c$. This forces any insertion tree $t$ of the
remainder to place this position in the root. We then apply induction to the
subtrees of $t$ and to $c$. The resulting trees can then all be attached to
the root, increasing the height by at most one.

One application of Lemma 4.1 is to construct short ideals in a pumping lemma
for counter automata. Part of this construction is independent from counters,
so we stay with NFAs for a moment. Suppose we have an insertion tree $t=(V,E)$
with map $\gamma\colon V\to\Delta^{*}$ and a subset $F\subseteq V$, whose
members we call _fixed vertices_ or _fixed cycles_. Those in $V\setminus F$
are called _pumpable vertices/cycles_.

We use fixed and pumpable vertices to guide a pumping process as follows. A
sequence $s=t_{1}\cdots t_{m}$ of insertion trees is called _compatible_ if
$\sigma(\alpha(t_{1}))=\cdots=\sigma(\alpha(t_{m}))$. We assume that we have a
global set $F$ of vertices that designates the fixed vertices for all these
trees. Suppose $v$ is a pumpable vertex. We obtain new compatible sequences in
two ways:

  * •

Let $v_{1},\ldots,v_{\ell}$ be the children of $v$. We choose $i\in[0,\ell]$
and split up $v$ at $i$, meaning that we create a new vertex $v^{\prime}$ with
$\gamma(v^{\prime})=\gamma(v)$ to the right of $v$ and move
$v_{i+1},\ldots,v_{\ell}$ (and, of course, their subtrees) to $v^{\prime}$.

  * •

If the whole subtree under $v$ is pumpable (we call such subtrees _pumpable_),
then we can duplicate this subtree and attach its root somewhere as a sibling
of $v$.

If $v$ is a root, these operations mean that we introduce a new tree in the
sequence. If a compatible sequence $s^{\prime}$ is obtained from $s$ by
repeatedly performing these operations, we say that $s^{\prime}$ is obtained
by _pumping $s$_. This allows us to define the following language:

$P(t_{1}\cdots
t_{m},F)=\\{\iota(\alpha(t^{\prime}_{1})\cdots\alpha(t^{\prime}_{k}))\mid\text{$t^{\prime}_{1}\cdots
t^{\prime}_{k}$ results from pumping $t_{1}\cdots t_{m}$}\\}.$

Here, for a walk $w$, $\iota(w)$ denotes the input word read by $w$. The
following Lemma will yield the desired short ideals.

######  Lemma 4.2.

Let $s=t_{1}\cdots t_{m}$ be a compatible sequence of insertion trees of
height $\leq h$ and let $F$ be a set of fixed vertices. Then, the language
$P(s,F)\mathord{\downarrow}$ is an ideal that satisfies
$|P(s,F)\mathord{\downarrow}|_{\mathsf{E}}\leq h|F|(2|Q|+|F|)^{2}$.

Roughly speaking, the pumping process is designed so that pumpable subtrees
only cause alphabets $Y$ in factors $Y^{*}$ of the ideal to grow and thus do
not affect the ideal length. Hence, the only vertices that contribute to the
length are those that are ancestors of vertices in $F$. Since the trees have
height $\leq h$, there are at most $h|F|$ such ancestors.

##  5 Counter Automata

In this section, we construct downward closure NFAs for counter automata and
prove upper bounds for ideal lengths. Mere computability of downward closures
of blind counter automata can be deduced from computability for Petri net
languages [14]. However, that necessarily results in non-primitive recursive
automata (see Section 8). As a special case of stacked counter automata, blind
counter automata were provided with a new construction method in [35]. That
algorithm, however, yields automata of non-elementary size. Here, we prove an
exponential bound.

######  Theorem 5.1.

For each $n$-state blind $k$-counter automaton $\mathcal{A}$, there is an NFA
$\mathcal{B}$ with $L(\mathcal{B})=L(\mathcal{A})\mathord{\downarrow}$ and
$|\mathcal{B}|\leq(3n)^{5nk+7k^{3}}$. Moreover, $\mathcal{B}$ can be computed
in exponential time.

### Linear Diophantine equations

In order to show correctness of our construction, we employ a result of [31]
[31], which bounds the norm of minimal non-negative solutions to a linear
Diophantine equation. Let $A\in\mathbb{Z}^{k\times m}$ be an integer matrix.
We write $\|A\|_{1,\infty}$ for $\sup_{i\in[1,k]}(\sum_{j\in[1,m]}|a_{ij}|)$,
where $a_{ij}$ is the entry of $A$ at row $i$ and column $j$. A solution
$x\in\mathbb{N}^{m}$ to the equation $Ax=0$ is _minimal_ if there is no
$y\in\mathbb{N}^{m}$ with $Ay=0$ and $y\leq x$, $y\neq x$. The set of all
solutions clearly forms a submonoid of $\mathbb{N}^{m}$, which is denoted $M$.
The set of minimal solutions is denoted $\mathcal{H}(M)$ and called the
_Hilbert basis_ of $M$. Let $r$ be the rank of $A$. Pottier showed the
following.

######  Theorem 5.2 ([31] [31]).

For each $x\in\mathcal{H}(M)$, $\|x\|_{1}\leq(1+\|A\|_{1,\infty})^{r}$.

By applying Theorem 5.2 to the matrix $(A|-b)$, it is easy to deduce that for
each $x\in\mathbb{N}^{m}$ with $Ax=b$, there is a $y\in\mathbb{N}^{m}$ with
$Ay=b$, $y\leq x$, and $\|y\|_{1}\leq(1+\|(A|-b)\|_{1,\infty})^{r+1}$.

### Automata for the downward closure

Let $\mathcal{A}$ be a blind $k$-counter automaton with $n$ states. The idea
of the construction of $\mathcal{B}$ is to traverse insertion trees of prime
cycles of $\mathcal{A}$. Although insertion trees were introduced for finite
automata, they also apply to blind counter automata if we regard the counter
updates as input symbols. $\mathcal{B}$ keeps track of where it is in the tree
using a stack of bounded height. The stack alphabet will be
$\Gamma=Q\times[-n,n]^{k}$. We define $B=n+n\cdot(3n)^{(k+1)^{2}}$. The state
set of our automaton $\mathcal{B}_{1}$ is the following:

$Q_{1}=Q\times\Gamma^{\leq
n}\times[-B,B]^{k}\times\mathbb{P}([-n,n]^{k})\times\mathbb{P}([-n,n]^{k}).$

Here, the number of states is clearly doubly exponential, but we shall make
the automaton smaller in two later steps. The idea behind $\mathcal{B}_{1}$ is
that counter values in the interval $[-B,B]$ are simulated precisely (in the
factor $[-B,B]^{k}$). Roughly speaking, whenever we encounter a cycle, we can
decide whether to  (i) add its effect to this precise counter or to  (ii)
remember the effect as “must be added at least once”. We call the former
_precise cycles_ ; the latter are dubbed _obligation cycles_ and are stored in
the first factor $\mathbb{P}([-n,n]^{k})$. In either case, the effect of a
cycle is kept as “repeatable” in the second factor $\mathbb{P}([-n,n]^{k})$.

In order to be able to guess for each cycle whether it should be a precise
cycle or an obligation cycle, we traverse an insertion tree of (the prime
cycles on) a walk of $\mathcal{A}$. On the stack (the factor $\Gamma^{\leq
n}$), we keep the cycles that we have started to traverse. Suppose we are
executing a cycle in a vertex $v$ and the path from the root to $v$ consists
of the vertices $v_{1},\ldots,v_{m}$. Let $\gamma(v_{i})$ be a $q_{i}$-cycle
for $i\in[1,m]$. Then, the stack content is
$(q_{1},u_{1})\cdots(q_{m},u_{m})$, where $u_{i}$ is the effect of the part of
$\gamma(v_{i})$ that has already been traversed.

In the end, we verify that  (i) the precise counter is zero and  (ii) one can
add up obligation cycles (each of them at least once) and repeatable cycles to
zero. The latter condition is captured in the following notion. Let
$S,T\subseteq\mathbb{Z}^{k}$ be finite sets with $S=\\{u_{1},\ldots,u_{s}\\}$,
$T=\\{v_{1},\ldots,v_{t}\\}$. We call the pair $(S,T)$ _cancellable_ if there
are $x_{1},\ldots,x_{s}\in\mathbb{N}\setminus\\{0\\}$ and
$y_{1},\ldots,y_{t}\in\mathbb{N}$ with
$\sum_{i=1}^{s}x_{i}u_{i}+\sum_{i=1}^{t}y_{i}v_{i}=0$. In particular,
$(\emptyset,T)$ is cancellable for any finite $T\subseteq\mathbb{Z}^{k}$.
Together, (i) and (ii) guarantee that the accepted word is in the downward
closure: They imply that we could have executed all of the obligation cycles
and some others (again) to fulfill our obligation. Hence, there is a run of
$\mathcal{A}$ accepting a superword.

The number of cycles we can use as precise cycles is limited by the capacity
$B$ of our precise counter. We shall apply Theorem 5.2 to show that there is
always a choice of cycles to use as precise cycles so as to reach zero in the
end and not exceed the capacity.

The first type of transition in $\mathcal{B}_{1}$ is the following. For each
transition $(p,a,d,q)\in\Delta$ and state $(p,\varepsilon,v,S,T)\in Q_{1}$
such that $v+d\in[-B,B]^{k}$, we have a transition

$(p,\varepsilon,v,S,T)\xrightarrow{a}(q,\varepsilon,v+d,S,T).$ (1)

These allow us to simulate transitions in a walk of $\mathcal{A}$ that are not
part of a cycle. We can guess that a cycle is starting. If we are in state
$p$, then we push $(p,0)$ onto the stack:

$(p,w,v,S,T)\xrightarrow{\varepsilon}(p,w(p,0),v,S,T).$ (2)

While we are traversing a cycle, new counter effects are stored in the topmost
stack entry. For each transition $(p,a,d,q)\in\Delta$ and state
$(p,w(r,u),v,S,T)\in Q_{1}$ such that $u+d\in[-n,n]^{k}$, we have a transition

$(p,w(r,u),v,S,T)\xrightarrow{a}(q,w(r,u+d),v,S,T).$ (3)

When we are at the end of a cycle, we have to decide whether it should be a
precise cycle or an obligation cycle. The following transition means it should
be precise: The counter effect $u$ of the cycle is added to the counter $v$,
the stack is popped, and $u$ is added to the set of repeatable effects $T$.
For each state $(p,w(p,u),v,S,T)\in Q_{1}$ such that $v+u\in[-B,B]^{k}$, we
have a transition

$(p,w(p,u),v,S,T)\xrightarrow{\varepsilon}(p,w,v+u,S,T\cup\\{u\\}).$ (4)

In order to designate the cycle as an obligation cycle, we have the following
transition: The stack is popped and $u$ is added to both $S$ and $T$. For each
state $(p,w(p,u),v,S,T)\in Q_{1}$, we include the transition

$(p,w(p,u),v,S,T)\xrightarrow{\varepsilon}(p,w,v,S\cup\\{u\\},T\cup\\{u\\})$
(5)

The initial state is $(q_{0},\varepsilon,0,\emptyset,\emptyset)$ and the final
states are all those of the form $(q,\varepsilon,0,S,T)$ where $q$ is final in
$\mathcal{A}$ and $(S,T)$ is cancellable. Employing Lemma 4.1 and Theorem 5.2,
one can now show that $L(\mathcal{A})\subseteq L(\mathcal{B}_{1})\subseteq
L(\mathcal{A})\mathord{\downarrow}$.

### State space reduction I

We have thus shown that
$L(\mathcal{B}_{1})\mathord{\downarrow}=L(\mathcal{A})\mathord{\downarrow}$.
However, $\mathcal{B}_{1}$ has a doubly exponential number of states.
Therefore, we now reduce the number of states in two steps. First, instead of
remembering the set $S$ of obligation effects, we only maintain a linearly
independent set of vectors generating the same vector space. For a set
$R\subseteq\mathbb{Q}^{k}$, let $\operatorname{span}(R)$ denote the
$\mathbb{Q}$-vector space generated by $R$. Moreover, $\mathbb{I}(R)$ denotes
the set of linearly independent subsets of $R$. Our new automaton
$\mathcal{B}_{2}$ has states

$Q_{2}=Q\times\Gamma^{\leq
n}\times[-B,B]^{k}\times\mathbb{I}([-n,n]^{k})\times\mathbb{P}([-n,n]^{k})$

and a state in $\mathcal{B}_{2}$ is final if it is final in $\mathcal{B}_{1}$.
$\mathcal{B}_{2}$ has the same transitions as $\mathcal{B}_{1}$, except that
aside from those of type 5, it has

$(p,w(p,u),v,S,T)\xrightarrow{\varepsilon}(p,w,v,S^{\prime},T\cup\\{u\\})$ (6)

for each linearly independent subset $S^{\prime}\subseteq S\cup\\{u\\}$ such
that $\operatorname{span}(S^{\prime})=\operatorname{span}(S\cup\\{u\\})$. Of
course, such an $S^{\prime}$ exists for any $S$ and $u$. This means, by
induction on the length, for any walk of $\mathcal{B}_{1}$ from $(p,w,v,S,T)$
to $(q,w^{\prime},v^{\prime},S^{\prime},T^{\prime})$, we can find a walk with
the same input in $\mathcal{B}_{2}$ from $(p,w,v,S,T)$ to
$(q,w^{\prime},v^{\prime},S^{\prime\prime},T^{\prime})$ with
$S^{\prime\prime}\subseteq S^{\prime}$ and
$\operatorname{span}(S^{\prime\prime})=\operatorname{span}(S^{\prime})$. Since
$(S^{\prime},T^{\prime})$ is cancellable and $S^{\prime}\subseteq T^{\prime}$,
the pair $(S^{\prime\prime},T^{\prime})$ is cancellable as well. This means,
our walk in $\mathcal{B}_{2}$ is accepting and hence
$L(\mathcal{B}_{1})\subseteq L(\mathcal{B}_{2})$. It remains to verify that
$L(\mathcal{B}_{2})\subseteq L(\mathcal{B}_{1})$.

Observe that for any walk arriving in $(q,w,v,S,T)$ in $\mathcal{B}_{2}$,
there is a corresponding walk in $\mathcal{B}_{1}$ arriving in
$(q,w,v,S^{\prime},T)$ for some $S^{\prime}\supseteq S$ with
$\operatorname{span}(S^{\prime})=\operatorname{span}(S)$. The next lemma tells
us that if $(q,w,v,S,T)$ is a final state in $\mathcal{B}_{2}$, then
$(q,w,v,S^{\prime},T)$ is final in $\mathcal{B}_{1}$. This implies that
$L(\mathcal{B}_{2})\subseteq L(\mathcal{B}_{1})$ and hence
$L(\mathcal{B}_{2})=L(\mathcal{B}_{1})$.

######  Lemma 5.3.

Let $T\subseteq\mathbb{Z}^{k}$ and $S_{1}\subseteq
S_{2}\subseteq\mathbb{Z}^{k}$ such that
$\operatorname{span}(S_{1})=\operatorname{span}(S_{2})$. If $(S_{1},T)$ is
cancellable, then so is $(S_{2},T)$.

### State space reduction II

We apply a similar transformation to the last factor of the state space. In
$\mathcal{B}_{3}$, we have the state space

$Q_{3}=Q\times\Gamma^{\leq
n}\times[-B,B]^{k}\times\mathbb{I}([-n,n]^{k})\times\mathbb{I}([-n,n]^{k}).$

and a state is final in $\mathcal{B}_{3}$ if and only if it is final in
$\mathcal{B}_{2}$. Analogous to $\mathcal{B}_{2}$, we change the transitions
so that instead of adding $u\in[-n,n]^{k}$ to $T$, we store an arbitrary
$T^{\prime}\in\mathbb{I}(T\cup\\{u\\})$.

This time, it is clear that $L(\mathcal{B}_{3})\subseteq L(\mathcal{B}_{2})$:
For every walk in $\mathcal{B}_{3}$ arriving at $(q,w,v,S,T)$, there is a
corresponding walk in $\mathcal{B}_{2}$ arriving at $(q,w,v,S,T^{\prime})$
such that $T\subseteq T^{\prime}$. Clearly, if $(S,T)$ is cancellable, then
$(S,T^{\prime})$ must be cancellable as well. The following Lemma implies
$L(\mathcal{B}_{2})\subseteq L(\mathcal{B}_{3})$: It says that for each walk
in $\mathcal{B}_{2}$ arriving at $(q,w,v,S,T)$, there is a corresponding walk
in $\mathcal{B}_{3}$ arriving at $(q,w,v,S,T^{\prime})$ for some linearly
independent $T^{\prime}\subseteq T$ such that $(S,T^{\prime})$ is cancellable
and hence $(q,w,v,S,T^{\prime})$ is final.

######  Lemma 5.4.

Let $S,T\subseteq\mathbb{Z}^{k}$ such that $(S,T)$ is cancellable. Then there
is a linearly independent subset $T^{\prime}\subseteq T$ such that
$(S,T^{\prime})$ is cancellable.

We have thus shown that
$L(\mathcal{B}_{3})\mathord{\downarrow}=L(\mathcal{A})\mathord{\downarrow}$.
An estimation of the size of $Q_{3}$ now completes the proof of Theorem 5.1.
We apply Theorem 5.1 to derive an algorithm for
$\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{RBC}$.

######  Corollary 5.5.

The problem $\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{RBC}$ is in
$\mathsf{NP}$.

Since Theorem 5.1 provides an exponential bound on
$|L(\mathcal{A})|_{\mathsf{I}}$, we can use an ideal witness
$w=w_{Y_{0}}^{m}x_{1}w_{Y_{1}}^{m}\cdots x_{\ell}w_{Y_{\ell}}^{m}$
(Proposition 3.2) for which we have to check membership in $L(\mathcal{A})$.
Since $\ell$ is polynomial and $m$ exponential, we can compute a compressed
representation of $w$ in form of a _straight-line program_ , a context-free
grammar that generates one word [27]. It follows easily from work of [16] [16]
that membership of such compressed words in languages of blind (or reversal-
bounded) counter automata is decidable in $\mathsf{NP}$.

### Fixed number of counters

Unfortunately, the size bound for the NFAs provided by Theorem 5.1 has the
number of states in the exponent, meaning that if we fix the number $k$ of
counters, we still have an exponential bound. In fact, we leave open whether
one can construct polynomial-sized NFAs for fixed $k$. However, in many cases
it suffices to have a polynomial bound on the length of ideals.

######  Theorem 5.6.

If $\mathcal{A}$ is an $n$-state blind $k$-counter automaton, then
$|L(\mathcal{A})|_{\mathsf{I}}\leq(5n)^{7(k+1)^{2}}$.

Recall that an upper bound on $|L|_{\mathsf{I}}$ is essentially a pumping
lemma (see Section 3). Here, the idea is to take a walk of $\mathcal{A}$ and
delete cycles until the remaining walk $u$ is at most $n$ steps. For the
deleted cycles, we take an insertion tree of height at most $n$ (Lemma 4.1).
Then, using Theorem 5.2, we pick a subset $F$ (whose size is polynomial when
fixing $k$) of cycles that can balance out the effect of $u$. We then employ
Lemma 4.2 to the insertion trees to construct an ideal whose length is
polynomial in $|F|$.

##  6 Context-Free Grammars

We turn to context-free grammars. First, we mention that given a context-free
grammar $\mathcal{G}$, one can construct in exponential time an (exponential-
sized) NFA accepting $L(\mathcal{A})\mathord{\downarrow}$ [26, 7, 29, 10, 4].
Second, we provide an algorithm for the problem
$\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{CFG}$.

######  Theorem 6.1.

The problem $\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{CFG}$ is in
$\mathsf{P}$.

In [34], this problem has been reduced to the _simultaneous unboundedness
problem (SUP)_ for context-free languages. The latter asks, given a language
$L\subseteq a_{1}^{*}\cdots a_{n}^{*}$, whether we have
$L\mathord{\downarrow}=a_{1}^{*}\cdots a_{n}^{*}$. Moreover, this reduction is
clearly polynomial. Hence, we assume that $L(\mathcal{G})\subseteq
a_{1}^{*}\cdots a_{n}^{*}$ and that the grammar $\mathcal{G}=(N,T,P,S)$ is
productive and in Chomsky normal form, meaning that productions are of the
form $A\to BC$, $A\to a_{i}$, or $A\to\varepsilon$ for $A,B,C\in N$. First, we
add productions $A\to\varepsilon$ for all $A\in N$, so that the resulting
grammar $\mathcal{G}^{\prime}$ satisfies
$L(\mathcal{G}^{\prime})=L(\mathcal{G})\mathord{\downarrow}$. For each $A\in
N$, we can in polynomial time construct a CFG for $\\{w\in(N\cup T)^{*}\mid
A\Rightarrow^{*}_{\mathcal{G}^{\prime}}w\\}$, so we can compute the sets
$L_{i}=\\{A\in N\mid A\Rightarrow^{*}_{\mathcal{G}^{\prime}}a_{i}A\\}$ and
$R_{i}=\\{A\in N\mid A\Rightarrow^{*}_{\mathcal{G}^{\prime}}Aa_{i}\\}$ using
membership queries. We can thus compute the grammar $\mathcal{G}^{\omega}$,
which results from $\mathcal{G}^{\prime}$ by  (i) removing all productions
$A\to a_{i}$,  (ii) adding $A\to a_{i}^{\omega}A$ for each $A\in L_{i}$ and
(iii) adding $A\to Aa_{i}^{\omega}$ for each $A\in R_{i}$. Clearly, an
occurrence of $a_{i}^{\omega}$ certifies the ability to generate an unbounded
number of $a_{i}$’s. Thus, if $a_{1}^{\omega}\cdots a_{n}^{\omega}\in
L(\mathcal{G}^{\omega})$, then $a_{1}^{*}\cdots a_{n}^{*}\subseteq
L(\mathcal{G}^{\prime})=L(\mathcal{G})\mathord{\downarrow}$. It is not hard to
see that the converse is true as well. We have thus reduced the SUP to the
membership problem.

##  7 Algorithms

### Algorithms for
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathsf{Ideal}$.

Suppose $\mathcal{M}=\mathsf{Ideal}$ and we want to decide whether $I\subseteq
J$ for ideals $I,J\subseteq X^{*}$. In logspace, we construct an ideal witness
$w$ for $I$ and $J$ (Proposition 3.2) and a DFA $\mathcal{A}$ for
$X^{*}\setminus J$ (Lemma 3.4) and check whether $w\in L(\mathcal{A})$. In all
other cases, to decide $L\mathord{\downarrow}\subseteq I$, we construct a DFA
$\mathcal{A}$ for $X^{*}\setminus I$ and check whether
$L\mathord{\downarrow}\cap L(\mathcal{A})=\emptyset$.

### Algorithms for $\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathsf{NFA}$.

Suppose $\mathcal{M}=\mathsf{Ideal}$ and we want to decide whether $I\subseteq
L(\mathcal{A})\mathord{\downarrow}$ for an NFA $\mathcal{A}$. Since
$|L(\mathcal{A})|_{\mathsf{I}}\leq|\mathcal{A}|$, we can construct in logspace
an ideal witness $w$ for $I$ and $L(\mathcal{A})\mathord{\downarrow}$ and
verify $w\in L(\mathcal{A})\mathord{\downarrow}$. In all other cases, we use a
short witness for $\mathsf{coNP}$-membership.

### Algorithms for $\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathsf{OCA}$.

Suppose $\mathcal{M}=\mathsf{Ideal}$ and we want to decide whether $I\subseteq
L(\mathcal{A})\mathord{\downarrow}$ for an OCA $\mathcal{A}$. We have a
polynomial bound on $|L(\mathcal{A})|_{\mathsf{I}}$ (see Section 2). Hence, we
construct in logspace an ideal witness $w$ for $I$ and
$L(\mathcal{A})\mathord{\downarrow}$. We can also construct in logspace an OCA
$\mathcal{A}^{\prime}$ with
$L(\mathcal{A}^{\prime})=L(\mathcal{A})\mathord{\downarrow}$. Membership for
OCA is in $\mathsf{NL}=\mathsf{coNL}$, so we can verify $w\in I$ and $w\notin
L(\mathcal{A}^{\prime})=L(\mathcal{A})\mathord{\downarrow}$. In all other
cases, we convert the OCA to an NFA (see Section 2).

### Algorithms for
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathsf{RBC}_{k,r}$.

Let $\mathcal{A}$ be drawn from $\mathsf{RBC}_{k,r}$. First, suppose
$\mathcal{M}=\mathsf{Ideal}$ and we want to decide whether $I\subseteq
L(\mathcal{A})$. By Theorem 5.6, we have a polynomial bound on
$|L(\mathcal{A})|_{\mathsf{I}}$ and can construct in logspace an ideal witness
$w$ for $I$ and $L(\mathcal{A})$. We can also construct in logspace an RBCA
$\mathcal{A}^{\prime}$ with
$L(\mathcal{A}^{\prime})=L(\mathcal{A})\mathord{\downarrow}$. Since membership
for $\mathsf{RBC}_{k,r}$ is in $\mathsf{NL}$ [12], we can check whether $w\in
L(\mathcal{A}^{\prime})$. Now let
$\mathcal{M}\in\\{\mathsf{NFA},\mathsf{OCA},\mathsf{RBC}_{k,r}\\}$ and we are
given $L$ in $\mathcal{M}$ and an automaton $\mathcal{A}$ from
$\mathsf{RBC}_{k,r}$. For $\mathsf{NFA}$, $\mathsf{OCA}$, and
$\mathsf{RBC}_{k,r}$, we have a polynomial bound on $|L|_{\mathsf{I}}$ (see
Sections 2 and 5.6). Thus, we guess an ideal $I$ of polynomial length and then
verify that $I\subseteq L\mathord{\downarrow}$ but $I\not\subseteq
L(\mathcal{A})\mathord{\downarrow}$. Since
$\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathcal{M}$ and
$\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{RBC}_{k,r}$ are in
$\mathsf{NL}$, the verification is done in $\mathsf{NL}$. Hence, non-inclusion
is in $\mathsf{NP}$. For $\mathcal{M}\in\\{\mathsf{CFG},\mathsf{RBC}\\}$, we
assume a fixed alphabet. Let $L$ be in $\mathcal{M}$. Then Propositions 3.3
and 5.6 provide us with a witness of polynomial length. Since (non-)membership
in $L\mathord{\downarrow}$ and in $L(\mathcal{A})\mathord{\downarrow}$ can be
decided in $\mathsf{NP}$, non-inclusion is in $\mathsf{NP}$.

### Algorithms for $\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathsf{CFG}$.

The case $\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{CFG}$ is shown
in Theorem 6.1. Suppose
$\mathcal{M}\in\\{\mathsf{NFA},\mathsf{OCA},\mathsf{RBC}_{k,r}\\}$ and we are
given $L$ in $\mathcal{M}$ and a CFG $\mathcal{G}$. We have a polynomial bound
on $|L|_{\mathsf{I}}$ (see Sections 2 and 5.6), so that we can guess a
polynomial-length ideal $I$. Since
$\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathcal{M}$ is in
$\mathsf{NL}$ in every case and
$\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{CFG}$ is in
$\mathsf{P}$, we can verify in polynomial time that $I\subseteq
L\mathord{\downarrow}$ and $I\not\subseteq
L(\mathcal{G})\mathord{\downarrow}$. Thus, non-inclusion is in $\mathsf{NP}$.
In the case $\mathcal{M}\in\\{\mathsf{RBC},\mathsf{CFG}\\}$, we construct
exponential-sized downward closure NFAs and check inclusion for them (and the
latter problem is in $\mathsf{coNP}$). This yields a $\mathsf{coNEXP}$
algorithm.

### Algorithms for $\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathsf{RBC}$.

Let $\mathcal{A}$ be from $\mathsf{RBC}$. The ideal case is treated in
Torollary 5.5. When given $L$ in
$\mathcal{M}\in\\{\mathsf{NFA},\mathsf{OCA},\mathsf{RBC}_{k,r}\\}$, we guess a
polynomial length ideal $I$ and verify that $I\subseteq L\mathord{\downarrow}$
in $\mathsf{NL}$. Since
$\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathsf{RBC}$ is in
$\mathsf{NP}$, we can also check in $\mathsf{coNP}$ that $I\not\subseteq
L(\mathcal{A})\mathord{\downarrow}$. Hence, non-inclusion is in
$\Sigma_{2}^{\mathsf{P}}$. For
$\mathcal{M}\in\\{\mathsf{CFG},\mathsf{RBC}\\}$, we proceed as for
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathsf{CFG}$.

##  8 Hardness

In this Section, we prove hardness results. Most of them are deduced from a
generic hardness theorem that, under mild assumptions, derives hardness from
the ability to generate finite sets with long words. We will work with bounds
that exhibit the following useful property. A monotone function
$f\colon\mathbb{N}\to\mathbb{N}$ will be called _amplifying_ if $f(n)\geq n$
for $n\geq 0$ and there is a polynomial $p$ such that $f(p(n))\geq f(n)^{2}$
for large enough $n\in\mathbb{N}$. We say that a model _has property
$\Delta(f)$_ (or short: _is $\Delta(f)$_) if for each given $n\in\mathbb{N}$,
one can construct in polynomial time a description of a finite language whose
longest word has length $f(n)$. For the sake of simplicity, we will abuse
notation slightly and write $\Delta(f(n))$ instead of $\Delta(f)$. For a
function $t\colon\mathbb{N}\to\mathbb{N}$, we use $\mathsf{coNTIME}(t)$ to
denote the complements of languages accepted by nondeterministic Turing
machines that are time bounded by $O(t(n^{c}))$ for some constant $c$.

We also need two mild language theoretic properties. A _transducer_ is a
finite automaton where every edge reads input and produces output. For a
transducer $\mathcal{T}$ and a language $L$, the language $\mathcal{T}L$
consists of all words output by the transducer while reading a word from $L$.
We call a model $\mathcal{M}$ a _full trio model_ if given a transducer
$\mathcal{T}$ and a language $L$ described with $\mathcal{M}$, one can compute
in polynomial time a description of $\mathcal{T}L$. A _substitution_ is a map
$\sigma\colon X\to\mathbb{P}(Y^{*})$ that replaces each letter by a language.
For languages $L$, we define $\sigma(L)$ in the obvious way. We call $\sigma$
_simple_ if $X\subseteq Y$ and there is some $x\in X$ such that for all
$x^{\prime}\in X\setminus\\{x\\}$, we have
$\sigma(x^{\prime})=\\{x^{\prime}\\}$ and $x$ occurs in each word from $L$ at
most once. We say that $\mathcal{M}$ has _closure under simple substitutions_
if given a description of $L$ and of $\sigma(x)$ in $\mathcal{M}$, we can
compute in polynomial time a description of $\sigma(L)$.

######  Theorem 8.1.

Let $t\colon\mathbb{N}\to\mathbb{N}$ be amplifying and let $\mathcal{M}$ and
$\mathcal{N}$ be full trio models that are $\Delta(t)$ and have closure under
simple substitutions. Then both
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathcal{N}$ and
$\mathcal{M}=_{\mathord{\downarrow}}\mathcal{N}$ are hard for
$\mathsf{coNTIME}(t)$. Moreover, this hardness already holds for binary
alphabets.

Since NFAs are $\Delta(n)$, Theorem 8.1 yields $\mathsf{coNP}$-hardness for
inclusion and equivalence. In [4], hardness of equivalence was shown directly.
RBCA and CFG clearly exhibit closure under simple substitutions and can
generate exponentially long words. This yields:

######  Corollary 8.2.

For $\mathcal{M},\mathcal{N}\in\\{\mathsf{CFG},\mathsf{RBC}\\}$,
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathcal{N}$ and
$\mathcal{M}=_{\mathord{\downarrow}}\mathcal{N}$ are $\mathsf{coNEXP}$-hard.

From Theorem 8.1, we can also deduce hardness for other models. It was shown
by [14] [14] that downward closures or Petri net languages are computable,
which implies decidability of our problems. We use Theorem 8.1 to prove an
Ackermann lower bound. Let $A_{n}\colon\mathbb{N}\to\mathbb{N}$ be defined as
$A_{0}(x)=x+1$, $A_{n+1}(0)=A_{n}(1)$, and $A_{n+1}(x+1)=A_{n}(A_{n+1}(x))$.
Then, the function $A\colon\mathbb{N}\to\mathbb{N}$ with $A(n)=A_{n}(n)$ is
the _Ackermann function_. Of course, for large enough $n$, we have
$A_{n}(x)\geq x^{2}$. For such $n$, we have $A(n+1)=A_{n}(A_{n+1}(n))\geq
A_{n+1}(n)^{2}\geq A(n)^{2}$, so $A$ is amplifying. A result of [28] [28] (see
also [32]) states that given $n\in\mathbb{N}$, one can construct in polynomial
time a Petri net that, from its initial marking, can produce up to $A(n)$
tokens in an output place. Hence, Petri nets are $\Delta(A)$ and they clearly
satisfy the language-theoretic conditions.

######  Corollary 8.3.

For Petri net languages, inclusion and equivalence of downward closures is
Ackermann-hard.

Building on the sufficient condition of [34], [15] [15] have shown that
downward closures are computable for higher-order pushdown automata. However,
the method of [34] does not yield any information about the complexity of this
computation. For $k\in\mathbb{N}$, we denote by $\exp_{k}$ the function with
$\exp_{0}(n)=n$ and $\exp_{k+1}(n)=2^{\exp_{k}(n)}$. It is easy to see that
order-$k$ pushdown automata are $\Delta(\exp_{k})$ (for instance, one can
adapt Example 2.5 of [8]). By $\mathsf{co}\mathchar 45\relax{}k\mathchar
45\relax\mathsf{NEXP}$, we denote the complements of languages accepted by
nondeterministic Turing machines in time $O(\exp_{k}(n^{c}))$ for some
constant $c$.

######  Corollary 8.4.

For higher-order pushdown automata of order $k$, inclusion and equivalence of
downward closures is hard for $\mathsf{co}\mathchar 45\relax{}k\mathchar
45\relax\mathsf{NEXP}$.

Our last hardness result could also be shown using the method of Theorem 8.1.
However, it is simpler to reduce a variant of the subset sum problem [6].

######  Proposition 8.5.

$\mathsf{NFA}\subseteq_{\mathord{\downarrow}}\mathsf{RBC}$ and
$\mathsf{NFA}=_{\mathord{\downarrow}}\mathsf{RBC}$ are
$\Pi_{2}^{\mathsf{P}}$-hard, even for binary alphabets.

We have thus shown hardness for all inclusion problems that do not involve
ideals. The remaining cases inherit hardness from the emptiness problem (for
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathsf{Ideal}$) or the non-
emptiness problem
($\mathsf{Ideal}\subseteq_{\mathord{\downarrow}}\mathcal{M}$).

## References

  * [1] Parosh Aziz Abdulla, Luc Boasson and Ahmed Bouajjani  “Effective Lossy Queue Languages”  In _ICALP 2001_
  * [2] Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani and Bengt Jonsson  “Using Forward Reachability Analysis for Verification of Lossy Channel Systems”  In _Formal Methods in System Design_ 25.1 Kluwer Academic Publishers, 2004, pp. 39–65
  * [3] Mohamed Faouzi Atig et al.  “The complexity of regular abstractions of one-counter languages” To appear in LICS 2016, 2016  arXiv:1602.03419
  * [4] Georg Bachmeier, Michael Luttenberger and Maximilian Schlund  “Finite Automata for the Sub- and Superword Closure of CFLs: Descriptional and Computational Complexity”  In _LATA 2015_
  * [5] Brenda S. Baker and Ronald V. Book  “Reversal-bounded multipushdown machines”  In _Journal of Computer and System Sciences_ 8.3, 1974, pp. 315–332
  * [6] Piotr Berman et al.  “On the complexity of pattern matching for highly compressed two-dimensional texts”  In _CPM 1997_
  * [7] Bruno Courcelle  “On constructing obstruction sets of words”  In _Bulletin of the EATCS_ 44, 1991, pp. 178–186
  * [8] Werner Damm and Andreas Goerdt  “An automata-theoretic characterization of the OI-hierarchy”  In _ICALP 1982_
  * [9] S. A. Greibach  “Remarks on blind and partially blind one-way multicounter machines”  In _Theoretical Computer Science_ 7.3, 1978, pp. 311 –324
  * [10] Hermann Gruber, Markus Holzer and Martin Kutrib  “More on the size of Higman-Haines sets: effective constructions”  In _Fundamenta Informaticae_ 91.1 IOS Press, 2009, pp. 105–121
  * [11] Hermann Gruber, Markus Holzer and Martin Kutrib  “The size of Higman-Haines sets”  In _Theoretical Computer Science_ 387.2, 2007, pp. 167–176
  * [12] Eitan M. Gurari and Oscar H. Ibarra  “The complexity of decision problems for finite-turn multicounter machines”  In _Journal of Computer and System Sciences_ 22.2, 1981, pp. 220 –229
  * [13] Christoph Haase and Piotr Hofman  “Tightening the Complexity of Equivalence Problems for Commutative Grammars”  In _STACS 2016_
  * [14] Peter Habermehl, Roland Meyer and Harro Wimmel  “The Downward-Closure of Petri Net Languages”  In _ICALP 2010_
  * [15] Matthew Hague, Jonathan Kochems and C.-H. Luke Ong  “Unboundedness and Downward Closures of Higher-order Pushdown Automata”  In _POPL 2016_
  * [16] Matthew Hague and Anthony Widjaja Lin  “Model Checking Recursive Programs with Numeric Data Types”  In _CAV 2011_
  * [17] Leonard H. Haines  “On free monoids partially ordered by embedding”  In _Journal of Combinatorial Theory_ 6.1 Elsevier, 1969, pp. 94–98
  * [18] Dung T. Huynh  “The complexity of equivalence problems for commutative grammars”  In _Information and Control_ 66.1, 1985, pp. 103–121
  * [19] Oscar H. Ibarra  “Reversal-bounded multicounter machines and their decision problems”  In _Journal of the ACM (JACM)_ 25.1 ACM, 1978, pp. 116–133
  * [20] Matthias Jantzen and Alexy Kurganskyy  “Refining the hierarchy of blind multicounter languages and twist-closed trios”  In _Information and Computation_ 185.2, 2003, pp. 159–181
  * [21] P. Jullien  “Contribution à létude des types d’ordres dispersés”, 1969
  * [22] P. Karandikar, M. Niewerth and Ph. Schnoebelen  “On the state complexity of closures and interiors of regular languages with subwords and superwords”  In _Theoretical Computer Science_ 610, Part A, 2016, pp. 91–107
  * [23] Eryk Kopczyński  “Complexity of Problems of Commutative Grammars”  In _Logical Methods in Computer Science_ 11.1, 2015
  * [24] Eryk Kopczyński and Anthony Widjaja To  “Parikh Images of Grammars: Complexity and Applications”  In _LICS 2010_
  * [25] Salvatore La Torre, Anca Muscholl and Igor Walukiewicz  “Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable”  In _CONCUR 2015_
  * [26] Jan Leeuwen  “Effective constructions in well-partially-ordered free monoids”  In _Discrete Mathematics_ 21.3, 1978, pp. 237–252
  * [27] Markus Lohrey  “Algorithmics on SLP-compressed strings: a survey”  In _Groups Complexity Cryptology_ 4.2, 2012, pp. 241–299
  * [28] Ernst W Mayr and Albert R Meyer  “The complexity of the finite containment problem for Petri nets”  In _Journal of the ACM_ 28.3 ACM, 1981, pp. 561–576
  * [29] Alexander Okhotin  “On the state complexity of scattered substrings and superstrings”  In _Fundamenta Informaticae_ 99.3 IOS Press, 2010, pp. 325–338
  * [30] Rohit J. Parikh  “On Context-Free Languages”  In _Journal of the ACM_ 13.4 New York, NY, USA: ACM, 1966, pp. 570–581
  * [31] Loïc Pottier  “Minimal solutions of linear diophantine systems : bounds and algorithms”  In _RTA 1991_
  * [32] Lutz Priese and Harro Wimmel  “Petri-Netze”  Springer-Verlag, 2003
  * [33] Narad Rampersad, Jeffrey Shallit and Zhi Xu  “The computational complexity of universality problems for prefixes, suffixes, factors, and subwords of regular languages”  In _Fundamenta Informaticae_ 116.1-4 IOS press, 2012, pp. 223–236
  * [34] Georg Zetzsche  “An Approach to Computing Downward Closures”  In _ICALP 2015_
  * [35] Georg Zetzsche  “Computing Downward Closures for Stacked Counter Automata”  In _STACS 2015_

##  Appendix A Ideals and Witnesses

###### Proof of Proposition 3.1.

Let $\mathcal{A}=(Q,X,\Delta,q_{0},Q_{f})$. Consider the DFA
$\mathcal{B}=(\mathbb{P}(Q),X,\Delta^{\prime},Q,Q^{\prime}_{f})$, where from a
state $P\subseteq Q$ on input $x\in X$, we enter the state $P^{\prime}$,
consisting of all $q^{\prime}\in Q$ that are reachable from a state in $P$ via
a path on which $x$ occurs. Moreover, $Q^{\prime}_{f}$ is the set of all
$P\subseteq Q$ with $P\cap Q_{f}=\emptyset$. Then clearly $\mathcal{B}$
accepts $X^{*}\setminus L(\mathcal{A})\mathord{\downarrow}$.

Choose $w\in K\mathord{\downarrow}\setminus
L(\mathcal{A})\mathord{\downarrow}$ of minimal length and write $w=w_{1}\cdots
w_{m}$ for letters $w_{1},\ldots,w_{m}$. Suppose $m>|\mathcal{A}|+1$ and
consider the run of $w$ in $\mathcal{B}$. For each $i\in[0,m]$, let
$P_{i}\subseteq Q$ be the state entered after reading $w_{1}\cdots w_{i}$.
Then we have $P_{0}\supseteq P_{1}\supseteq\cdots$ and since $m>|Q|+1$, there
are $i<j$ with $P_{i}=P_{j}$. Yet this means that also $w^{\prime}=w_{1}\cdots
w_{i}w_{j+1}\cdots w_{m}$ is a member of $L(\mathcal{B})=X^{*}\setminus
L(\mathcal{A})\mathord{\downarrow}$. Moreover, we have $w^{\prime}\preceq w$
and thus $w^{\prime}\in K\mathord{\downarrow}$. This contradicts our choice of
$w$. ∎

###### Proof of Proposition 3.2.

The implications “(i)$\Rightarrow$(ii)” and “(ii)$\Rightarrow$(iii)” are
trivial, so assume (iii). Write
$L\mathord{\downarrow}=\bigcup_{i=1}^{\ell}I_{i}$ as a union of ideals of
length $\leq|L|_{\mathsf{I}}$. Then we have
$w_{Y_{0}}^{m}x_{1}w_{Y_{1}}^{m}\cdots x_{n}w_{Y_{n}}^{m}\in I_{i}$ for some
$i$. Since $I_{i}$ has length at most $|L|_{\mathsf{I}}$, there is an NFA
$\mathcal{A}$ with at most $|L|_{\mathsf{I}}+1$ states for $I_{i}$. However,
we have $m\geq|L|_{\mathsf{I}}+1$, so in the computation of the NFA for
$w_{Y_{0}}^{m}x_{1}w_{Y_{1}}^{m}\cdots x_{n}w_{Y_{n}}^{m}$, for each
$i\in[0,n]$, some power $w_{Y_{i}}^{k_{i}}$, $k_{i}>0$, has to lie on a cycle
of $\mathcal{A}$. We can therefore pump each of these cycles, which implies
$I\subseteq I_{i}\subseteq L\mathord{\downarrow}$. ∎

###### Proof of Lemma 3.4.

Let
$I=Y_{0}^{*}\\{x_{1},\varepsilon\\}Y_{1}^{*}\cdots\\{x_{n},\varepsilon\\}Y_{n}^{*}$
with. For $i\in[0,n]$ and $a\in X$, let

$J_{i,a}=\\{j\in[i,n]\mid a\in
Y_{i}^{*}\\{x_{i+1},\varepsilon\\}Y_{i+1}^{*}\cdots\\{x_{j},\varepsilon\\}Y_{j}^{*}\\}$

Our DFA has states $Q=\\{0,\ldots,n+1\\}$ and for $i\in Q$, we have
$i\xrightarrow{a}j$ if and only if

$j=\begin{cases}\min J_{i,a}&\text{if $J_{i,a}\neq\emptyset$}\\\ n+1&\text{if
$J_{i,a}=\emptyset$}\end{cases}$

Moreover, $0$ is the initial state and the states $0,\ldots,n$ are final.
Clearly, the automaton is ordered, has $n+2$ states, and can be constructed in
logarithmic space. In order to show the correctness, we define the ideal
$I_{k}=Y_{0}^{*}\\{x_{1},\varepsilon\\}Y_{1}^{*}\cdots\\{x_{k},\varepsilon\\}Y_{k}^{*}$
for each $k\in[0,n]$. Observe that $I_{0}\subseteq
I_{1}\subseteq\cdots\subseteq I_{n}=I$. By induction on the length of $w$, it
is easy to see that if $0\xrightarrow{w}j$, then

  * •

if $j\in[0,n]$, then $j$ is the smallest number with $w\in I_{j}$.

  * •

if $j=n+1$, then $w\notin I$.

In particular, the automaton accepts $I$. ∎

###### Proof of Lemma 3.5.

To make our induction work, we define $f_{n}\colon\mathbb{N}\to\mathbb{N}$ by
$f_{n}(1)=n-1$ and $f_{n}(k)=(f_{n}(k-1)+1)\cdot(n-1)$. We claim that if
$w>f_{n}(|X|)$ for $w\in X^{*}$, then $w$ has a position at which every
ordered $n$-state DFA cycles.

We proceed by induction on $|X|$. If $X=\\{a\\}$, then it suffices to consider
$w=a^{n}$. Consider an ordered $n$-state DFA $\mathcal{A}$ and let
$q_{0},q_{1},\ldots,q_{n}$ be the states occupied while reading $w$. Then
there are $i<j$ with $q_{i}=q_{j}$ and since $\mathcal{A}$ is ordered, we have
$q_{i}=q_{i+1}$. This means, $q_{i}$ has an $a$-labeled loop and therefore
$q_{i}=q_{i+1}=q_{i+2}=\cdots=q_{n}$. In particular, $\mathcal{A}$ cycles at
the last position of $w$.

Now suppose $k=|X|>1$ and $|w|>f_{n}(k)=(f_{n}(k-1)+1)(n-1)$. For every word
$v\in X^{*}$, let $\alpha(v)\in X^{*}$ be the shortest prefix of $v$ in which
every letter from $X$ occurs. If $v$ does not contain every letter from $X$,
then we define $\alpha(v)=v$. We factorize $w$ as $p_{1}\cdots p_{m}$ by
applying $\alpha$ to $w$, then applying $\alpha$ to the rest of the word, and
so on. Formally, we set $r_{0}=w$, $p_{i}=\alpha(r_{i-1})$, and define $r_{i}$
so that $r_{i-1}=p_{i}r_{i}$. For some smallest $m\geq 1$, we have
$p_{m}=r_{m}$. Then clearly $w=p_{1}\cdots p_{m}$ and every $p_{i}$ is non-
empty.

For each $i\in[1,m]$, let $p^{\prime}_{i}$ be obtained from $p_{i}$ by
removing its last position. By the choice of $p_{i}$, the word
$p^{\prime}_{i}$ contains at most $k-1$ distinct letters. Hence, if
$|p^{\prime}_{i}|>f_{n}(k-1)$ for some $i\in[1,m]$, then $p^{\prime}_{i}$
contains a position at which every ordered $n$-state DFA cycles. In
particular, $w$ contains such a position (because every computation on $w$
contains some computation on $p^{\prime}_{i}$). Therefore, we may assume that
$|p_{i}|=|p^{\prime}_{i}|+1\leq f_{n}(k-1)+1$ for every $i\in[1,m]$.

If we had $m\leq n-1$, this would imply $|w|=|p_{1}\cdots
p_{m}|\leq(f_{n}(k-1)+1)(n-1)$, which is not the case. Hence, we have $m\geq
n$. Now consider an ordered $n$-state DFA $\mathcal{A}$ with its computation

$q_{0}\xrightarrow{p_{1}}q_{1}\xrightarrow{p_{2}}\cdots\xrightarrow{p_{m}}q_{m}.$

Since $m+1>n$, there are $i<j$ with $q_{i}=q_{j}$ and since $\mathcal{A}$ is
ordered, we have $q_{i}=q_{i+1}=\cdots=q_{j}$. We distinguish two cases.

  * •

If $j=m$, then our computation cycles at every position in $p_{m}$.

  * •

If $j<m$, then $p_{j}$ contains every letter from $X$ at least once. This
means $q_{i}$ has an $a$-loop for every $a\in X$. Therefore,
$q_{i}=q_{i+1}=\cdots=q_{m}$. In particular, our computation cycles on every
position in $p_{m}$.

Thus, we have shown that any ordered $n$-state DFA cycles on every position in
$p_{m}$, which proves our claim.

From the definition of $f_{n}$, it follows easily by induction that
$f_{n}(k)=\sum_{i=1}^{k}(n-1)^{i}$ and hence $f_{n}(k)\leq k\cdot(n-1)^{k}$. ∎

##  Appendix B Insertion trees

###### Proof of Lemma 4.1.

Let $w\in\Delta^{*}$ be a prime $q$-cycle and let $P_{w}\subseteq Q$ be the
set of states occurring properly in $w$. We show by induction on $|P_{w}|$
that every prime cycle $w$ admits an insertion tree of height at most
$|P_{w}|$.

If no state from $P_{w}$ repeats in $w$, then $w$ is simple and the statement
is trivial. For each $p\in P_{w}$ that does repeat in $w$, let $\lambda(p)$ be
the length of the longest $p$-cycle that is a factor of $w$. Among all states
from $P_{w}$ that repeat in $w$, we choose $p$ such that $\lambda(p)$ is
maximal. Then $w=xyz$ where $y$ is a $p$-cycle of length $\lambda(p)$. Observe
that by the maximality of $p$, there is no state that occurs properly both in
$x$ and in $z$.

We write $y=y_{1}\cdots y_{r}$ such that each $y_{i}$ is a prime $p$-cycle.
Then since $p$ does not occur properly in $y_{i}$, each $y_{i}$ admits an
insertion tree $t_{i}$ of height $|P_{w}|-1$.

Consider any insertion tree $t$ of $xz$. Observe that since there is no state
that occurs properly both in $x$ and in $z$, the only cycle in $t$ where $p$
can occur is $t$’s root. Therefore, if $s_{1},\ldots,s_{k}$ are the subtrees
of $t$ immediately below the root, then no $\alpha(s_{i})$ contains $p$. We
can therefore factorize each $\alpha(s_{i})$ into prime cycles that each have
an insertion tree of height at most $|P_{w}|-1$. Thus, by replacing in $t$
each $s_{i}$ by this sequence of trees, we obtain an insertion tree
$t^{\prime}$ of $xz$ of height at most $|P_{w}|$.

Since $p$ occurs in the root of $t^{\prime}$ and this is the only occurrence
of $p$ in $t^{\prime}$, we can attach the trees $t_{i}$ directly below the
root of $t^{\prime}$ to obtain a insertion tree $t^{\prime\prime}$ of $w$.
Moreover, since each $t_{i}$ has height at most $|P_{w}|-1$,
$t^{\prime\prime}$ has height at most $|P_{w}|$. ∎

###### Proof of Lemma 4.2.

If $F=\emptyset$, then we can duplicate every tree in the sequence, leading to
$P(s,F)\mathord{\downarrow}=Y^{*}$, where $Y$ is the set of letters occurring
anywhere on a tree in $s$. Hence, $P(s,F)\mathord{\downarrow}$ is an ideal of
expression length one. Thus, we assume $F\neq\emptyset$.

As the first step, we consider the case where $s$ consists of one tree $t$.
Let $A$ be the set of vertices in $t$ that are ancestors of vertices in $F$.
We show by induction on $h$ that $P(t,F)\mathord{\downarrow}$ is an ideal and
$|P(t,F)|_{\mathsf{E}}\leq|A|\cdot(2|Q|+|F|)$.

Let $r$ be the root of $t$ and $\gamma(r)=e_{1}\cdots e_{\ell}$, where
$e_{1},\ldots,e_{\ell}\in\Delta$. Let $C$ be the set of children of $r$ that
are in $A$. Moreover, let $e_{i}=(q_{i-1},a_{i},q_{i})$ for $i\in[1,\ell-1]$.
Recall that every child of $r$ is assigned a $q_{i}$-cycle for some
$i\in[1,\ell-1]$. For each $i\in[1,\ell-1]$, consider the subtrees ‘inserted
after $e_{i}$’: In other words, those subtrees directly below $r$ whose root
node is assigned a $q_{i}$-cycle by $\gamma$. Some of them contain a fixed
vertex; let $s_{i,1},\ldots,s_{i,k_{i}}$ be those subtrees. The other subtrees
inserted after $e_{i}$ are pumpable; let $Y_{i}$ be the set of input letters
occurring in them. Let $F_{i,j}\subseteq F$ be the set of fixed nodes in
$s_{i,j}$. Moreover, let $A_{i,j}$ be the set of vertices in $s_{i,j}$ that
are ancestors of fixed vertices (in $s_{i,j}$). Note that since
$F\neq\emptyset$, we have $r\in A$ and thus

$|A|=1+\sum_{i=1}^{\ell-1}\sum_{j=1}^{k_{i}}|A_{i,j}|.$

By induction, $P(s_{i,j},F_{i,j})\mathord{\downarrow}$ is an ideal and we have

$|P(s_{i,j},F_{i,j})\mathord{\downarrow}|_{\mathsf{E}}\leq|A_{i,j}|\cdot(2|Q|+|F_{i,j}|)\leq|A_{i,j}|\cdot(2|Q|+|F|).$
(7)

  * •

Suppose $r\in F$. Then we have
$P(t,F)\mathord{\downarrow}=\\{a_{1},\varepsilon\\}I_{1}\\{a_{2},\varepsilon\\}\cdots
I_{\ell-1}\\{a_{\ell},\varepsilon\\}$, where

$I_{i}=Y_{i}^{*}(P(s_{i,1},F_{i,1})\mathord{\downarrow})Y_{i}^{*}\cdots(P(s_{i,k_{i}},F_{i,k_{i}})\mathord{\downarrow})Y_{i}^{*}$

for $i\in[1,\ell-1]$. Hence, $P(t,F)\mathord{\downarrow}$ is an ideal. Let us
estimate the expression length. Note that (7) yields

$|I_{i}|_{\mathsf{E}}\leq
k_{i}+1+\sum_{j=1}^{k_{i}}|P(s_{i,j},F_{i,j})\mathord{\downarrow}|_{\mathsf{E}}\leq
k_{i}+1+(2|Q|+|F|)\cdot\sum_{j=1}^{k_{i}}|A_{i,j}|$

and therefore

$\displaystyle|P(t,F)\mathord{\downarrow}|_{\mathsf{E}}$
$\displaystyle\leq\ell+\sum_{i=1}^{\ell-1}|I_{i}|\leq\ell+\sum_{i=1}^{\ell-1}(k_{i}+1)+(2|Q|+|F|)\sum_{i=1}^{\ell-1}\sum_{j=1}^{k_{i}}|A_{i,j}|$
$\displaystyle\leq
2\ell+\underbrace{\sum_{i=1}^{\ell-1}k_{i}}_{\leq|F|}\leavevmode\nobreak\
\leavevmode\nobreak\ +\leavevmode\nobreak\ \leavevmode\nobreak\
(2|Q|+|F|)\underbrace{\sum_{i=1}^{\ell-1}\sum_{j=1}^{k_{i}}|A_{i,j}|}_{=|A|-1}$
$\displaystyle\leq 2|Q|+|F|\leavevmode\nobreak\ \leavevmode\nobreak\
+\leavevmode\nobreak\ \leavevmode\nobreak\ (2|Q|+|F|)\cdot(|A|-1)$
$\displaystyle\leq|A|\cdot(2|Q|+|F|).$

  * •

Suppose $r\notin F$. Then we have $P(t,F)\mathord{\downarrow}=I_{1}\cdots
I_{\ell-1}$, where

$I_{i}=Z_{i}^{*}(P(s_{i,1},F_{i,1})\mathord{\downarrow})Z_{i}^{*}\cdots(P(s_{i,k_{i}},F_{i,k_{i}})\mathord{\downarrow})Z_{i}^{*},$

for $i\in[1,\ell-1]$ with $Z_{i}=Y_{i}\cup\\{a_{1},\ldots,a_{\ell}\\}$. Hence,
$P(t,F)\mathord{\downarrow}$ is an ideal. Let us estimate the expression
length. As before, (7) yields

$|I_{i}|_{\mathsf{E}}\leq
k_{i}+1+\sum_{i=1}^{k_{i}}|P(s_{i,j},F_{i,j})\mathord{\downarrow}|_{\mathsf{E}}\leq
k_{i}+1+(2|Q|+|F|)\cdot\sum_{j=1}^{k_{i}}|A_{i,j}|$

and therefore

$\displaystyle|P(t,F)\mathord{\downarrow}|_{\mathsf{E}}$
$\displaystyle\leq\sum_{i=1}^{\ell-1}(k_{i}+1)\leavevmode\nobreak\
\leavevmode\nobreak\ +\leavevmode\nobreak\ \leavevmode\nobreak\
(2|Q|+|F|)\sum_{i=1}^{\ell-1}\sum_{j=1}^{k_{i}}|A_{i,j}|$
$\displaystyle\leq\ell+\sum_{i=1}^{\ell-1}k_{i}\leavevmode\nobreak\
\leavevmode\nobreak\ +\leavevmode\nobreak\ \leavevmode\nobreak\
(2|Q|+|F|)\sum_{i=1}^{\ell-1}\sum_{j=1}^{k_{i}}|A_{i,j}|$ $\displaystyle\leq
2|Q|+|F|\leavevmode\nobreak\ \leavevmode\nobreak\ +\leavevmode\nobreak\
\leavevmode\nobreak\ (2|Q|+|F|)\cdot(|A|-1)$
$\displaystyle\leq|A|\cdot(2|Q|+|F|).$

This concludes our first step. Note that since $t$ has height $\leq h$, every
vertex in $F$ has at most $h$ ancestors, so that $|A|\leq h\cdot|F|$. This
means, our first step implies that in the case of a single tree $t$, we have
$|P(t,F)\mathord{\downarrow}|_{\mathsf{E}}\leq h|F|\cdot(2|Q|+|F|)$.

Let us now consider $P(s,F)\mathord{\downarrow}$ where $s=t_{1}\cdots t_{m}$
is a compatible sequence. Of the trees $t_{1},\ldots,t_{m}$, let
$t^{\prime}_{1},\ldots,t^{\prime}_{\ell}$ be those which contain a fixed
vertex. The other trees in the sequence $t_{1},\ldots,t_{m}$ are pumpable and
we define $Y$ to be the set of letters occurring in those pumpable trees. Note
that $\ell\leq|F|$.

According to our first step, we have
$|P(t^{\prime}_{i},F)\mathord{\downarrow}|_{\mathsf{E}}\leq
h|F|\cdot(2|Q|+|F|)$ for each $i\in[1,\ell]$. Moreover, we have

$P(s,F)\mathord{\downarrow}=Y^{*}P(t^{\prime}_{1},F)\mathord{\downarrow}Y^{*}\cdots
P(t^{\prime}_{\ell},F)\mathord{\downarrow}Y^{*},$

which means $P(s,F)\mathord{\downarrow}$ is an ideal and we may estimate

$\displaystyle|P(s,F)\mathord{\downarrow}|_{\mathsf{E}}$
$\displaystyle\leq(\ell+1)+\sum_{i=1}^{\ell}|P(t^{\prime}_{i},F)\mathord{\downarrow}|_{\mathsf{E}}\leq\ell+1+\ell\cdot
h|F|\cdot(2|Q|+|F|)$ $\displaystyle\leq h\cdot|F|\cdot(2|Q|+|F|)^{2},$

which proves the Lemma. ∎

##  Appendix C Counter automata

We prove the statements of Section 5 in the order they are made. We begin with
Theorem 5.1.

###### Proof of Theorem 5.1.

We have seen that
$L(\mathcal{B}_{3})\mathord{\downarrow}=L(\mathcal{A})\mathord{\downarrow}$.
To estimate the size of $\mathcal{B}_{3}$, notice that

$\displaystyle|[-B,B]^{k}|$
$\displaystyle=(2B+1)^{k}\leq(2(n+n\cdot(3n)^{(k+1)^{2}})+1)^{k}$
$\displaystyle=(2n\cdot(3n)^{(k+1)^{2}}+2n+1)^{k}\leq(3n)^{((k+1)^{2}+1)k}\leq(3n)^{5k^{3}}.$

Furthermore, our stack alphabet satisfies $|\Gamma|=n\cdot(2n+1)^{k}$, so that

$|\Gamma^{\leq
n}|\leq|\Gamma|^{n+1}=n^{n+1}\cdot(2n+1)^{(n+1)k}\leq(3n)^{4nk}.$

Finally, we can estimate
$|\mathbb{I}([-n,n]^{k})|\leq\binom{(2n+1)^{k}}{k}\leq(2n+1)^{k^{2}}\leq(3n)^{k^{2}}$.
This means in total $|Q_{3}|\leq
n\cdot(3n)^{4nk+5k^{3}+2k^{2}}\leq(3n)^{5nk+7k^{3}}$. This completes the proof
of Theorem 5.1. ∎

Next, we show that $L(\mathcal{B}_{1})$ and $L(\mathcal{A})$ have the same
downward closure.

######  Proposition C.1.

$L(\mathcal{A})\subseteq L(\mathcal{B}_{1})\subseteq
L(\mathcal{A})\mathord{\downarrow}$.

We prove Proposition C.1 in the following two lemmas.

######  Lemma C.2.

$L(\mathcal{A})\subseteq L(\mathcal{B}_{1})$.

###### Proof.

Let $w\in\Delta^{*}$ be an accepting walk of $\mathcal{A}$. We can write
$w=u_{0}v_{1}u_{1}\cdots v_{\ell}u_{\ell}$ such that $|u_{0}\cdots
u_{\ell}|\leq n$ and every $v_{i}$ is a prime cycle. For each $v_{i}$, Lemma
4.1 yields an insertion tree $t_{i}$ of height at most $n$. In
$\mathcal{B}_{1}$, we simulate $u_{0}\cdots u_{\ell}$ by transitions of type
1. When we arrive at a prime cycle $v_{i}$, we traverse the tree $t_{i}$: When
at the current state a subtree is attached in $t_{i}$, we use a transition of
type 2. When we arrive at the state where our current cycle has started, we
use either 4 or 5 to use the cycle as a precise cycle or as an obligation
cycle, respectively. During a cycle, we use transitions 3.

It remains to be shown that there exists a choice of cycles as ‘precise’ or
‘obligation’ to obtain an accepting run of $\mathcal{B}_{1}$, i.e. the
capacity in the factor $[-B,B]^{k}$ is not exceeded and the sets $S$ and $T$
in the factors $\mathbb{P}([-n,n]^{k})$ form a cancellable $(S,T)$. To this
end, we apply Theorem 5.2. Let $e_{1},\ldots,e_{m}\in\mathbb{Z}^{k}$ be the
different effects (in any order) of the (simple) cycles in all the insertion
trees $t_{i}$, $i\in[1,\ell]$. Being effects of simple cycles, they are even
contained in $[-n,n]^{k}$. For each $i\in[1,m]$, let $x_{i}$ be the number of
times $e_{i}$ occurs as an effect of a cycle. Let $e$ be the effect of the
walk $u_{0}\cdots u_{\ell}$. Then we have $e\in[-n,n]^{k}$. Since the walk
$w=u_{0}v_{1}u_{1}\cdots v_{\ell}u_{\ell}$ is accepting in $\mathcal{A}$, we
have $e+\sum_{i=1}^{m}x_{i}e_{i}=0$.

Consider the matrix $A\in\mathbb{Z}^{k\times m}$ with columns
$e_{1},\ldots,e_{m}$. Then the vector $x=(x_{1},\ldots,x_{m})$ satisfies
$Ax=-e$. Since the $e_{i}$ are pairwise distinct and members of $[-n,n]^{k}$,
we have $m\leq(2n+1)^{k}$. This yields $\|(A|e)\|_{1,\infty}\leq(m+1)n$.
Moreover, $A$ has rank at most $k$. By Theorem 5.2, there exists a
$y\in\mathbb{N}^{m}$ with $Ay=-e$, $y\leq x$, and

$\|y\|_{1}\leq(1+(m+1)n)^{k+1}=(mn+n+1)^{k+1}\leq((2n+1)^{k+1})^{k+1}\leq(3n)^{(k+1)^{2}}.$

We can therefore choose for each $i\in[1,m]$, $y_{i}$ of the $x_{i}$ cycles
with effect $e_{i}$ and use them as precise cycles. Then, in the end, we
arrive at a state $(q,\varepsilon,v,S,T)$ with $v=0$. Since we used at most
$\|y\|_{1}$ precise cycles and at most $n$ transitions in the walk
$u_{1}\cdots u_{\ell}$, the counter values encountered during the computation
are bounded in absolute value by $n+n\cdot(3n)^{(k+1)^{2}}=B$.

Observe that we have $T=\\{e_{1},\ldots,e_{m}\\}$. Consider
$z\in\mathbb{N}^{m}$ with $z=x-y$. By our choice of precise cycles,
$S=\\{e_{i}\mid z_{i}>0\\}$. Therefore, since $Az=0$, the pair $(S,T)$ is
cancellable. Hence, we have reached a final state of $\mathcal{B}_{1}$ and
read the same word as $w$. ∎

######  Lemma C.3.

$L(\mathcal{B}_{1})\subseteq L(\mathcal{A})\mathord{\downarrow}$.

###### Proof.

Consider a walk $w$ in $\mathcal{B}_{1}$ from $(p,\varepsilon,0,S,T)$ to
$(q,\varepsilon,v,S^{\prime},T^{\prime})$. Let $S^{\prime}\setminus
S=\\{e_{1},\ldots,e_{m}\\}$ and $(S^{\prime}\setminus
S)\cup(T^{\prime}\setminus T)=\\{e_{1},\ldots,e_{m+\ell}\\}$. Let
$A\in\mathbb{Z}^{(m+\ell)\times k}$ be the matrix with columns
$e_{1},\ldots,e_{m+\ell}$. Moreover, for each $i\in[1,m]$, let
$x_{i}\in\mathbb{N}\setminus\\{0\\}$ be the number of times a cycle with
effect $e_{i}$ was used as an obligation cycle. Let $x\in\mathbb{N}^{m+\ell}$
be the vector $x=(x_{1},\ldots,x_{m+\ell})$ where $x_{m+i}=0$ for
$i\in[1,\ell]$.

It is easy to show by induction on the maximal stack height in $w$ that for
every $y\in\mathbb{N}^{m+\ell}$ with $y\geq x$, there exists a walk
$w^{\prime}$ in $\mathcal{A}$ from $(p,0)$ to $(q,v+Ay)$ such that
$w^{\prime}$ reads a superword of the input of $w$: We execute all the
obligation cycles as normal cycles in $\mathcal{A}$, which means adding the
effect $Ax$. Then, for each effect $e_{i}$, we execute some cycle with effect
$e_{i}$ an additional $y_{i}-x_{i}$ times. In total, we add $v+Ay$ to the
counter in $\mathcal{A}$.

Now suppose $w$ is an accepting walk. Then $S=T=\emptyset$, the pair
$(S^{\prime},T^{\prime})$ is cancellable, and $v=0$. Since
$(S^{\prime},T^{\prime})$ is cancellable, there is a $z\in\mathbb{N}^{m+\ell}$
with $z_{i}\geq 1$ for $i\in[1,m]$ such that $Az=0$. Since $x_{m+i}=0$ for
$i\in[1,\ell]$, we can find a number $M\in\mathbb{N}\setminus\\{0\\}$ such
that $Mz\geq x$. We set $y=Mz$ and since then $y\geq x$, we may apply our
observation above to this $y$. This yields a walk $w^{\prime}$ in
$\mathcal{A}$ from $(p,0)$ to $(q,v+Ay)=(q,0+MAz)=(q,0)$ such that
$w^{\prime}$ reads a superword of the word read by $w$. This means,
$w^{\prime}$ is accepting, so that the word read by $w$ is contained in
$L(\mathcal{A})\mathord{\downarrow}$. ∎

###### Proof of Lemma 5.3.

We may clearly assume that $|S_{2}\setminus S_{1}|=1$. Hence, let $(S_{1},T)$
be cancellable, $S_{1}=\\{u_{1},\ldots,u_{s}\\}$, and
$S_{2}=\\{u_{1},\ldots,u_{s+1}\\}$. Since
$\operatorname{span}(S_{1})=\operatorname{span}(S_{2})$, there are
$z_{1},\ldots,z_{s+1}\in\mathbb{Q}$ with $z_{s+1}\neq 0$ and
$\sum_{i=1}^{s+1}z_{i}u_{i}=0$. By multiplying with a common denominator and,
if necessary, switching the sign of the $z_{1},\ldots,z_{s+1}$, we may assume
that $z_{1},\ldots,z_{s}\in\mathbb{Z}$ and
$z_{s+1}\in\mathbb{N}\setminus\\{0\\}$.

Let $T=\\{v_{1},\ldots,v_{t}\\}$. Since $(S_{1},T)$ is cancellable, there are
are $x_{1},\ldots,x_{s}\in\mathbb{N}\setminus\\{0\\}$ and
$y_{1},\ldots,y_{t}\in\mathbb{N}$ with

$x_{1}u_{1}+\cdots+x_{s}u_{s}\leavevmode\nobreak\ \leavevmode\nobreak\
+\leavevmode\nobreak\ \leavevmode\nobreak\ y_{1}v_{1}+\cdots+y_{t}v_{t}=0.$

Since $x_{i}\geq 1$ for $i\in[1,s]$, we can find
$M\in\mathbb{N}\setminus\\{0\\}$ with $M\cdot x_{i}>-z_{i}$ for every
$i\in[1,s]$. Then, since $\sum_{i=1}^{s+1}z_{i}u_{i}=0$, we have

$\displaystyle 0$
$\displaystyle=M\left(\sum_{i=1}^{s}x_{i}u_{i}+\sum_{i=1}^{t}y_{i}v_{i}\right)+\sum_{i=1}^{s+1}z_{i}u_{i}=\sum_{i=1}^{s}(Mx_{i}+z_{i})u_{i}+z_{s+1}u_{s+1}+\sum_{i=1}^{t}(My_{i})v_{i}$

Since $Mx_{i}+z_{i}\in\mathbb{N}\setminus\\{0\\}$ for $i\in[1,s]$ and
$z_{s+1}\in\mathbb{N}\setminus\\{0\\}$, this proves that $(S_{2},T)$ is
cancellable. ∎

###### Proof of Lemma 5.4.

Let $S=\\{u_{1},\ldots,u_{s}\\}$ and choose $T^{\prime}\subseteq T$ minimal
with the property that $(S,T^{\prime})$ is cancellable. Let
$T^{\prime}=\\{v_{1},\ldots,v_{t}\\}$. Then there are
$x_{1},\ldots,x_{s}\in\mathbb{N}\setminus\\{0\\}$ and
$y_{1},\ldots,y_{t}\in\mathbb{N}$ with
$\sum_{i=1}^{s}x_{i}u_{i}+\sum_{i=1}^{t}y_{i}v_{i}=0$. By minimality of
$T^{\prime}$, we have $y_{i}>0$ for every $i\in[1,t]$. Suppose $T^{\prime}$ is
linearly dependent. Then there are $z_{1},\ldots,z_{t}\in\mathbb{Z}$, not all
zero, such that $\sum_{i=1}^{t}z_{i}v_{i}=0$. We may assume that at least one
$z_{i}$ is positive, because otherwise they are all at most zero and we can
negate them.

Choose $j\in[1,t]$ such that $z_{j}/y_{j}$ is maximal, meaning
$z_{j}/y_{j}\geq z_{i}/y_{i}$ for every $i\in[1,t]$. Note that then $z_{j}>0$
because otherwise, $z_{i}\leq 0$ for every $i\in[1,t]$. Then we have
$z_{j}y_{i}\geq y_{j}z_{i}$ for every $i\in[1,t]$ and hence

$\displaystyle
0=z_{j}\left(\sum_{i=1}^{s}x_{i}u_{i}+\sum_{i=1}^{t}y_{i}v_{i}\right)-y_{j}\left(\sum_{i=1}^{t}z_{i}v_{i}\right)=\sum_{i=1}^{s}(z_{j}x_{i})u_{i}+\sum_{i=1}^{t}\underbrace{(z_{j}y_{i}-y_{j}z_{i})}_{\geq
0}v_{i}.$

Since $z_{j}x_{i}>0$ for $i\in[1,s]$ and we have the coefficient
$z_{j}y_{j}-y_{j}z_{j}=0$ in front of $v_{j}$, the last equation tells us that
$(S,T^{\prime}\setminus\\{v_{j}\\})$ is cancellable. This contradicts the
choice of $T^{\prime}$. Therefore $T^{\prime}$ is linearly independent. ∎

###### Proof of Torollary 5.5.

Suppose we are given an ideal
$I=Y_{0}^{*}\\{x_{1},\varepsilon\\}Y_{1}^{*}\cdots\\{x_{\ell},\varepsilon\\}Y_{\ell}^{*}$
and a blind $k$-counter automaton $\mathcal{A}$ with $n$ states. By Theorem
5.1, we have an exponential bound upper bound $m$ on
$|L(\mathcal{A})|_{\mathsf{I}}$. According to Proposition 3.2, we have
$I\subseteq L(\mathcal{A})\mathord{\downarrow}$ if and only if
$w:=w_{Y_{0}}^{m}x_{1}w_{Y_{1}}^{m}\cdots x_{\ell}w_{Y_{\ell}}^{m}\in
L\mathord{\downarrow}$. Now the word $w$ may be exponentially long, but since
$m$ is at most exponential, we can compute $m$ in binary representation.

Given the polynomial-sized ideal and the binary representation of $m$, we can
construct a polynomial-sized straight-line program $\mathcal{G}$ for $w$: A
_straight-line program_ (SLP) is a context-free grammar that generates exactly
one word (see [27] for details and a survey). $\mathcal{G}$ is obtained from
an SLP for the polynomial-length word $z_{0}x_{1}z_{1}\cdots x_{\ell}z_{\ell}$
and SLPs for the words $w_{Y_{i}}^{m}$, which in turn result from an SLP for
$\\{a^{m}\\}$. The latter is easily constructed from the binary representation
of $m$.

Therefore, it remains to be shown that the _compressed membership problem_ for
blind counter automata is decidable in $\mathsf{NP}$. The latter asks, given
an SLP $\mathcal{G}$ and a blind counter automaton $\mathcal{A}$, whether the
word generated by $\mathcal{G}$ is accepted by $\mathcal{A}$. This can be
decided by constructing an automaton that has access to a pushdown and blind
(or reversal-bounded) counters that accepts $L(\mathcal{G})\cap
L(\mathcal{A})$. For such automata, the emptiness problem is in $\mathsf{NP}$,
as shown by [16] [16]. ∎

###### Proof of Theorem 5.6.

We show that for every $u\in L(\mathcal{A})$, there exists an ideal $I$ of
length at most $(5n)^{7(k+1)^{2}}$ with $u\in I\subseteq
L\mathord{\downarrow}$.

So let $w\in\Delta^{*}$ be an accepting walk of $\mathcal{A}$. We can write
$w=u_{0}v_{1}u_{1}\cdots v_{\ell}u_{\ell}$ such that
$u_{0},\ldots,u_{\ell}\in\Delta$, $|u_{0}\cdots u_{\ell}|\leq n$, and every
$v_{i}$ is a cycle. We factorize each $v_{i}=v_{i,1}\cdots v_{i,k_{i}}$ into
prime cycles $v_{i,1},\ldots,v_{i,k_{i}}$ and let Lemma 4.1 provide an
insertion tree $t_{i,j}$ of $v_{i,j}$ of height at most $n$.

Let $e_{1},\ldots,e_{m}\in\mathbb{Z}^{k}$ be the effects of cycles occurring
in any of these trees. Note that $\|e_{i}\|_{\infty}\leq n$ for $i\in[1,m]$,
so that $m\leq(3n)^{k}$. For $i\in[1,m]$, let
$x=(x_{1},\ldots,x_{m})\in\mathbb{N}^{m}$ be the vector such that $x_{i}$ is
the number of times a cycle with effect $e_{i}$ occurs. Moreover, let
$e\in\mathbb{Z}^{k}$ be the effect of $u_{0}\cdots u_{\ell}$. Then we have
$\|e\|_{\infty}\leq n$. Let $A\in\mathbb{Z}^{k\times m}$ be the matrix with
columns $e_{1},\ldots,e_{m}$. Since $w$ is accepting, we have $Ax=-e$. Note
that

$\|(A|e)\|_{1,\infty}\leq\|e\|_{\infty}+\sum_{i=1}^{m}\|e_{i}\|_{\infty}\leq(m+1)n\leq((3n)^{k}+1)n\leq(4n)^{k+1}$

and that the rank of $(A|e)$ is at most $k$. According to Theorem 5.2, there
is a $y\in\mathbb{N}^{m}$, $y\leq x$, such that $Ay=-e$ and
$\|y\|_{1}\leq(1+(4n)^{k+1})^{k+1}\leq(5n)^{(k+1)^{2}}$.

From our insertion trees, we now select for each $i\in[1,m]$, $y_{i}$-many
vertices whose cycles have effect $e_{i}$. This is possible since $y\leq x$.
Let $F$ be the set of these vertices. Then we have
$|F|\leq\|y\|_{1}\leq(5n)^{(k+1)^{2}}$. For each $i\in[0,\ell]$, let $a_{i}\in
X\cup\\{\varepsilon\\}$ be the input read by $u_{i}$. We claim that the
language

$K=a_{0}P(t_{1,1}\cdots t_{1,k_{i}},F)a_{1}\cdots P(t_{\ell,1}\cdots
t_{\ell,k_{\ell}},F)a_{\ell}$

is contained in $L(\mathcal{A})\mathord{\downarrow}$. Let
$z=(z_{1},\ldots,z_{m})\in\mathbb{N}^{m}$ be the vector with $z=x-y$. Then
$Az=0$ and every pumpable vertex has an effect $e_{i}$ where $z_{i}\geq 1$.

Now suppose we obtain a walk $w^{\prime}$ of $\mathcal{A}$ by performing some
pumping to obtain a word $u^{\prime}\in K$, either by duplicating a single
vertex or by duplicating a whole pumpable subtree. Note that it might happen
that $w^{\prime}$ does not leave the counters at zero in the end. But we will
show that we can pump even more to get such a walk. For each $i\in[1,m]$, let
$z^{\prime}_{i}\in\mathbb{N}$ be the number of times we add an occurrence of a
cycle with effect $e_{i}$. Let
$z^{\prime}=(z^{\prime}_{1},\ldots,z^{\prime}_{m})$. Since $z^{\prime}_{i}\geq
1$ implies $z_{i}\geq 1$, we can find an $N\in\mathbb{N}$ with $N\cdot z\geq
z^{\prime}$. Now for every $i\in[1,m]$ with $z^{\prime}_{i}\geq 1$, we can
find a pumpable vertex $v_{i}$ whose cycle has effect $e_{i}$. We can pump
$v_{i}$ an additional $Nz_{i}-z^{\prime}_{i}$ times. This results in a walk
$w^{\prime\prime}$ of $\mathcal{A}$ with effect $e+Ax+ANz=e+Ax=0$, meaning
that it is accepting. Moreover, if $u^{\prime\prime}$ is the input word read
by $w^{\prime\prime}$, then we have $u^{\prime}\preceq u^{\prime\prime}\in
L(\mathcal{A})$. This proves $K\subseteq L(\mathcal{A})\mathord{\downarrow}$,
which was our claim.

This means that the language

$I=K\mathord{\downarrow}=\\{a_{0},\varepsilon\\}P(t_{1,1}\cdots
t_{1,k_{1}},F)\mathord{\downarrow}\\{a_{1},\varepsilon\\}\cdots
P(t_{\ell,1}\cdots
t_{\ell,k_{\ell}},F)\mathord{\downarrow}\\{a_{\ell},\varepsilon\\}$

is contained in $L(\mathcal{A})\mathord{\downarrow}$. By Lemma 4.2, it is an
ideal and satisfies

$\displaystyle|I|_{\mathsf{E}}$
$\displaystyle\leq\ell+1+\sum_{i=1}^{\ell}|P(t_{i,1}\cdots
t_{i,k_{i}},F)\mathord{\downarrow}|_{\mathsf{E}}\leq
n+n^{2}\cdot|F|\cdot(2n+|F|)^{2}$
$\displaystyle\leq\left(2n^{2}\cdot(5n)^{(k+1)^{2}}\right)\cdot\left(2n+(5n)^{(k+1)^{2}}\right)^{2}$
$\displaystyle\leq\left((5n)^{3(k+1)^{2}}\right)\cdot(5n)^{4(k+1)^{2}}\leq(5n)^{7(k+1)^{2}},$

which completes our proof. ∎

##  Appendix D Context-Free Grammars

The following lemma remains to be shown.

######  Lemma D.1.

We have $a_{1}^{\omega}\cdots a_{n}^{\omega}\in L(\mathcal{G}^{\omega})$ if
and only if $a_{1}^{*}\cdots a_{n}^{*}\subseteq
L(\mathcal{G})\mathord{\downarrow}$.

###### Proof.

Suppose $a_{1}^{*}\cdots a_{n}^{*}\subseteq
L(\mathcal{G})\mathord{\downarrow}=L(\mathcal{G}^{\prime})$. Then there are
derivation trees $t_{1},t_{2},\ldots$ of $\mathcal{G}^{\prime}$ with
$|\mathsf{yield}(t_{j})|_{a_{i}}\geq j$ for every $i\in[1,n]$ and $j\geq 1$.

On the vertices of $t_{j}$, we define partial orders $\ll_{i}$ as follows. We
have $u\ll_{i}v$ if $v$ is a descendant of $u$ and
$|\mathsf{yield}(u)|_{a_{i}}>|\mathsf{yield}(v)|_{a_{i}}$. By induction on
$\ell$, it is easy to check that if all $\ll_{i}$-chains in $t_{j}$ have
length $\leq\ell$, then $|\mathsf{yield}(t_{j})|_{a_{i}}\leq 2^{\ell}$. Hence,
if $m>2^{|N|}$, then $|\mathsf{yield}(t_{m})|_{a_{i}}>2^{|N|}$, so that
$t_{m}$ must have a $\ll_{i}$-chain of length $>|N|$. On this chain, some
$A_{i}\in N$ has to repeat, meaning $A_{i}\in L_{i}\cup R_{i}$. We can
therefore expand $t_{m}$ by applying for each $i\in[1,n]$ the production
$A_{i}\to a_{i}^{\omega}A_{i}$ or $A_{i}\to A_{i}a_{i}^{\omega}$. Then, we
replace every $a_{i}$-leaf by $\varepsilon$. By construction, the resulting
tree $t$ is a derivation tree of $\mathcal{G}^{\omega}$ and every
$a_{i}^{\omega}$ appears exactly once. Hence, $\mathsf{yield}(t)$ is a
permutation of $a_{1}^{\omega}\cdots a_{n}^{\omega}$. It remains to be shown
that $\mathsf{yield}(t)=a_{1}^{\omega}\cdots a_{n}^{\omega}$.

Consider the morphism
$\alpha\colon\\{a_{1}^{\omega},\ldots,a_{n}^{\omega}\\}^{*}\to\\{a_{1},\ldots,a_{n}\\}^{*}$
such that for every $i\in[1,n]$, we have $\alpha(a_{i}^{\omega})=a_{i}$.
Recall that for every production $A\to a_{i}^{\omega}A$ or $A\to
Aa_{i}^{\omega}$ in $\mathcal{G}^{\omega}$, we have
$A\Rightarrow^{*}_{\mathcal{G}^{\prime}}a_{i}A$ or
$A\Rightarrow^{*}_{\mathcal{G}^{\prime}}Aa_{i}$, respectively. This tells us
that $\alpha(L(\mathcal{G}^{\omega}))\subseteq
L(\mathcal{G}^{\prime})\subseteq a_{1}^{*}\cdots a_{n}^{*}$. Therefore,
$\alpha(\mathsf{yield}(t))=a_{1}\cdots a_{n}$ and hence
$\mathsf{yield}(t)=a_{1}^{\omega}\cdots a_{n}^{\omega}$. ∎

##  Appendix E Hardness

###### Proof of Theorem 8.1.

We actually prove a stronger statement, namely that the following problem is
hard for $\mathsf{coNTIME}(t)$:

Given:

A description in $\mathcal{M}$ of the language $X^{\leq m}$ and a description
in $\mathcal{N}$ of a language $L\subseteq X^{\leq m}$, where $X$ is an
alphabet and $m\in\mathbb{N}$.

Question:

Does $X^{\leq m}\mathord{\downarrow}\subseteq L\mathord{\downarrow}$ hold?

This is clearly an instance of both
$\mathcal{M}\subseteq_{\mathord{\downarrow}}\mathcal{N}$ and of
$\mathcal{M}=_{\mathord{\downarrow}}\mathcal{N}$. If we show that already this
special case is hard, then so is the case of binary alphabets: Suppose
$X=\\{a_{1},\ldots,a_{k}\\}$ and let $\gamma\colon X^{*}\to\\{a,b\\}$ be the
morphism with $\gamma(a_{i})=a^{i}b^{k-i}$ for $i\in[1,k]$. Then clearly
$\gamma(X^{\leq m})\mathord{\downarrow}\subseteq\gamma(L)\mathord{\downarrow}$
if and only if $X^{\leq m}\mathord{\downarrow}\subseteq
L\mathord{\downarrow}$. Hence, we only show hardness for the problem above.

Let $K\subseteq Y^{*}$ belong to $\mathsf{coNTIME}(t)$. Then there is a
$t(n^{c})$-time-bounded ($c\geq 1$) Turing machine $M$ with one tape, tape
alphabet $Z\supseteq Y$ (which includes the blank symbol), and state set $Q$
that accepts the complement of $K$.

Our goal is to construct the language $L\subseteq X^{\leq m}$ in such a way
that the words in $L$ of length $m$ are precisely those words that do not
encode an accepting computation of $M$. Here, $m$ will be chosen so that if
$M$ has an accepting computation, it is encoded by a word of length $m$. Then,
we will have $X^{\leq m}\mathord{\downarrow}\subseteq L\mathord{\downarrow}$
if and only if $M$ does not accept the given input word. Our first task is to
find a suitable $m$.

Observe that a monotone function $h\colon\mathbb{N}\to\mathbb{N}$ is
amplifying if and only if $h(n)\geq n$ for $n\geq 0$ and there is a $d\geq 1$
such that $h(n^{d})\geq h(n)^{2}$ for large enough $n$. Let
$g\colon\mathbb{N}\to\mathbb{N}$ be defined as $g(n)=t(n^{c})$. Since $t$ is
amplifying, $g$ is as well: for some constant $d$, we have
$g(n^{d})=t(n^{cd})\geq t(n^{c})^{2}=g(n)^{2}$ for large enough
$n\in\mathbb{N}$. Since $g$ is amplifying, there is a constant $e\geq 1$ such
that $g(n^{e})\geq g(n)\cdot(g(n)+2)$ for all $n\geq n_{0}$. We define
$f(n)=g(n^{e})$.

With these choices, we have: $M$ is time bounded by $g$, the models
$\mathcal{M}$ and $\mathcal{N}$ are $\Delta(g)$ and $\Delta(f)$, and $f(n)\geq
g(n)\cdot(g(n)+2)$ for $n\geq n_{0}$.

Now fix $w\in Y^{*}$ and let $n=|w|$. For the reduction, it means no loss of
generality to assume $n\geq n_{0}$. We choose $m=f(n)+g(n)+3$. We encode a
configuration of $M$ by a word $uqv$, where $u,v\in Z^{*}$, $q\in Q$, and
$|uv|=g(n)$ (recall that $M$ is $g$-time-bounded and hence $g$-space-bounded).
It means that $M$ is in state $q$ and its head is at the first position of
$v$. A computation is then encoded as a word $\\#u_{1}\\#\cdots
u_{k}\\#u_{k+1}$, where $u_{1},\ldots,u_{k}$ encode the configurations of the
computation (in this order) and $u_{k+1}$ is any suffix in $Z^{*}$. Since
$m=f(n)+g(n)+3\geq g(n)\cdot(g(n)+3)$ and $M$ is $g$-time-bounded, all
computations have encodings where $|\\#u_{1}\cdots\\#u_{k+1}|=m$.

Since $\mathcal{M}$ and $\mathcal{N}$ are $\Delta(g)$ and $\Delta(f)$, we can
construct for each model finite languages whose longest word has length $g(n)$
or $f(n)$, respectively. By applying a homomorphism and taking the downward
closure, we can thus construct descriptions of
$\\{a^{g(n)}\\}\mathord{\downarrow}$ and of
$\\{a^{f(n)}\\}\mathord{\downarrow}$ in each of the models, in polynomial
time. Let $X=Z\cup Q\cup\\{\\#\\}$. Using rational transductions and simple
substitutions, we get $X^{\leq m}=X^{f(n)+g(n)+3}\mathord{\downarrow}$ in
$\mathcal{M}$ and

$L_{1}=\\{a^{i}\\#a^{g(n)+1}\\#a^{f(n)-i}\mid
i\in[0,f(n)]\\}\mathord{\downarrow}$

in $\mathcal{N}$. Note that $L_{1}\subseteq\\{a,\\#\\}^{\leq m}$.

In the rest of the proof, we construct a (polynomial-sized) rational
transduction $T$ such that $TL_{1}\subseteq X^{\leq m}$ and $(TL_{1})\cap
X^{m}$ contains precisely those words that do not encode a computation of $M$
that accepts $w$. Then, we have clearly shown that the problem described at
the beginning of the proof is hard for $\mathsf{coNTIME}(t)$.

A word $u\in X^{*}$ of length $m$ can fail to be an accepting computation for
$w$ for the following reasons. We decompose
$u=u_{0}\\#u_{1}\\#\cdots\\#u_{k+1}$.

  1. 1.

It does not begin with $\\#$, i.e. $u_{0}\neq\varepsilon$.

  2. 2.

Two $\\#$’s are less than $g(n)+1$ positions apart.

  3. 3.

Two $\\#$’s are more than $g(n)+1$ positions apart (without a $\\#$ in
between).

  4. 4.

Some $u_{i}$ is not contained in $Z^{*}QZ^{*}$.

  5. 5.

The first configuration $u_{1}$ is not an initial configuration with input
$w$.

  6. 6.

The last configuration, i.e. $u_{k}$, is not accepting.

  7. 7.

For some $i\in[1,k-1]$, the configuration $u_{i}$ cannot reach $u_{i+1}$ in
one step.

For each of the cases 1, 2, 3, 4, 5, 6 and 7, we shall explain how to obtain a
transduction that generates those words from $L_{1}$. If we then have rational
transductions $T_{1},\ldots,T_{7}$, we take the rational transduction
$T=T_{1}\cup\cdots\cup T_{7}$, which is clearly as desired above.

Note that the cases 1, 4, 5 and 6 are trivial, so we consider cases 2, 3 and
7. For 2, notice that with a constant-sized rational transduction $R_{<}$, one
can obtain

$P_{<}=\\{a^{i}\\#a^{\ell}\\#a^{g(n)+1-\ell}a^{f(n)-i}\mid
i\in[0,f(n)],\leavevmode\nobreak\ \ell\in[0,g(n)+1]\\}\mathord{\downarrow}.$

as $R_{<}L_{1}$. Indeed, $R_{<}$ reads a word from $L_{1}$ and outputs every
letter as read, up to the first $\\#$. Then, before it sees the second $\\#$
in the input, it nondeterministically chooses a time to output $\\#$ early.
Then, it reads the rest of the input and outputs $a$ for each input letter, be
it $a$ or $\\#$. Using a similar strategy, one can obtain

$P_{>}=\\{a^{i}\\#a^{g(n)+1+\ell}\\#a^{f(n)-i-\ell}\mid
i\in[0,f(n)],\leavevmode\nobreak\ \ell\in[0,f(n)-i]\\}\mathord{\downarrow}$

using a constant-sized rational transduction $R_{>}$. Now from $P_{<}$ and
$P_{>}$, it is easy to obtain all words of case 2 and 3, respectively.

The case 7 is also not hard to realize with $L_{1}$ as input. We only have to
make sure that either the immediate surrounding of the head is not updated
properly or the rest of the tape is not copied correctly. For words of length
$m$ (and those are the only ones where we must produce an incorrect encoding),
the input language $L_{1}$ gives us, with the two $\\#$’s, two pointers that
are precisely $g(n)+1$ positions apart. We can therefore guarantee that at
least one of these errors is present. The details are very straightforward. ∎

###### Proof of Torollary 8.2.

According to Theorem 8.1, it suffices to show that each
$\mathcal{M}\in\\{\mathsf{CFG},\mathsf{RBC}\\}$ is $\Delta(2^{n})$.

For $\mathsf{CFG}$, we can take the well-known grammar with nonterminals
$A_{0},\ldots,A_{n}$, start symbol $A_{n}$, and productions $A_{i}\to
A_{i-1}A_{i-1}$ for $i\in[1,n]$, and $A_{0}\to a$. It clearly generates
$\\{a^{2^{n}}\\}$.

For $\mathsf{RBC}$, we use a blind $(n+1)$-counter automaton. We increment the
first counter once and then, for each $i=1,\ldots,n$, we count down counter
$i$ and simultaneously count up counter $i+1$ at twice the speed. After these
$n$ phases, counter $n+1$ contains the value $2^{n}$. Then, we count down
counter $n+1$ and each time read an $a$. Hence, we accept $\\{a^{2^{n}}\\}$. ∎

###### Proof of Proposition 8.5.

The _generalized subset sum problem_ is the following:

Given:

Two vectors $u,v\in\mathbb{N}^{n}$ and $t\in\mathbb{N}$, encoded in binary.

Question:

Is it true that for every $x\in\\{0,1\\}^{n}$, there exists a
$y\in\\{0,1\\}^{n}$ that satisfies $\langle u,x\rangle+\langle v,y\rangle=t$?

Here, $\langle w,z\rangle$ denotes the scalar product of
$w,z\in\mathbb{Z}^{n}$. This problem is known to be
$\Pi_{2}^{\mathsf{P}}$-complete [6].

We identify vectors over $\\{0,1\\}$ of length $n$ with words over $\\{0,1\\}$
of length $n$. Let $u,v\in\mathbb{N}^{n}$ and $t\in\mathbb{N}$ be an instance
of the generalized subset sum problem and suppose each entry of $u$ and $v$ is
encoded with $k$ bits. Like in Torollary 8.2, we can easily construct an RBCA
$\mathcal{A}$ with $3k$ counters that accepts $\\{x\in\\{0,1\\}^{n}\mid\exists
y\in\\{0,1\\}^{n}\colon\langle u,x\rangle+\langle v,y\rangle=t\\}$: As it
reads $x$, it uses counters $1,\ldots,k$ to build up $\langle u,x\rangle$ in
counter $k$. Then, it guesses $y$ bit-by-bit while using counters
$k+1,\ldots,2k$ to build up $\langle v,y\rangle$ in counter $2k$. Afterwards,
it accumulates $t$ in counter $3k$ using counters $2k+1,\ldots,3k$. Finally,
it counts down counter $3k$ one-by-one and in each step, decrements counter
$k$ or $2k$. In the end, all counters are zero if and only if $\langle
u,x\rangle+\langle v,y\rangle=t$.

Let $\mathcal{B}$ be the obvious $(n+1)$-state NFA that accepts
$\\{0,1\\}^{n}$. Then we clearly have
$L(\mathcal{B})\mathord{\downarrow}\subseteq
L(\mathcal{A})\mathord{\downarrow}$ if and only if our instance of the
generalized subset sum problem is positive. ∎