15415 LABEL:LastPageApr. 09, 2019Dec. 18, 2019

# On Functions Weakly Computable by Pushdown Petri Nets and Related Systems

Jérôme Leroux  LaBRI, Univ. Bordeaux & CNRS, France  ,  M Praveen  Chennai
Mathematical Institute, India  ,  Philippe Schnoebelen  LSV, ENS Paris-Saclay
& CNRS, France  and  Grégoire Sutre  LaBRI, Univ. Bordeaux & CNRS, France

###### Abstract.

We consider numerical functions weakly computable by grammar-controlled vector
addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly
compute all fast growing functions $F_{\alpha}$ for $\alpha<\omega^{\omega}$,
hence they are computationally more powerful than standard vector addition
systems. On the other hand they cannot weakly compute the inverses
$F_{\alpha}^{-1}$ or indeed any sublinear function. The proof relies on a
pumping lemma for runs of GVASes that is of independent interest.

###### Key words and phrases:

Petri nets, pushdown vector addition systems, weak computation, fast-growing
functions, pumping lemma

This work was partly supported by grant ANR-17-CE40-0028 of the French
National Research Agency ANR (project BRAVAS), and by the Indo-French CNRS UMI
2000 ReLaX.

##  1\. Introduction

Pushdown Petri nets are Petri nets extended with a pushdown stack. They have
been used to model asynchronous programs [34] and, more generally, recursive
programs with integer variables [2]. They sometimes appear under a different
but essentially equivalent guise: stack/pushdown/context-free vector addition
systems [19, 22, 26], partially blind multi-counter machines [10] with a
pushdown stack, etc. It is not yet known whether reachability is decidable for
pushdown Petri nets and this is one of the major open problems in computer
science. However, a series of recent results improved our understanding of the
computational power of these models: coverability, reachability and
boundedness are Tower-hard [19, 21], and boundedness is solvable in hyper-
Ackermannian time [22].

With the present article, we contribute to this line of work. We recall
_Grammar-Controlled Vector Addition Systems_ [26], or GVAS, a variant model,
close to Pushdown Petri nets, where the pushdown stack is replaced by a
context-free restriction on the firing of rules. The runs are now naturally
organized in a derivation tree, and the stack is not actually present in the
configurations: this leads to a simplified mathematical treatment, where the
usual monotonicity properties of VASes can be put to use.

As a step towards understanding the expressive power of these GVASes, we
consider the number-theoretical functions that are _weakly computable_ in this
model. Restricting to weakly computing a numerical function is a natural idea
when dealing with models like VASes and GVASes that lack zero-tests, or, more
precisely, that cannot initiate a given action on the condition that a
counter’s value is zero, only on the condition that it is not zero.

This notion has been used since the early days of Petri nets and has proved
very useful in hardness or impossibility proofs: For Petri nets and VASSes,
the undecidability of equivalence problems, and the Ackermann-hardness of the
same problems for bounded systems, have been proved using the fact that
multivariate polynomials with positive integer coefficients —aka positive
Diophantine polynomials— and, respectively, the fast-growing functions
$(F_{i})_{i\in{\mathbb{N}}}$ in the Grzegorczyk hierarchy, are all weakly
computable [12, 28, 16]. More recently, the nonelementary complexity lower
bound for VASS reachability is obtained thanks to a uniform (polynomial size)
family of systems computing (exactly) $n$-EXP(2) from $n$ [5].

The above results rely on showing how _some_ useful functions are weakly
computable by Petri nets and VASSes. But not much is known about exactly which
functions are weakly computable or not. It is known that all such functions
are monotonic. They are all primitive-recursive. The class of weakly
computable functions is closed under composition.

In this article, we show that functions weakly computable by GVASes go beyond
those weakly computable by VASSes, in particular we show how to weakly compute
the Fast Growing $(F_{\alpha})$ for all $\alpha<\omega^{\omega}$.

A folklore conjecture states that the inverses of the fast-growing functions
are not weakly computable by Petri nets. It is stated as fact in [32, p.252]
but no reference is given. In this article, we settle the issue by proving
that any unbounded function weakly computable by Petri nets and more generally
by GVASes is in $\Omega(x)$, i.e., it eventually dominates $c\cdot x$ for some
constant $c>0$. Thus any function that is sublinear, like
$x\mapsto\lfloor\sqrt{x}\rfloor$, or $x\mapsto\lfloor\log x\rfloor$, is not
weakly computable by GVASes. The proof technique is interesting in its own
right: it relies on a pumping lemma on runs of GVASes that could have wider
applications. This pumping lemma follows from a well-quasi-ordering on the set
of runs that further directs it.

### Beyond Petri nets and VASSes.

Petri nets and VASSes are a classic example of well-structured systems [1, 8].
In recent years, weakly computing numerical functions has proved to be a
fundamental tool for understanding the expressive power and the complexity of
some families of well-structured systems that are more powerful than Petri
nets and VASSes [33, 14, 11]. For such systems, the hardness proofs rely on
weakly computing fast-growing functions $(F_{\alpha})_{\alpha\in\textit{Ord}}$
that extend Grzegorczyk’s hierarchy. These hardness proofs also crucially rely
on weakly computing the inverses of the $F_{\alpha}$’s.

There are several extensions of Petri nets for which reachability (or
coverability or boundedness) remains decidable: nets with nested zero-tests
[30], recursive VASSes [3] and Branching VASSes [7], VASSes with pointers to
counters [6], unordered data Petri nets [20], etc., and of course pushdown
VASes and GVASes. For the latter, while coverability and reachability are
still open in general, partial decidability results have been obtained by
looking at sub-classes, namely GVASes with finite-index grammars [2] and
GVASes of dimension one [26]. In many cases, it is not known how these
extensions compare in expressive power and in complexity. We believe that
weakly computable functions can be a useful tool when addressing these
questions.

### Related models.

The GVAS model can simulate counter machines extended with nested zero-tests
(from [30]), and the vector addition systems extended with a pushdown stack
(from [22]). The first simulation was shown in [2] and holds even for GVASes
with finite-index grammars. The second one comes from the classical
transformation of a pushdown automaton into a context-free grammar that
recognizes the same language. There exists still other models that extend
vector addition systems with stack-related mechanisms, e.g., Mayr’s Process
Rewrite Systems [29] or Haddad and Poitrenaud’s Recursive Petri Nets [13].
Pending some further, more formal, comparison, it seems that these models are
less expressive than Pushdown VASes since they only allow limited interactions
between stack and counters.

### Outline of the paper.

Section 2 introduces GVASes and fixes some notation. In Section 3, we
introduce flow trees, a tree-shaped version of runs of GVASes for which we
develop our two main tools: a well-quasi-ordering between flow trees and an
Amalgamation Theorem. The following two sections explore applications of the
Amalgamation Theorem in understanding the computing power of GVASes: via GVAS-
definable sets in Section 4, via weakly computable function in Section 5.
Finally, we show in Section 6 that GVASes can weakly compute all Fast-Growing
functions $F_{\alpha}$ for $\alpha<\omega^{\omega}$.

##  2\. Grammar-Controlled Vector Addition Systems

This section recalls the model of grammar-controlled vector addition systems,
originally from [26]. In a nutshell, these are intersections of classical VAS
with context-free grammars. Remark 2.3 relates them with the equivalent model
of pushdown vector addition systems.

### Vector Addition Systems

For a _dimension_ $d\in{\mathbb{N}}$, we consider _configurations_ that are
vectors ${\mathbf{c}},{\mathbf{d}},{\mathbf{x}},{\mathbf{y}},\ldots$ in
${\mathbb{N}}^{d}$, and _actions_ that are vectors
$\mathbf{a}\in{\mathbb{Z}}^{d}$. We write
${\mathbf{x}}\xrightarrow{{\mathbf{a}}}{\mathbf{y}}$ for two configurations
${\mathbf{x}},{\mathbf{y}}$ in ${\mathbb{N}}^{d}$ if
${\mathbf{y}}={\mathbf{x}}+{\mathbf{a}}$. A _vector addition system_ (a _VAS_)
is a transition system of the form
$({\mathbb{N}}^{d},\\{\xrightarrow{{\mathbf{a}}}\\}_{{\mathbf{a}}\in\mathbf{A}})$
generated by a finite set $\mathbf{A}\subseteq{\mathbb{Z}}^{d}$ of actions.

In a VAS, the one-step transition relations
$\\{\xrightarrow{{\mathbf{a}}}\\}_{{\mathbf{a}}\in\mathbf{A}}$ are composed in
a natural way: with any word
$w=\mathbf{a}_{1}\cdots{\mathbf{a}}_{k}\in\mathbf{A}^{*}$ of actions, we
associate the binary relation $\xrightarrow{w}$ defined over configurations by
$\mathbf{x}\xrightarrow{w}\mathbf{y}$ iff there exists a sequence
$\mathbf{c}_{0},\ldots,\mathbf{c}_{k}$ of configurations such that
$\mathbf{c}_{0}=\mathbf{x}$, $\mathbf{c}_{k}=\mathbf{y}$ and such that
$\mathbf{c}_{j-1}\xrightarrow{{\mathbf{a}}_{j}}\mathbf{c}_{j}$ for every
$1\leq j\leq k$. Those relations are monotonic:

$\mathbf{x}\xrightarrow{w}\mathbf{y}\text{ and
}\mathbf{v}\in{\mathbb{N}}^{d}\text{ implies
}\mathbf{x}+\mathbf{v}\xrightarrow{w}\mathbf{y}+\mathbf{v}\>.$ (1)

### Notation

When writing configurations ${\mathbf{c}}\in{\mathbb{N}}^{d}$, we sometimes
split the vector in parts, writing e.g.,
${\mathbf{c}}=({\mathbf{x}},{\mathbf{y}})$ for some
${\mathbf{x}}\in{\mathbb{N}}^{d_{1}}$ and
${\mathbf{y}}\in{\mathbb{N}}^{d_{2}}$ with $d=d_{1}+d_{2}$. We also write
${\mathbf{0}}_{d}$ for the null vector in ${\mathbb{N}}^{d}$, often leaving
the dimension implicit.

### Grammar-controlled Vector Addition Systems

A $d$-dimensional _grammar-controlled vector addition system_ (a _GVAS_) can
be seen as a context-free grammar using terminals from ${\mathbb{Z}}^{d}$, or
equivalently as a VAS where the valid sequences of actions are generated by a
context-free grammar. Formally, a $d$-dimensional GVAS is some
$G=(V,\mathbf{A},R,S)$ where $V$ is a finite set of _nonterminals_ , where
$\mathbf{A}\subseteq{\mathbb{Z}}^{d}$ is a finite set of terminals called
_actions_ , where $R\subseteq V\times(V\cup\mathbf{A})^{*}$ is a finite set of
production _rules_ , and $S\in V$ is the _start symbol_. Following the usual
convention, a rule $(T,u)$ is also written $T\rightarrow u$. We denote
nonterminals from $V$ with capital letters like $S,T,\ldots$ while symbols
from the larger set $V\cup\mathbf{A}$ are denoted with $X,Y,\ldots$. Words in
$(V\cup\mathbf{A})^{*}$ are denoted with $w,u,v,\ldots$. As usual,
$\varepsilon$ denotes the empty word.

For all words $w,w^{\prime}\in(V\cup\mathbf{A})^{*}$, we say that
$w\xLongrightarrow{}w^{\prime}$ is a _derivation step_ of $G$ if there exist
two words $v,v^{\prime}$ in $(V\cup\mathbf{A})^{*}$ and a rule $(T,u)$ in $R$
such that $w=vTv^{\prime}$ and $w^{\prime}=vuv^{\prime}$. Let
$\xLongrightarrow{*}$ denote the reflexive and transitive closure of
$\xLongrightarrow{}$. The language $L_{G}\subseteq\mathbf{A}^{*}$ generated by
$G$ seen as a grammar is defined as usual with $w\in
L_{G}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{\Leftrightarrow}}S\xLongrightarrow{*}w\in\mathbf{A}^{*}$. More
generally, for any $u\in(V\cup\mathbf{A})^{*}$, the language $L_{G}(u)$ is
$\\{w\in\mathbf{A}^{*}\leavevmode\nobreak\ |\leavevmode\nobreak\
u\xLongrightarrow{*}w\\}$.

When $G$ is a GVAS, we are interested in what sequences of actions may occur
between configurations in ${\mathbb{N}}^{d}$. For this, we extend the
definition of the $\xrightarrow{w}$ relation and consider $\xrightarrow{u}$
for any $u\in(V\cup\mathbf{A})^{*}$. Formally, we let

$\displaystyle\mathbf{x}\xrightarrow{u}\mathbf{y}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{\Leftrightarrow}}\exists w\in
L_{G}(u):\mathbf{x}\xrightarrow{w}\mathbf{y}\>.$ (2)

A labeled pair ${\mathbf{x}}\xrightarrow{u}{\mathbf{y}}$ is called a _run_ of
the GVAS, and should not be confused with the derivations
$w\xLongrightarrow{*}w^{\prime}$ that only involve the grammar part.

Like VASes, GVASes are monotonic:

$\mathbf{x}\xrightarrow{u}\mathbf{y}\text{ and
}\mathbf{v}\in{\mathbb{N}}^{d}\text{ implies
}\mathbf{x}+\mathbf{v}\xrightarrow{u}\mathbf{y}+\mathbf{v}\>.$ (3)

The underlying grammar $G$ is left implicit in the above notation. We
sometimes write ${\mathbf{x}}\xrightarrow{G}{\mathbf{y}}$ instead of
${\mathbf{x}}\xrightarrow{S}{\mathbf{y}}$, where $S$ is the start symbol of
$G$, when several grammars are considered simultaneously.

######  Example 2.1.

Let $d=1$, $V=\\{S,T\\}$, and consider the 1-dimensional GVAS given by the
following four rules in Backus-Naur form:

$\displaystyle S$ $\displaystyle\rightarrow\mathbf{1}\leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \mathbf{-1}\,S\,T\>,$ $\displaystyle T$
$\displaystyle\rightarrow\mathbf{0}\leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \mathbf{-1}\,T\,\mathbf{2}\>.$

Since we shall claim in Section 5 that this GVAS weakly computes the $2^{n}$
function, let us state and prove the main properties of its runs. Formally,
for every $k,k^{\prime},n,n^{\prime}\in{\mathbb{N}}$, one has:

$\displaystyle k\xrightarrow{T}k^{\prime}$ $\displaystyle\text{ iff }k\leq
k^{\prime}\leq 2k\>,$ $\displaystyle n\xrightarrow{S}n^{\prime}$
$\displaystyle\text{ iff }1\leq n^{\prime}\leq 2^{n}\>.$ (4)

Thus, even in dimension 1, the reachability relation may not be semilinear.

To prove (4) assume first that $k\xrightarrow{T}k^{\prime}$ for some natural
numbers $k,k^{\prime}$. There exists $m\in{\mathbb{N}}$ such that
$k\xrightarrow{\mathbf{-1}^{m}\mathbf{0}\mathbf{2}^{m}}k^{\prime}$. In
particular $m\leq k$ and $k^{\prime}=k+m$. We deduce that $k\leq
k^{\prime}\leq 2k$. Conversely, let $k,k^{\prime}$ be two natural numbers such
that $k\leq k^{\prime}\leq 2k$. Observe that
$T\xLongrightarrow{*}\mathbf{-1}^{n}\mathbf{0}\mathbf{2}^{n}$ where $n$ is
defined as $k^{\prime}-k$. The following relations show that
$k\xrightarrow{T}k^{\prime}$:

$k\leavevmode\nobreak\ \xrightarrow{\mathbf{-1}^{n}}\leavevmode\nobreak\
k-n\leavevmode\nobreak\ \xrightarrow{\mathbf{0}}\leavevmode\nobreak\
k-n\leavevmode\nobreak\ \xrightarrow{\mathbf{2}^{n}}\leavevmode\nobreak\
k^{\prime}\>.$

Now, assume that $n\xrightarrow{S}n^{\prime}$ for some natural numbers
$n,n^{\prime}$, There exists $m\in{\mathbb{N}}$ such that
$n\xrightarrow{\mathbf{-1}^{m}\mathbf{1}T^{m}}n^{\prime}$. It follows that
$m\leq n$, and from the previous paragraph, we deduce that
$n^{\prime}\leq(n-m+1)2^{m}\leq 2^{n}$ by observing that $x+1\leq 2^{x}$ for
every $x\in{\mathbb{N}}$ and by replacing $x$ by $n-m$. Conversely, let
$n,n^{\prime}$ be two natural numbers such that $1\leq n^{\prime}\leq 2^{n}$.
Observe that $S\xLongrightarrow{*}\mathbf{-1}^{n}\mathbf{1}T^{n}$. Let us
introduce a natural number $m$ in $\\{0,\ldots,n-1\\}$ such that $2^{m}\leq
n^{\prime}\leq 2^{m+1}$. The following relations show that
$n\xrightarrow{S}n^{\prime}$:

$n\xrightarrow{\mathbf{-1}^{n}}0\xrightarrow{\mathbf{1}}2^{0}\xrightarrow{T}2^{1}\cdots\xrightarrow{T}2^{m}\xrightarrow{T}n^{\prime}\xrightarrow{T^{n-1-m}}n^{\prime}\>.$
∎

######  Example 2.2.

Let $G$ be the 2-dimensional GVAS with a single nonterminal symbol and the
following three rules:

$S\rightarrow S\,S\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\
\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle
2\end{array}\bigr{)}\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\
\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle 2\\\\[-5.0pt]
\scriptstyle-1\end{array}\bigr{)}\>.$

Let $w=\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle
2\end{array}\bigr{)}\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle 2\\\\[-5.0pt]
\scriptstyle-1\end{array}\bigr{)}\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle 2\end{array}\bigr{)}$ and observe that $S\xLongrightarrow{*}w$.
We have $\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle 2\\\\[-5.0pt]
\scriptstyle
2\end{array}\bigr{)}\xrightarrow{\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle 2\end{array}\bigr{)}}\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
1\\\\[-5.0pt] \scriptstyle
4\end{array}\bigr{)}\xrightarrow{\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
2\\\\[-5.0pt]
\scriptstyle-1\end{array}\bigr{)}}\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
3\\\\[-5.0pt] \scriptstyle
3\end{array}\bigr{)}\xrightarrow{\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle 2\end{array}\bigr{)}}\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
2\\\\[-5.0pt] \scriptstyle 5\end{array}\bigr{)}$ and hence
$\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle 2\\\\[-5.0pt] \scriptstyle
2\end{array}\bigr{)}\xrightarrow{S}\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
2\\\\[-5.0pt] \scriptstyle 5\end{array}\bigr{)}$. ∎

######  Remark 2.3.

It is well known that, from a formal language viewpoint, context-free grammars
are equivalent to pushdown automata. Similarly, GVAS can be equivalently
presented as VAS extended with a pushdown stack. Formally, a $d$-dimensional
_Pushdown Vector Addition System_ (a _PVAS_) is a transition system of the
form
$({\mathbb{N}}^{d}\times\Gamma^{*},\\{\xrightarrow{{\mathbf{p}}}\\}_{{\mathbf{p}}\in\mathbf{P}})$
generated by a pair $(\Gamma,\mathbf{P})$ where $\Gamma$ is a finite _stack
alphabet_ and
$\mathbf{P}\subseteq\Gamma^{*}\times\Gamma^{*}\times{\mathbb{Z}}^{d}$ is a
finite set of _actions_. So configurations are now pairs $(\mathbf{x},u)$
where $\mathbf{x}\in{\mathbb{N}}^{d}$ is as for VAS and $u\in\Gamma^{*}$ is a
word denoting the contents of the stack. Intuitively, an action
${\mathbf{p}}=(\alpha,\beta,\mathbf{a})$ pops the string $\alpha$ from the top
of the stack, then pushes the string $\beta$ onto the top of the stack, and
adds $\mathbf{a}$ to the vector of natural numbers. Formally, each action
$(\alpha,\beta,\mathbf{a})\in\mathbf{P}$ induces a binary relation
$\xrightarrow{(\alpha,\beta,\mathbf{a})}$ on configurations defined by
$(\mathbf{x},u)\xrightarrow{(\alpha,\beta,\mathbf{a})}(\mathbf{y},v)$ if
$\mathbf{y}=\mathbf{x}+\mathbf{a}$ and there exists $w$ such that $u=\alpha w$
and $v=\beta w$. GVASes can be translated into equivalent PVASes and vice-
versa.

For instance, the PVAS corresponding to Example 2.2 is generated by the pair
$(\Gamma,\mathbf{P})$ where $\Gamma=\\{S\\}$ and $\mathbf{P}$ is the set of
actions $\\{(S,SS,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle 0\\\\[-5.0pt]
\scriptstyle
0\end{array}\bigr{)}),(S,\varepsilon,\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle
2\end{array}\bigr{)}),(S,\varepsilon,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
2\\\\[-5.0pt] \scriptstyle-1\end{array}\bigr{)})\\}$. Corresponding to
$\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle 2\\\\[-5.0pt] \scriptstyle
2\end{array}\bigr{)}\xrightarrow{w}\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
2\\\\[-5.0pt] \scriptstyle 5\end{array}\bigr{)}$ with
$w=\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle
2\end{array}\bigr{)}\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle 2\\\\[-5.0pt]
\scriptstyle-1\end{array}\bigr{)}\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle 2\end{array}\bigr{)}$ there, we have

$(S,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle 2\\\\[-5.0pt] \scriptstyle
2\end{array}\bigr{)})\xrightarrow{\\!S,SS,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
0\\\\[-5.0pt] \scriptstyle
0\end{array}\bigr{)}\\!}(SS,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
2\\\\[-5.0pt] \scriptstyle
2\end{array}\bigr{)})\xrightarrow{\\!S,\varepsilon,\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle
2\end{array}\bigr{)}\\!}(S,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
1\\\\[-5.0pt] \scriptstyle
4\end{array}\bigr{)})\xrightarrow{\\!S,SS,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
0\\\\[-5.0pt] \scriptstyle
0\end{array}\bigr{)}\\!}(SS,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
1\\\\[-5.0pt] \scriptstyle
4\end{array}\bigr{)})\xrightarrow{\\!S,\varepsilon,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
2\\\\[-5.0pt]
\scriptstyle-1\end{array}\bigr{)}\\!}(S,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
3\\\\[-5.0pt] \scriptstyle
3\end{array}\bigr{)})\xrightarrow{\\!S,\varepsilon,\bigl{(}\begin{array}[]{<EMAIL_ADDRESS>\scriptstyle
2\end{array}\bigr{)}\\!}(\varepsilon,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
2\\\\[-5.0pt] \scriptstyle 5\end{array}\bigr{)})$

in the PVAS.

##  3\. Well-Quasi-Ordering Runs in GVASes

In this section we define flow trees of GVASes and show that they satisfy an
amalgamation property. This property is used in the next section to provide a
geometrical decomposition of GVAS sets, and in the following section to show
that unbounded weakly computable functions are in $\Omega(n)$.

Let $G=(V,\mathbf{A},R,S)$ be a $d$-dimensional GVAS. _Flow trees_ of $G$ are
trees that combine a transition ${\mathbf{x}}\xrightarrow{w}{\mathbf{y}}$ in
the VAS part of $G$ with a derivation tree for the corresponding
$S\xLongrightarrow{*}w$ in the grammar part of $G$.

Flow trees are finite rooted ordered trees labeled with transitions of $G$: we
write $t=\sigma[t_{1},\ldots,t_{\ell}]$ to denote a flow tree $t$ made of a
root with $\ell$ subtrees $t_{1},\ldots,t_{\ell}$. The root is labeled by a
transition $\sigma$ of $G$, of the form
${\mathbf{c}}\xrightarrow{X}{\mathbf{d}}$ with $X\in V\cup\mathbf{A}$. We
write $\operatorname{root}(t)=\sigma$. Formally, $F(G)$ is the least set of
trees that contains all
$({\mathbf{c}}\xrightarrow{{\mathbf{a}}}{\mathbf{d}})[]$ with
${\mathbf{a}}\in\mathbf{A}$ and ${\mathbf{c}}+{\mathbf{a}}={\mathbf{d}}$, and
all $({\mathbf{c}}\xrightarrow{T}{\mathbf{d}})[t_{1},\ldots,t_{\ell}]$ with
$T\in V$ and $t_{1},\ldots,t_{\ell}\in F(G)$ such that there is a rule $T$ in
$R$ and configurations
${\mathbf{c}}_{0},{\mathbf{c}}_{1},\ldots,{\mathbf{c}}_{\ell}$ with
${\mathbf{c}}_{0}={\mathbf{c}}$, ${\mathbf{c}}_{\ell}={\mathbf{d}}$ and such
that, for $i=1,\ldots,\ell$, the root of $t_{i}$ is labeled with
${\mathbf{c}}_{i-1}\xrightarrow{X_{i}}{\mathbf{c}}_{i}$. A _subtree_ of
$t=\sigma[t_{1},\ldots,t_{\ell}]$ is either $t$ itself or a subtree of some
$t_{i}$ for $i=1,\ldots,\ell$. A (sub)tree
$({\mathbf{c}}\xrightarrow{X}{\mathbf{d}})[t_{1},\ldots,t_{\ell}]$ is a _leaf_
when $\ell=0$: this requires that $X={\mathbf{a}}\in\mathbf{A}$ is an action
(and then ${\mathbf{d}}={\mathbf{c}}+{\mathbf{a}}$) or that $X=T\in V$ is a
non-terminal and $T$ is a rule in $R$ (and then ${\mathbf{d}}={\mathbf{c}}$).

As is standard, we use _positions_ to identify occurrences of subtrees inside
$t$. Formally, a position is a finite sequence of natural numbers, and the
positions of the subtrees of $t$, denoted ${\mathit{Pos}}(t)$ are given
inductively by

${\mathit{Pos}}(\sigma[t_{1},\ldots,t_{l}])\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\\{\varepsilon\\}\cup\\{i.q\leavevmode\nobreak\
|\leavevmode\nobreak\ 1\leq i\leq l\land q\in{\mathit{Pos}}(t_{i})\\}\>.$

For $p\in{\mathit{Pos}}(t)$, the subtree of $t$ at position $p$ is denoted
$t/p$.

######  Example 3.3.

Recall the 1-dimensional GVAS $G$ from Example 2.1. The grammar admits, among
others, a derivation $S\xLongrightarrow{*}w$ for
$w=\mathbf{-1}\,\mathbf{-1}\,\mathbf{1}\,\mathbf{0}\,\mathbf{0}$. Thus
$3\xrightarrow{w}2$ is a transition in $G$.

In Fig. 1 we display a derivation tree witnessing $S\xLongrightarrow{*}w$ and
a flow tree witnessing ${\mathbf{c}}\xrightarrow{w}{\mathbf{d}}$ for
${\mathbf{c}}=3$ and ${\mathbf{d}}=2$. ∎

$S$$\mathbf{-1}$$S$$T$$\mathbf{-1}$$S$$T$$\mathbf{0}$$\mathbf{0}$$\mathbf{1}$$3\xrightarrow{S}2$$3\xrightarrow{\mathbf{-1}}2$$2\xrightarrow{S}2$$2\xrightarrow{T}2$$2\xrightarrow{\mathbf{-1}}1$$1\xrightarrow{S}2$$2\xrightarrow{T}2$$2\xrightarrow{\mathbf{0}}2$$2\xrightarrow{\mathbf{0}}2$$1\xrightarrow{\mathbf{1}}2$
Figure 1. Continuing Example 2.1: $S\rightarrow\mathbf{1}\leavevmode\nobreak\
|\leavevmode\nobreak\ \mathbf{-1}\,S\,T$ and
$T\rightarrow\mathbf{0}\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathbf{-1}\,T\,\mathbf{2}$.
Left: Derivation tree witnessing $S\xLongrightarrow{*}w$, with
$w=\mathbf{-1}\mathbf{-1}\,\mathbf{1}\,\mathbf{0}\,\mathbf{0}$.
Right: Flow tree witnessing $3\xrightarrow{w}2$.

We now extend to flow trees of GVASes an ordering initially introduced by
Jančar for runs of VASes [15, Def. 6.4].

######  Definition 3.4 (Ordering GVAS transitions and flow trees).

For two transitions $\sigma={\mathbf{c}}\xrightarrow{X}{\mathbf{d}}$ and
$\theta={\mathbf{c}}^{\prime}\xrightarrow{X^{\prime}}{\mathbf{d}}^{\prime}$
with $X,X^{\prime}\in V\cup\mathbf{A}$, we let

$\sigma\leq\theta\>\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{\Leftrightarrow}}\>{\mathbf{c}}\leq{\mathbf{c}}^{\prime}\land{\mathbf{d}}\leq{\mathbf{d}}^{\prime}\land
X=X^{\prime}\>.$

The ordering $\leq_{G}$ between flow trees $s,t\in F(G)$ is defined by
induction on the structure of trees:
$s=\sigma[s_{1},\ldots,s_{k}]\leq_{G}t=\theta[t_{1},\ldots,t_{\ell}]$ if, and
only if, $\sigma\leq\theta$ and there exists a subtree $t^{\prime}$ of $t$ of
the form
$t^{\prime}=\theta^{\prime}[t^{\prime}_{1},\ldots,t^{\prime}_{\ell^{\prime}}]$
with $\sigma\leq\theta^{\prime}$, $\ell^{\prime}=k$ and
$s_{j}\leq_{G}t^{\prime}_{j}$ for every $1\leq j\leq k$.

This definition is well-founded and, since the subtree relation is transitive,
$\leq_{G}$ is clearly reflexive and transitive, i.e., is a quasi-ordering. In
the appendix, we prove the following key property:

######  Lemma 3.5 (See Appendix A).

$(F(G),\leq_{G})$ is a well-quasi-ordering.

In other words, any infinite sequence $s_{0},s_{1},s_{2},\ldots$ of flow trees
contains an infinite increasing subsequence
$s_{i_{0}}\leq_{G}s_{i_{1}}\leq_{G}s_{i_{2}}\leq_{G}\cdots$.

######  Example 3.6.

The flow trees shown in Fig. 2 illustrate the ordering $\leq_{G}$, on a
$1$-dimensional GVAS with non-terminals $S,T,U,V$ and the following rules:
$S\rightarrow\mathbf{3}\,T\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathbf{3}\,U$, $T\rightarrow\mathbf{-2}\leavevmode\nobreak\
|\leavevmode\nobreak\ V\,T$, $U\rightarrow T$ and $V\rightarrow\epsilon$. We
can see that $t_{1}\leq_{G}t_{2}$ from the following orderings on the subtrees
of $t_{1}$ and $t_{2}$: $t_{1}/1\leq_{G}t_{2}/1$, $t_{1}/2\leq_{G}t_{2}/2$ and
$t_{1}/21\leq_{G}t_{2}/221$. It can be verified that $t_{1}\not\leq_{G}t_{0}$.
However, $t_{1}\sqsubseteq t_{0}$, where $\sqsubseteq$ is the standard
homeomorphic embedding 111 defined by $s=\sigma[s_{1},\ldots,s_{k}]\sqsubseteq
t$ if, and only if, there exists a subtree
$t^{\prime}=\theta^{\prime}[t^{\prime}_{1},\ldots,t^{\prime}_{\ell^{\prime}}]$
of $t$ such that $\sigma\leq\theta^{\prime}$, $k\leq\ell^{\prime}$ and
$s_{1}\sqsubseteq t^{\prime}_{j_{1}},\ldots,s_{k}\sqsubseteq
t^{\prime}_{j_{k}}$ for some subsequence $1\leq
j_{1}<\cdots<j_{k}\leq\ell^{\prime}$.  of labeled trees. This can be seen by
the following orderings: $t_{1}/1\sqsubseteq t_{0}/1$, $t_{1}/2\sqsubseteq
t_{0}/21$ and $t_{1}/21\sqsubseteq t_{0}/211$.

$3\xrightarrow{S}4$$3\xrightarrow{\mathbf{3}}6$$6\xrightarrow{U}4$$6\xrightarrow{T}4$$6\xrightarrow{\mathbf{-2}}4$$t_{0}$$\not\geq_{G}$$2\xrightarrow{S}3$$2\xrightarrow{\mathbf{3}}5$$5\xrightarrow{T}3$$5\xrightarrow{\mathbf{-2}}3$$t_{1}$$\leq_{G}$$3\xrightarrow{S}4$$3\xrightarrow{\mathbf{3}}6$$6\xrightarrow{T}4$$6\xrightarrow{V}6$$6\xrightarrow{T}4$$6\xrightarrow{\mathbf{-2}}4$$t_{2}$

Figure 2. Illustration for Example 3.6:
$S\rightarrow\mathbf{3}\,T\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathbf{3}\,U$, $T\rightarrow\mathbf{-2}\leavevmode\nobreak\
|\leavevmode\nobreak\ V\,T$, $U\rightarrow T$ and $V\rightarrow\epsilon$.

When $\sigma\leq\theta$ for some
$\sigma={\mathbf{c}}\xrightarrow{X}{\mathbf{d}}$ and
$\theta={\mathbf{c}}^{\prime}\xrightarrow{X}{\mathbf{d}}^{\prime}$, we also
write $\sigma\leq^{\Delta}\theta$ with
$\Delta=({\mathbf{c}}^{\prime}-{\mathbf{c}},{\mathbf{d}}^{\prime}-{\mathbf{d}})$.
Similarly, we write $s\leq_{G}^{\Delta}t$ for two flow trees $s$ and $t$ when
$s\leq_{G}t$ and $\operatorname{root}(s)\leq^{\Delta}\operatorname{root}(t)$.

The pair $\Delta$ is called a _lifting_. Note that necessarily $\Delta$
belongs to $({\mathbb{N}}^{d})^{2}$ and that $\sigma\leq^{\Delta}\theta$ and
$\theta\leq^{\Delta^{\prime}}\rho$ entail
$\sigma\leq^{\Delta+\Delta^{\prime}}\rho$. We write $\rho=\sigma+\Delta$ when
$\sigma\leq^{\Delta}\rho$. Two liftings $\Delta=({\mathbf{a}},{\mathbf{b}})$
and $\Delta^{\prime}=({\mathbf{a}}^{\prime},{\mathbf{b}}^{\prime})$ can be
chained if ${\mathbf{b}}={\mathbf{a}}^{\prime}$. In this case we let
$\Delta\cdot\Delta^{\prime}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}({\mathbf{a}},{\mathbf{b}}^{\prime})$. Note this partial operation
is associative.

When $t/p=t^{\prime}\leq_{G}u$ we can replace $t^{\prime}$ by $u$ inside $t$
but this requires a bit of surgery to ensure the result is well-formed. First,
for a flow tree $t$ and a displacement ${\mathbf{a}}\in{\mathbb{N}}^{d}$, we
let $t+{\mathbf{a}}$ be the tree defined via

$\sigma[t_{1},\ldots,t_{\ell}]+{\mathbf{a}}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}(\sigma+({\mathbf{a}},{\mathbf{a}}))[t_{1}+{\mathbf{a}},\ldots,t_{\ell}+{\mathbf{a}}]\>.$

Obviously, $t+{\mathbf{a}}$ is a valid flow tree, with
$t\leq_{G}^{({\mathbf{a}},{\mathbf{a}})}(t+{\mathbf{a}})$. Now, when
$t/p=t^{\prime}\leq_{G}^{\Delta}u$ for $\Delta=({\mathbf{a}},{\mathbf{b}})$,
we define $t[u]_{p}$ by induction on $p$ in the following way:

$\displaystyle t[u]_{\varepsilon}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}u,$ $\displaystyle
t[u]_{i.q}$ $\displaystyle\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}(\sigma+\Delta)[t_{1}+{\mathbf{a}},\ldots,t_{i-1}+{\mathbf{a}},t_{i}[u]_{q},t_{i+1}+{\mathbf{b}},\ldots,t_{k}+{\mathbf{b}}].$

######  Claim 1.

If $t/p\leq^{\Delta}_{G}u$ then $t[u]_{p}$ is a valid flow tree satisfying
$t\leq_{G}^{\Delta}t[u]_{p}$.

######  Proof 3.7.

By induction on $p$. If $p=\varepsilon$ the claim holds trivially. Assume
$p=i.q$ with $1\leq i\leq k$ and let $u^{\prime}=t_{i}[u]q$. By induction
hypothesis, $t_{i}\leq_{G}^{\Delta}u^{\prime}$. This implies that $t[u]_{p}$
is a well-defined flow tree. Since furthermore
$t_{j}\leq_{G}t_{j}+{\mathbf{a}}$ when $1\leq j<i$, and symmetrically,
$t_{j}\leq_{G}t_{j}+{\mathbf{b}}$ when $i<j\leq k$, we see that
$t\leq_{G}t[u]_{p}$. Finally, we observe that
$\operatorname{root}(t)\leq^{\Delta}\operatorname{root}(t[u]_{p})$.

######  Lemma 3.8.

Let $t=\sigma[t_{1},\ldots,t_{k}]$ and assume
$t_{i}\leq_{G}^{\Delta_{i}}u_{i}$ for $i=1,\ldots,k$. If
$\Delta_{1}\cdot\Delta_{2}\cdots\Delta_{k}=\Delta$ is defined, then
$u=(\sigma+\Delta)[u_{1},\ldots,u_{k}]$ is a valid flow tree satisfying
$t\leq_{G}^{\Delta}u$.

######  Proof 3.9.

Since $\Delta=\Delta_{1}\cdots\Delta_{k}$ is defined, we can write
$\Delta_{i}=({\mathbf{a}}_{i-1},{\mathbf{a}}_{i})$ and
$\Delta=({\mathbf{a}}_{0},{\mathbf{a}}_{k})$. Assume
$\sigma={\mathbf{c}}_{0}\xrightarrow{X}{\mathbf{c}}_{k}$, with
$\operatorname{root}(t_{i})={\mathbf{c}}_{i-1}\xrightarrow{Y_{i}}{\mathbf{c}}_{i}$
for $i=1,\ldots,k$. Then
$\operatorname{root}(u_{i})=({\mathbf{c}}_{i-1}+{\mathbf{a}}_{i-1})\xrightarrow{Y_{i}}({\mathbf{c}}_{i}+{\mathbf{a}}_{i})$
and $u$ is a valid transition. That $t\leq_{G}u$ is immediate.

######  Theorem 3.10 (Amalgamation).

If $s\leq_{G}^{\Delta_{1}}t_{1}$ and $s\leq_{G}^{\Delta_{2}}t_{2}$ then there
exists $s^{\prime}$ s.t. $t_{1}\leq_{G}^{\Delta_{2}}s^{\prime}$ and
$t_{2}\leq_{G}^{\Delta_{1}}s^{\prime}$ (further entailing
$s\leq_{G}^{\Delta_{1}+\Delta_{2}}s^{\prime}$).

######  Proof 3.11.

By induction on $s$. Assume $s=\sigma[s_{1},\ldots,s_{k}]$. Since
$s\leq_{G}^{\Delta_{1}}t_{1}$, there is a subtree
$t_{1}/p=t^{1}=\rho_{1}[t_{1}^{1},\ldots,t_{k}^{1}]$ of $t_{1}$ such that
$\sigma\leq\rho_{1}$ and $s_{j}\leq_{G}t_{j}^{1}$ for all $j=1,\ldots,k$.
Assume that $\sigma\leq^{\Delta^{\prime}_{1}}\rho_{1}$ and that
$s_{j}\leq_{G}^{\Gamma_{j}}t_{j}^{1}$ for $j=1,\ldots,k$. Since $s$ and
$t^{1}$ are valid flow trees, we deduce that
$\Delta^{\prime}_{1}=\Gamma_{1}\cdots\Gamma_{k}$. Symmetrically, from
$s\leq_{G}^{\Delta_{2}}t_{2}$, we know that there is a subtree $t^{2}=t_{2}/q$
of $t_{2}$, of the form $t^{2}=\rho_{2}[t^{2}_{1},\ldots,t^{2}_{k}]$ with
$\sigma\leq^{\Delta^{\prime}_{2}}\rho_{2}$,
$s_{j}\leq_{G}^{\Gamma^{\prime}_{j}}t^{2}_{j}$ for $j=1,\ldots,k$, and
$\Delta^{\prime}_{2}=\Gamma^{\prime}_{1}\cdots\Gamma^{\prime}_{k}$.

By the induction hypothesis, there exists flow trees
$s^{\prime}_{1},\ldots,s^{\prime}_{k}$ such that
$t^{1}_{j}\leq_{G}^{\Gamma^{\prime}_{j}}s^{\prime}_{j}$ and
$t^{2}_{j}\leq_{G}^{\Gamma_{j}}s^{\prime}_{j}$ for all $j=1,\ldots,k$. We now
define

$\displaystyle u$ $\displaystyle\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}(\rho_{2}+\Delta^{\prime}_{1})[s^{\prime}_{1},\ldots,s^{\prime}_{k}],$
$\displaystyle u^{\prime}$ $\displaystyle\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}t_{2}[u]_{q},$ $\displaystyle s^{\prime}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}t_{1}[u^{\prime}]_{p},$

and claim that these are valid flow trees, $s^{\prime}$ being the flow tree
witnessing the Lemma.

To begin with, and since $\Delta^{\prime}_{1}=\Gamma_{1}\cdots\Gamma_{k}$, $u$
is well-formed by Lemma 3.8 and satisfies
$t^{2}\leq_{G}^{\Delta^{\prime}_{1}}u$. Since
$\rho_{2}+\Delta^{\prime}_{1}=\rho_{1}+\Delta^{\prime}_{2}$, and since
$\Delta^{\prime}_{2}=\Gamma^{\prime}_{1}\cdots\Gamma^{\prime}_{k}$, one also
has $t^{1}\leq_{G}^{\Delta^{\prime}_{2}}u$.

Then, and since $t^{2}\leq_{G}^{\Delta^{\prime}_{1}}u$, we have
$t_{2}=t_{2}[t^{2}]_{q}\leq_{G}^{\Delta^{\prime}_{1}}t_{2}[u]_{q}=u^{\prime}$
as in Claim 1. Thus the root of $u^{\prime}$ is
$\sigma+\Delta_{2}+\Delta^{\prime}_{1}=\rho_{1}+\Delta_{2}$. We deduce
$t^{1}\leq_{G}^{\Delta_{2}}u^{\prime}$, relying on $t^{1}\leq_{G}u$. As in
Claim 1, we obtain
$t_{1}\leq_{G}^{\Delta_{2}}t_{1}[u^{\prime}]_{p}=s^{\prime}$, proving the
first half of the Lemma.

On the other hand, from $t_{2}\leq_{G}u^{\prime}$ we get
$t_{2}\leq_{G}^{\Delta_{1}}s^{\prime}$ by just checking that the root of
$t_{2}$, i.e., $\sigma+\Delta_{2}$, is smaller than the root of $s^{\prime}$,
i.e., $\sigma+\Delta_{1}+\Delta_{2}$. This provides the other half and
completes the proof.

##  4\. GVAS-Definable Predicates

We explore in this section a natural notion of computable sets and relations
for the GVAS model, defined as projections of reachability sets. The context-
free grammar ingredient of GVASes is essential in the proof that the class of
computable sets is closed under intersection, while the Amalgamation Theorem
proves that computable sets are finite union of shifted periodic sets.

######  Definition 4.1.

A $n$-dimensional _GVAS-definable predicate_ is a subset $\mathbf{X}$ of
${\mathbb{N}}^{n}$ such that there exists a $d$-dimensional GVAS $G$ with
$d=n+\ell$ for some $\ell\in{\mathbb{N}}$ such that:

$\mathbf{X}=\\{{\mathbf{x}}\in{\mathbb{N}}^{n}\mid\exists{\mathbf{e}}\in{\mathbb{N}}^{\ell}:{\mathbf{0}}_{d}\xrightarrow{G}({\mathbf{x}},{\mathbf{e}})\\}\>.$
($\dagger$)

When ($\dagger$ ‣ 4.1) holds, we say that $G$ defines $\mathbf{X}$ using
$\ell$ auxiliary counters.

The class of GVAS-definable predicates is clearly closed under union,
cartesian product 222defined via
$\mathbf{X}\times\mathbf{Y}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\\{({\mathbf{x}},{\mathbf{y}})\mid{\mathbf{x}}\in\mathbf{X},\
{\mathbf{y}}\in\mathbf{Y}\\}$., and by projecting away some components. We
will provide additional closure properties in the remainder of this section.
GVAS-definable predicates form a rich class that strictly contains all
Presburger sets, i.e., subsets of ${\mathbb{N}}^{n}$ that are definable in
$\mathsf{FO}({\mathbb{N}};+)$, the first-order theory of natural numbers with
addition.

######  Remark 4.2.

Presburger sets are GVAS-definable predicates. The proof is obtained by
introducing the class of semilinear sets as follows. A _linear set_ of
${\mathbb{N}}^{n}$ is a set of the form
$\\{\mathbf{b}+\lambda_{1}\mathbf{p}_{1}+\cdots+\lambda_{k}\mathbf{p}_{k}\mid\lambda_{j}\in{\mathbb{N}}\\}$
where $\mathbf{b}$ and $\mathbf{p}_{1},\ldots,\mathbf{p}_{k}$ are vectors in
${\mathbb{N}}^{n}$. A _semilinear set_ of ${\mathbb{N}}^{n}$ is a finite union
of linear sets of ${\mathbb{N}}^{n}$. Let us recall that a subset of
${\mathbb{N}}^{n}$ is Presburger if, and only if, it is semilinear [9]. Since
the class of GVAS-definable predicates is closed under union, it is sufficient
to show that every linear set is GVAS-definable. We associate with a linear
set
$\mathbf{X}=\\{\mathbf{b}+\lambda_{1}\mathbf{p}_{1}+\cdots+\lambda_{k}\mathbf{p}_{k}\mid\lambda_{j}\in{\mathbb{N}}\\}$
the $n$-dimensional GVAS $G$ that generates the regular language
$\mathbf{b}\mathbf{p}_{1}^{*}\ldots\mathbf{p}_{k}^{*}$. Notice that $G$
defines the linear set $\mathbf{X}$ (using no auxiliary counter).

######  Example 4.3.

Let $G$ be the 2-dimensional GVAS given by the following four rules:

$\displaystyle S$
$\displaystyle\rightarrow\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
0\\\\[-5.0pt] \scriptstyle 1\end{array}\bigr{)}\leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
1\\\\[-5.0pt] \scriptstyle 0\end{array}\bigr{)}\,S\,T\>,$ $\displaystyle T$
$\displaystyle\rightarrow\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
0\\\\[-5.0pt] \scriptstyle 0\end{array}\bigr{)}\leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
0\\\\[-5.0pt]
\scriptstyle-1\end{array}\bigr{)}\,T\,\bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
0\\\\[-5.0pt] \scriptstyle 2\end{array}\bigr{)}\>.$

This GVAS is a variant of the 1-dimensional GVAS given in Example 2.1.
Analogously to that example, it can be shown that $G$ defines the set
$\mathbf{X}=\\{(x,y)\in{\mathbb{N}}^{2}\mid 1\leq y\leq 2^{x}\\}$, which is
not semilinear.

A geometrical decomposition of the GVAS-definable predicates can be shown
thanks to the _periodic sets_. A subset $\mathbf{P}$ of ${\mathbb{N}}^{d}$ is
said to be _periodic_ [27] if it contains the zero vector, and if
$\mathbf{x}+\mathbf{y}\in\mathbf{P}$ for every
$\mathbf{x},\mathbf{y}\in\mathbf{P}$. Note that a periodic $\mathbf{P}$ is not
necessarily finitely generated, hence not necessarily semilinear (see Example
4.6). The following Proposition extends the known decomposition of Presburger
sets into linear sets.

######  Proposition 4.4.

Every GVAS-definable predicate $\mathbf{X}\subseteq{\mathbb{N}}^{n}$ can be
decomposed into a finite union of sets of the form $\mathbf{b}+\mathbf{P}$
where $\mathbf{b}\in{\mathbb{N}}^{n}$ and $\mathbf{P}$ is a periodic subset of
${\mathbb{N}}^{n}$.

######  Proof 4.5.

There exists a $d$-dimensional GVAS $G$ that defines the set $\mathbf{X}$ with
$\ell$ auxiliary counters. Let us consider the set $T$ of flow trees $t$ such
that $\operatorname{root}({t})=(\mathbf{0}_{d},S,(\mathbf{x},\mathbf{e}))$ for
some $\mathbf{x}\in{\mathbb{N}}^{n}$, $\mathbf{e}\in{\mathbb{N}}^{\ell}$ and
where $S$ is the start symbol of $G$. For such a flow tree $t$ in $T$, we
denote by $\mu(t)$ the vector $\mathbf{x}$. With each $s\in T$ we associate
the set ${\uparrow}s=\\{t\in T\mid s\leq_{G}t\\}$. Since $(T,\leq_{G})$ is a
wqo, there exists a finite subset $T_{0}$ of $T$ such that

$T=\bigcup_{s\in T_{0}}{\uparrow}s\>.$

Given $s\in T$, we introduce the set $\mathbf{P}_{s}=\\{\mu(t)-\mu(s)\mid
t\in{\uparrow}s\\}$. Theorem 3.10 shows that $\mathbf{P}_{s}$ is a periodic
set. Now, just observe that the following equality holds:

$\mathbf{X}=\bigcup_{s\in T_{0}}\mu(s)+\mathbf{P}_{s}\>.$

The proposition is proved.

######  Example 4.6.

Continuing Example 4.3, the set $\mathbf{X}=\\{(x,y)\in{\mathbb{N}}^{2}\mid
1\leq y\leq 2^{x}\\}$ may be decomposed into $\mathbf{X}=(0,1)+\mathbf{P}$
where $\mathbf{P}$ is the periodic set
$\mathbf{P}=\\{(x,y)\in{\mathbb{N}}^{2}\mid 0\leq y<2^{x}\\}$.

The rest of this section discusses various closure properties of GVAS-
definable predicates. We start with boolean operations. As mentioned
previously, GVAS-definable predicates are closed under union. In order to
prove closure under intersection, we first provide a technical lemma that
shows how auxiliary counters of a GVAS can be assumed to be zero at the end of
the computation.

######  Lemma 4.7.

For every $d$-dimensional GVAS $G$ and for every subset $I$ of
$\\{1,\ldots,d\\}$, there is a $(d+1)$-dimensional GVAS $G_{I}$ such that for
every ${\mathbf{x}}\in{\mathbb{N}}^{d}$ and for every $c\in{\mathbb{N}}$, we
have:

${\mathbf{0}}_{d+1}\xrightarrow{G_{I}}({\mathbf{x}},c)\text{ iff
}{\mathbf{0}}_{d}\xrightarrow{G}{\mathbf{x}}\land c=0\land\bigwedge_{i\in
I}{\mathbf{x}}[i]=0\>.$ (5)

######  Proof 4.8.

The idea of the proof is to put the counters in $I$ “on a budget” (see, e.g.,
[33] for details on the budgeting construction) and to harness the expressive
power given by context-free grammars to non-deterministically initialize the
total budget, simulate $G$ with the given budget, and finally check that the
budget is fully restored at the end of the computation, which guarantees that
the counters in $I$ are zero.

Formally, let us introduce the function $\Delta_{I}$ that maps vectors
${\mathbf{x}}$ of ${\mathbb{Z}}^{d}$ to the number
$\Delta_{I}({\mathbf{x}})=\sum_{i\in I}\mathbf{x}[i]$. We also introduce the
mapping $\mu_{I}:{\mathbb{Z}}^{d}\rightarrow{\mathbb{Z}}^{d+1}$ defined by
$\mu_{I}({\mathbf{x}})=({\mathbf{x}},-\Delta_{I}({\mathbf{x}}))$. This mapping
is extended over words of actions as a word morphism, and over languages by
$\mu_{I}(L)=\\{\mu_{I}(w)\mid w\in L\\}$. Let us introduce the actions
$\mathbf{a}_{+}=({\mathbf{0}}_{d},1)$, and
$\mathbf{a}_{-}=({\mathbf{0}}_{d},-1)$. In linear time, from $G$ we can define
a $(d+1)$-dimensional GVAS $G_{I}$ that generates the following language:

$L_{G_{I}}=\bigcup_{k\in{\mathbb{N}}}\mathbf{a}_{+}^{k}\mu_{I}(L_{G})\mathbf{a}_{-}^{k}\>.$

Let us prove that this GVAS satisfies the lemma. We consider
${\mathbf{x}}\in{\mathbb{N}}^{d}$ and $c\in{\mathbb{N}}$.

Assume first that ${\mathbf{0}}_{d+1}\xrightarrow{G_{I}}({\mathbf{x}},c)$. In
that case, there exists $k\in{\mathbb{N}}$ and $w\in L_{G}$ such that
${\mathbf{0}}_{d+1}\xrightarrow{\mathbf{a}_{+}^{k}\mu_{I}(w)\mathbf{a}_{-}^{k}}({\mathbf{x}},c)$.
Observe that we have

${\mathbf{0}}_{d+1}\xrightarrow{\mathbf{a}_{+}^{k}}({\mathbf{0}}_{d},k)\xrightarrow{\mu_{I}(w)}({\mathbf{x}},c+k)\xrightarrow{\mathbf{a}_{-}^{k}}({\mathbf{x}},c)\>.$

Since $\mu_{I}(w)$ preserves the sum of the counters in $I$ and of the last
counter, it follows that
$\Delta_{I}({\mathbf{0}}_{d})+k=\Delta_{I}({\mathbf{x}})+c+k$. Thus
$c+\Delta_{I}({\mathbf{x}})=0$. It follows that $c=0$ and ${\mathbf{x}}[i]=0$
for every $i\in I$. Moreover, from
${\mathbf{0}}_{d}\xrightarrow{w}{\mathbf{x}}$ we derive
${\mathbf{0}}_{d}\xrightarrow{G}{\mathbf{x}}$.

Conversely, let us assume that ${\mathbf{0}}_{d}\xrightarrow{G}{\mathbf{x}}$,
$c=0$ and ${\mathbf{x}}[i]=0$ for every $i\in I$. There exists $w\in L_{G}$
such that ${\mathbf{0}}_{d}\xrightarrow{w}{\mathbf{x}}$. There exists
$k\in{\mathbb{N}}$ large enough such that
$({\mathbf{0}}_{d},k)\xrightarrow{\mu_{I}(w)}({\mathbf{x}},k-\Delta_{I}({\mathbf{x}}))=({\mathbf{x}},k)$.
It follows that
${\mathbf{0}}_{d+1}\xrightarrow{\mathbf{a}_{+}^{k}\mu_{I}(w)\mathbf{a}_{-}^{k}}({\mathbf{x}},0)=({\mathbf{x}},c)$.
Thus ${\mathbf{0}}_{d+1}\xrightarrow{G_{I}}({\mathbf{x}},c)$.

We are now ready to prove that GVAS-definable predicates are closed under
intersection.333By contrast, we believe that “VAS-definable” predicates are
not closed under intersection (unless one requires auxiliary counters to be
zero at the end of the computation). This conjecture remains to be proved.

######  Lemma 4.9.

The class of GVAS-definable predicates is closed under intersection.

######  Proof 4.10.

Let $\mathbf{X},\mathbf{Y}\subseteq{\mathbb{N}}^{n}$ be GVAS-definable. Since
the class of GVAS-definable predicates is closed under cartesian product, it
follows that $\mathbf{X}\times\mathbf{Y}$ is also GVAS-definable. Hence, there
exists a $d$-dimensional GVAS $H$ with $\ell$ auxiliary counters that defines
that set. Let us consider the mapping
$\mu:{\mathbb{Z}}^{d}\rightarrow{\mathbb{Z}}^{n}\times{\mathbb{Z}}^{d}$
defined by
$\mu(\mathbf{x},\mathbf{y},\mathbf{e})=(\mathbf{0}_{n},\mathbf{x},\mathbf{y},\mathbf{e})$
for every $\mathbf{x},\mathbf{y}\in{\mathbb{Z}}^{n}$ and
$\mathbf{e}\in{\mathbb{Z}}^{\ell}$. The mapping $\mu$ is extended as a word
morphism. We introduce the action $\mathbf{a}_{i}$ in ${\mathbb{Z}}^{n+d}$
defined as follows:

$\mathbf{a}_{i}=({\mathbf{i}}_{i,n},-{\mathbf{i}}_{i,n},-{\mathbf{i}}_{i,n},{\mathbf{0}}_{\ell})\>.$

Obviously, we can build a $(d+n)$-dimensional GVAS $G$ such that
$L_{G}=\mu(L_{H})\mathbf{a}_{1}^{*}\cdots\mathbf{a}_{d}^{*}$. Now, let
$I=\\{n+1,\ldots,3n\\}$ and let us apply Lemma 4.7 on $G$ and $I$. We obtain a
$(d+n+1)$-GVAS that defines $\mathbf{X}\cap\mathbf{Y}$.

######  Remark 4.11.

The class of GVAS-definable predicates is not closed under taking complements,
see Proposition 5.9.

We now investigate closure under sum 444defined via
$\mathbf{X}+\mathbf{Y}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\\{{\mathbf{x}}+{\mathbf{y}}\mid{\mathbf{x}}\in\mathbf{X},\
{\mathbf{y}}\in\mathbf{Y}\\}$. and under the associated Kleene star, which we
call periodic hull. Formally, the _periodic hull_ of a subset
$\mathbf{X}\subseteq{\mathbb{N}}^{n}$ is the set of finite sums of vectors in
$\mathbf{X}$. It turns out that the class of GVAS-definable predicates is
closed under sum and periodic hull. Closure under sum can be proved along the
same lines as closure under intersection (see Lemma 4.9). The detailed proof
is left as an exercise. Closure under periodic hull is more involved and
requires well-behaved GVASes.

In the definition of a GVAS-definable predicate $\mathbf{X}$ given in
($\dagger$ ‣ 4.1), the vector $\mathbf{e}$ can be seen as auxiliary counters
that can have arbitrary values at the end of the computation. We say that a
$d$-dimensional GVAS $G$ defining a predicate
$\mathbf{X}\subseteq{\mathbb{N}}^{n}$ using $\ell$ auxiliary counters is
_auxiliary-resetting_ if for every
$(\mathbf{x},\mathbf{e})\in{\mathbb{N}}^{n}\times{\mathbb{N}}^{\ell}$ such
that $\mathbf{0}_{d}\xrightarrow{G}({\mathbf{x}},{\mathbf{e}})$ we have
${\mathbf{e}}=\mathbf{0}_{\ell}$. We also say that $G$ is _output-increasing_
if every action of $G$ is an element of
${\mathbb{N}}^{n}\times{\mathbb{Z}}^{\ell}$ meaning that the output counters
${\mathbf{x}}$ cannot be decremented during a computation.

Let us first prove that GVAS-definable predicates can be defined by auxiliary-
resetting output-increasing GVAS. To do so, we introduce, for every
$k\in{\mathbb{N}}$, the unit vector $\mathbf{i}_{i,k}$ of ${\mathbb{N}}^{k}$
defined by $\mathbf{i}_{i,k}[j]=0$ if $j\not=i$ and $\mathbf{i}_{i,k}[i]=1$.

######  Lemma 4.12.

For every $d$-dimensional GVAS $G$ defining a set
$\mathbf{X}\subseteq{\mathbb{N}}^{n}$, there is a $(d+n+1)$-dimensional
auxiliary-resetting output-increasing GVAS defining $\mathbf{X}$.

######  Proof 4.13.

We introduce the mapping $\mu:{\mathbb{Z}}^{d}\rightarrow{\mathbb{Z}}^{n+d}$
defined by $\mu({\mathbf{a}})=(\mathbf{0}_{n},{\mathbf{a}})$. This mapping is
extended as a word morphism. Observe that there exists a $(d+n)$-dimensional
GVAS $G^{\prime}$ satisfying the following equality:

$L_{G^{\prime}}=\mu(L_{G})(\mathbf{i}_{1,n},-\mathbf{i}_{1,n},\mathbf{0}_{\ell})^{*}\cdots(\mathbf{i}_{n,n},-\mathbf{i}_{n,n},\mathbf{0}_{\ell})^{*}(\mathbf{0}_{n},\mathbf{0}_{n},-\mathbf{i}_{1,\ell})^{*}\cdots(\mathbf{0}_{n},\mathbf{0}_{n},-\mathbf{i}_{\ell,\ell})^{*}\>.$

This GVAS $G^{\prime}$ satisfies
$\mathbf{0}_{d+n}\xrightarrow{G^{\prime}}({\mathbf{x}},\mathbf{0}_{n},\mathbf{0}_{\ell})$
with ${\mathbf{x}}\in{\mathbb{N}}^{n}$ if, and only if, there exists
${\mathbf{e}}\in{\mathbb{N}}^{\ell}$ such that
$\mathbf{0}_{d}\xrightarrow{G}({\mathbf{x}},{\mathbf{e}})$. Moreover, actions
of that GVAS are in ${\mathbb{N}}^{n}\times{\mathbb{Z}}^{d}$. By applying the
construction given in the proof of Lemma 4.7 on $G^{\prime}$ with
$I=\\{n,\ldots,d+n\\}$ observe that we get a $(d+n+1)$-dimensional auxiliary-
resetting output-increasing GVAS defining $\mathbf{X}$.

######  Corollary 4.14.

The class of GVAS-definable predicates is closed under periodic hull.

######  Proof 4.15.

Assume that a predicate $\mathbf{X}\subseteq{\mathbb{N}}^{n}$ is GVAS-
definable. Lemma 4.12 shows that $\mathbf{X}$ is defined by a $d$-dimensional
auxiliary-resetting output-increasing GVAS $G$ using $\ell$ auxiliary
counters. As context-free languages are closed under Kleene star, there exists
a GVAS $G^{\prime}$ satisfying $L_{G^{\prime}}=L_{G}^{*}$. We show that
$G^{\prime}$ defines the periodic hull of $\mathbf{X}$. Let
$\mathbf{y}=\mathbf{x}_{1}+\cdots+\mathbf{x}_{k}$ with $k\in{\mathbb{N}}$ and
$\mathbf{x}_{1},\ldots,\mathbf{x}_{k}\in\mathbf{X}$ and let us prove that
$\mathbf{0}_{d}\xrightarrow{G^{\prime}}(\mathbf{y},\mathbf{0}_{\ell})$. We
introduce $\mathbf{y}_{j}=\mathbf{x}_{1}+\cdots+\mathbf{x}_{j}$ for every
$j\in\\{0,\ldots,k\\}$. Let $i\in\\{1,\ldots,k\\}$. Since
${\mathbf{x}}_{i}\in\mathbf{X}$ and $G$ is auxiliary-resetting, we get
$\mathbf{0}_{d}\xrightarrow{G}(\mathbf{x}_{i},\mathbf{0}_{\ell})$. By
monotony, we can add on both sides the vector
$(\mathbf{y}_{i-1},\mathbf{0}_{\ell})$ and derive
$(\mathbf{y}_{i-1},\mathbf{0}_{\ell})\xrightarrow{G}(\mathbf{y}_{i},\mathbf{0}_{\ell})$.
We get
$(\mathbf{y}_{0},\mathbf{0}_{\ell})\xrightarrow{G}(\mathbf{y}_{1},\mathbf{0}_{\ell})\cdots\xrightarrow{G}(\mathbf{y}_{k},\mathbf{0}_{\ell})$.
Since $\mathbf{y}_{0}=\mathbf{0}_{n}$ and $\mathbf{y}_{k}=\mathbf{y}$, we have
proved that
$\mathbf{0}_{d}\xrightarrow{G^{\prime}}(\mathbf{y},\mathbf{0}_{\ell})$.
Conversely, let $\mathbf{y}\in{\mathbb{N}}^{n}$ and
$\mathbf{e}\in{\mathbb{N}}^{\ell}$ such that
$\mathbf{0}_{d}\xrightarrow{G^{\prime}}(\mathbf{y},\mathbf{e})$ and let us
prove that $\mathbf{y}$ is in the periodic hull of $\mathbf{X}$. Since
$L_{G^{\prime}}=L_{G}^{*}$, we have
$(\mathbf{y}_{0},\mathbf{e}_{0})\xrightarrow{G}(\mathbf{y}_{1},\mathbf{e}_{1})\cdots\xrightarrow{G}(\mathbf{y}_{k},\mathbf{e}_{k})$
for some sequence
$(\mathbf{y}_{0},\mathbf{e}_{0}),\ldots,(\mathbf{y}_{k},\mathbf{e}_{k})$ such
that $(\mathbf{y}_{0},\mathbf{e}_{0})=\mathbf{0}_{d}$ and
$(\mathbf{y}_{k},\mathbf{e}_{k})=(\mathbf{y},\mathbf{e})$. Since $G$ is
output-increasing we deduce that $\mathbf{x}_{i}$, defined as
$\mathbf{x}_{i}=\mathbf{y}_{i}-\mathbf{y}_{i-1}$, is in ${\mathbb{N}}^{n}$ and
satisfies
$(\mathbf{0}_{n},\mathbf{e}_{i-1})\xrightarrow{G}(\mathbf{x}_{i},\mathbf{e}_{i})$.
As $G$ is auxiliary-resetting, by induction we deduce that
$\mathbf{e}_{i}=\mathbf{0}$ for every $i$. It follows that
$\mathbf{x}_{i}\in\mathbf{X}$. As
$\mathbf{y}=\mathbf{x}_{1}+\cdots+\mathbf{x}_{k}$, we conclude that
$\mathbf{y}$ is in the periodic hull of $\mathbf{X}$.

To conclude this section, we discuss closure under relational composition and
under the associated Kleene star (namely, the reflexive-transitive closure).
For the purpose of GVAS-definability, we view binary relations on
${\mathbb{N}}^{n}$ as subsets of ${\mathbb{N}}^{2n}$. The class of GVAS-
definable binary relations on ${\mathbb{N}}^{n}$ is closed under relational
composition. This claim follows from closure of GVAS-definable predicates
under cartesian product, intersection and projection. However, GVAS-definable
binary relations are not closed under reflexive-transitive closure in general,
as the following example shows.

######  Example 4.16.

Consider the binary relation $\mathbf{R}$ on ${\mathbb{N}}$ defined by
$\mathbf{R}=\\{(x,2x)\mid x\in{\mathbb{N}}\\}$. The binary relation
$\mathbf{R}$ is clearly GVAS-definable. However, its reflexive-transitive
closure $\mathbf{R}^{*}=\\{(x,2^{k}x)\mid x,k\in{\mathbb{N}}\\}$ is not GVAS-
definable. Indeed, if $\mathbf{R}^{*}$ were GVAS-definable then, by
Proposition 4.4, there would exist some $\mathbf{b}\in{\mathbb{N}}^{2}$, some
periodic $\mathbf{P}\subseteq{\mathbb{N}}^{2}$ and two distinct powers $2\leq
2^{k}<2^{\ell}$ such that

$(1,2^{k}),(1,2^{\ell})\in\mathbf{b}+\mathbf{P}\subseteq\mathbf{R}^{*}\>.$

We now use the assumption that $\mathbf{P}$ is periodic and derive a
contradiction. Let us write $\mathbf{b}=(b_{1},b_{2})$. Note that $b_{1}\leq
1$ and $b_{2}\leq 2^{k}$ since $(1,2^{k})\in\mathbf{b}+\mathbf{P}$. There are
three cases.

  * •

If $\mathbf{b}=\mathbf{0}$ then $(1,2^{k})$ and $(1,2^{\ell})$ are both in
$\mathbf{P}$, hence, $(2,2^{k}+2^{\ell})$ is also in $\mathbf{P}$ by
periodicity, and so $(2,2^{k}+2^{\ell})\in\mathbf{R}^{*}$. This is impossible
since $2^{k}+2^{\ell}$ is not a power of two (as $k\neq\ell$).

  * •

If $b_{1}>0$ then $b_{1}=1$, hence, $(1,2^{\ell})=(1,b_{2})+(0,p_{2})$ for
some $(0,p_{2})\in\mathbf{P}$. Note that $p_{2}>0$ since $b_{2}\leq
2^{k}<2^{\ell}$. Since $\mathbf{b}+\mathbf{P}\subseteq\mathbf{R}^{*}$, we get
by periodicity that $(1,b_{2}+np_{2})\in\mathbf{R}^{*}$ for every
$n\in{\mathbb{N}}$. This means that $b_{2}+np_{2}$ is a power of two for every
$n\in{\mathbb{N}}$, which is impossible as $p_{2}>0$.

  * •

If $b_{1}=0$ and $b_{2}>0$ then $(1,2^{\ell})=(0,b_{2})+(1,p_{2})$ for some
$(1,p_{2})\in\mathbf{P}$. Since
$\mathbf{b}+\mathbf{P}\subseteq\mathbf{R}^{*}$, we get by periodicity that
$(n,b_{2}+np_{2})\in\mathbf{R}^{*}$ for every $n\in{\mathbb{N}}$. Taking
$n=b_{2}+1$, we derive that $(b_{2}+1,b_{2}+(b_{2}+1)p_{2})\in\mathbf{R}^{*}$.
This is impossible since $b_{2}>0$ and $y$ is a multiple of $x$ for every
$(x,y)\in\mathbf{R}^{*}$.

##  5\. Weakly Computable Functions

There is a classical notion of number-theoretical functions weakly computable
by Petri nets [12]. In this section, we extend the idea to GVASes.

As we argued in the introduction, the notion of weakly computable functions
has recently gained new relevance with the development of well-structured
systems that go beyond Petri nets and VASSes in expressive power, while
sharing some of their characteristics.

The expected way for a GVAS to compute a numerical function
$f:{\mathbb{N}}\to{\mathbb{N}}$ is to start with some input number $n$ stored
in a designated input counter and, from that configuration, eventually reach a
configurations with $f(n)$ in a designated output counter. In order for that
GVAS to be correct (as a computer for $f$), it should be impossible that it
reaches a value differing from $f(n)$ in the output counter. In that case, we
say that the GVAS _strongly computes_ $f$. This notion of correctness is fine
with other models like Minsky machines but it is too strong for GVASes and
does not lead to an interesting family of computable functions. In fact, GVAS
are essentially nondeterministic devices, and the above notion of strongly
computing some function does not accommodate nondeterminism nicely.

With this in mind, and in the setting of VASes, Rabin defined a notion of
“weakly computing $f$” that combines the following two principles:

Completeness:

For any $n\in{\mathbb{N}}$, there is a computation with input $n$ and output
$f(n)$;

Safety:

Any computation from input $n$ to some output $r$ satisfies $r\leq f(n)$.

This leads to our definition of weak GVAS computers, where the input and
output counters are the first two components.

######  Definition 5.1 (Weak GVAS computers).

Let $f:{\mathbb{N}}\to{\mathbb{N}}$ be a total function. A _weak GVAS
computer_ (with $\ell$ auxiliary counters) for $f$ is a $d$-dimensional GVAS
$G$ with $d=2+\ell$ that satisfies the following two properties:

$\displaystyle\forall n:\exists n^{\prime},\mathbf{e}:\>$
$\displaystyle(n,0,{\mathbf{0}}_{\ell})\xrightarrow{G}(n^{\prime},f(n),\mathbf{e})\>,$
(CO) $\displaystyle\forall n,n^{\prime},r,\mathbf{e}:\>$
$\displaystyle(n,0,{\mathbf{0}}_{\ell})\xrightarrow{G}(n^{\prime},r,\mathbf{e})\text{
implies }r\leq f(n)\>.$ (SA)

We say that $f$ is _weakly computable_ , or WC, if there is a weak GVAS
computer for it.

For convenience, Definition 5.1 assumes that the input is given in the first
counter of $G$, and that the result is found in the second counter. Note that
$G$ may use its $\ell$ last counters for auxiliary calculations. We focus on
total functions over the natural numbers rather than total functions over the
vectors of natural numbers to simplify the presentation. However, results
given in this section can be easily extended to this more general setting.

######  Example 5.2 (A weak computer for exponentiation).

Example 2.1 shows that the function $f:{\mathbb{N}}\rightarrow{\mathbb{N}}$
defined by $f(n)=2^{n}$ is WC. ∎

Only monotonic functions can be weakly computed in the above sense. This is an
immediate consequence of the monotonicity of GVASes (see (3)). Recall that a
total function $f:{\mathbb{N}}\to{\mathbb{N}}$ is _non-decreasing_ if $n\leq
m$ implies $f(n)\leq f(m)$.

######  Proposition 5.3 (Monotonicity of WC functions).

If $f$ is WC then $f$ is non-decreasing.

######  Proof 5.4.

Assume that $n\leq m$ and pick any weak GVAS computer $G$ for $f$. By (CO), we
have $(n,0,{\mathbf{0}}_{\ell})\xrightarrow{G}(n^{\prime},f(n),\mathbf{e})$
for some $n^{\prime}\in{\mathbb{N}}$ and $\mathbf{e}\in{\mathbb{N}}^{\ell}$.
By monotonicity, it follows that
$(n+(m-n),0,{\mathbf{0}}_{\ell})\xrightarrow{G}(n^{\prime}+(m-n),f(n),\mathbf{e})$.
We get $f(n)\leq f(m)$ by (SA).

We may now relate WC computability with GVAS-definability.

######  Lemma 5.5.

A total function $f:{\mathbb{N}}\to{\mathbb{N}}$ is WC if, and only if, $f$ is
non-decreasing and the following set is GVAS-definable.

$\\{(x,y)\in{\mathbb{N}}\times{\mathbb{N}}\mid y\leq f(x)\\}\>.$

######  Proof 5.6.

Assume first that $f$ is WC. There exists a weak GVAS computer (with $\ell$
auxiliary counters) for $f$ given as a $d$-dimensional GVAS $G$ with
$d=2+\ell$ that satisfies (CO) and (SA). Let us consider the mapping
$\mu:{\mathbb{Z}}^{d}\rightarrow{\mathbb{Z}}^{d+1}$ defined by
$\mu(a,b,\mathbf{e})=(0,b,a,\mathbf{e})$ for every $a,b\in{\mathbb{Z}}$, and
$\mathbf{e}\in{\mathbb{Z}}^{\ell}$. The mapping $\mu$ is extended as a word
morphism. Let us show that a GVAS $G^{\prime}$ such that
$L_{G^{\prime}}=(1,0,1,\mathbf{0}_{\ell})^{*}\mu(L_{G})(0,-1,0,\mathbf{0}_{\ell})^{*}$
is defining the set $\\{(x,y)\in{\mathbb{N}}\times{\mathbb{N}}\mid y\leq
f(x)\\}$. Let $(x,y)$ in that set. From (CO), there exists a word $\sigma\in
L_{G}$, $x^{\prime}\in{\mathbb{N}}$ and $\mathbf{e}\in{\mathbb{N}}^{\ell}$
such that
$(x,0,\mathbf{0}_{\ell})\xrightarrow{\sigma}(x^{\prime},f(x),\mathbf{e})$. The
word
$\sigma^{\prime}=(1,0,1,\mathbf{0}_{\ell})^{x}\mu(\sigma)(0,-1,0,\mathbf{0})^{f(x)-y}$
shows that
$(0,0,0,\mathbf{0}_{\ell})\xrightarrow{\sigma^{\prime}}(x,y,x^{\prime},\mathbf{e})$.
As $\sigma^{\prime}\in L_{G^{\prime}}$, we get
$(0,0,0,\mathbf{0}_{\ell})\xrightarrow{G^{\prime}}(x,y,x^{\prime},\mathbf{e})$.
Conversely, assume that
$(0,0,0,\mathbf{0}_{\ell})\xrightarrow{\sigma^{\prime}}(x,y,x^{\prime},\mathbf{e})$
for some $x,y,x^{\prime}\in{\mathbb{N}}$, $\mathbf{e}\in{\mathbb{N}}^{\ell}$
and $\sigma^{\prime}\in L_{G^{\prime}}$, and let us prove that $y\leq f(x)$.
By definition of $G^{\prime}$, there exists $n,m\in{\mathbb{N}}$ and a word
$\sigma\in L_{G}$ such that
$\sigma^{\prime}=(1,0,1,\mathbf{0}_{\ell})^{n}\mu(\sigma)(0,-1,0,\mathbf{0}_{\ell})^{m}$.
It follows that
$(n,0,n,\mathbf{0}_{\ell})\xrightarrow{\mu(\sigma)}(x,y+m,x^{\prime},\mathbf{e})$.
Since actions occurring in $\mu(\sigma)$ cannot modify the first counter, we
get $n=x$. Moreover,
$(x,0,\mathbf{0}_{\ell})\xrightarrow{\sigma}(x^{\prime},y+m,\mathbf{e})$. From
(SA), we derive $y+m\leq f(x)$. Hence $y\leq f(x)$. We have proved that
$\\{(x,y)\in{\mathbb{N}}\times{\mathbb{N}}\mid y\leq f(x)\\}$ is GVAS-
definable.

Conversely, let us assume that $f$ is non-decreasing and that
$\\{(x,y)\in{\mathbb{N}}\times{\mathbb{N}}\mid y\leq f(x)\\}$ is GVAS-
definable. There exists a $d$-dimensional GVAS $G$ with $d=2+\ell$ such that:

$\\{(x,y)\mid y\leq
f(x)\\}=\\{(x,y)\mid\exists\mathbf{e}\in{\mathbb{N}}^{\ell}:(0,0,\mathbf{0}_{\ell})\xrightarrow{G}(x,y,\mathbf{e})\\}\>.$

Let us consider the mapping
$\mu:{\mathbb{Z}}^{d}\rightarrow{\mathbb{Z}}^{d+1}$ defined by
$\mu(a,b,\mathbf{e})=(-a,b,a,\mathbf{e})$ for every $a,b\in{\mathbb{Z}}$, and
$\mathbf{e}\in{\mathbb{Z}}^{\ell}$. The mapping $\mu$ is extended as a word
morphism. Let us show that a GVAS $G^{\prime}$ such that
$L_{G^{\prime}}=\bigcup_{k\in{\mathbb{N}}}(1,0,0,\mathbf{0}_{\ell})^{k}\mu(L_{G})(-1,0,0,\mathbf{0}_{\ell})^{k}$
is a weak GVAS computer for $f$. Let us first consider $x\in{\mathbb{N}}$. By
definition of $G$, there exists a word $\sigma\in L_{G}$ and
$\mathbf{e}\in{\mathbb{N}}^{\ell}$ such that
$(0,0,\mathbf{0}_{\ell})\xrightarrow{\sigma}(x,f(x),\mathbf{e})$. Notice that
for $k$ large enough, we have
$(k+x,0,0,\mathbf{0}_{\ell})\xrightarrow{\mu(\sigma)}(k,f(x),x,\mathbf{e})$.
The word
$\sigma^{\prime}=(1,0,0,\mathbf{0}_{\ell})^{k}\mu(\sigma)(-1,0,0,\mathbf{0}_{\ell})^{k}$
is such that
$(x,0,0,\mathbf{0}_{\ell})\xrightarrow{\sigma^{\prime}}(0,f(x),x,\mathbf{e})$.
Hence (CO) is satisfied by $G^{\prime}$. Finally, let us assume that
$(x,0,0,\mathbf{0}_{\ell})\xrightarrow{\sigma^{\prime}}(z,y,x^{\prime},\mathbf{e})$
for a word $\sigma^{\prime}\in L_{G^{\prime}}$ and
$x^{\prime},y,z\in{\mathbb{N}}$ and $\mathbf{e}\in{\mathbb{N}}^{\ell}$. There
exists $k\in{\mathbb{N}}$ and $\sigma\in L_{G}$ such that
$\sigma^{\prime}=(1,0,0,\mathbf{0}_{\ell})^{k}\mu(\sigma)(-1,0,0,\mathbf{0}_{\ell})^{k}$.
It follows that
$(x+k,0,0,\mathbf{0}_{\ell})\xrightarrow{\mu(\sigma)}(z+k,y,x^{\prime},\mathbf{e})$.
By definition of $\mu$, since the effect of the sum of the first and third
counters is zero, we get $x+k+0=z+k+x^{\prime}$. Hence $x^{\prime}\leq x$ and
in particular $f(x^{\prime})\leq f(x)$. Moreover, we have
$(0,0,\mathbf{0}_{\ell})\xrightarrow{\sigma}(x^{\prime},y,\mathbf{e})$. By
definition of $G$, we get $y\leq f(x^{\prime})$. We have proved that $y\leq
f(x)$. Hence (SA) is satisfied by $G^{\prime}$. We have proved that
$G^{\prime}$ is a weak GVAS computer for $f$

By combining Lemma 5.5 and the decomposition of GVAS-definable sets given by
Proposition 4.4, we obtain two interesting, albeit negative, results on WC
functions and GVAS-definable sets.

######  Proposition 5.7.

Let $f$ be an unbounded WC function. Then there exists a rational number $c>0$
and some $z\in{\mathbb{Z}}$ such that $f(n)\geq cn+z$ for every
$n\in{\mathbb{N}}$.

######  Proof 5.8.

Lemma 5.5 shows that the set $\mathbf{X}$ defined as $\\{(n,m)\mid m\leq
f(n)\\}$ is GVAS-definable. Proposition 4.4 shows that $\mathbf{X}$ can be
decomposed into a finite union of sets of the form $(a,b)+\mathbf{P}$ where
$(a,b)\in{\mathbb{N}}^{2}$ and $\mathbf{P}$ is a periodic subset of
${\mathbb{N}}^{2}$. Since $f$ is unbounded, there exists $(p,q)\in\mathbf{P}$
such that $q>0$. It follows $(a,b)+k(p,q)\in\mathbf{X}$ for every
$k\in{\mathbb{N}}$. In particular $f(a+kp)\geq b+kq$ for every
$k\in{\mathbb{N}}$. As $f(a)\in{\mathbb{N}}$ and $q>0$, we deduce that $p>0$.
Let us consider $n\in{\mathbb{N}}$ such that $n\geq a$ and observe that there
exists $k\in{\mathbb{N}}$ such that:

$k\leq\frac{n-a}{p}<k+1\>.$

It follows that $a+kp\leq n$ and in particular $f(a+kp)\leq f(n)$. Hence
$f(n)\geq b+kq\geq b+(\frac{n-a}{p}-1)q$. Introducing $c=\frac{q}{p}$, we
deduce that $f(n)-cn\geq b-c(a+p)$ for every $n\geq a$. We have proved the
lemma with any $z\in{\mathbb{Z}}$ satisfying $z\leq f(n)-cn$ for every $0\leq
n<a$ and $z\leq b-c(a+p)$.

######  Proposition 5.9.

The complement of a GVAS-definable set is not always GVAS-definable.

######  Proof 5.10.

Recall from Example 5.2 that the function $f:{\mathbb{N}}\to{\mathbb{N}}$
defined by $f(n)=2^{n}$ is WC. We derive from Lemma 5.5 that
$\mathbf{X}\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\\{(n,m)\mid m\leq
2^{n}\\}$ is GVAS-definable. Assume, by way of contradiction, that the
complement $\mathbf{Y}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\\{(n,m)\mid 2^{n}<m\\}$ is GVAS-definable. From a GVAS defining
$\mathbf{Y}$, we easily derive a GVAS defining
$\mathbf{Z}\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\\{(n,m)\mid
2^{m}\leq n+1\\}$, by swapping the first two counters and then decrementing
the first counter by two at the end. It follows from Lemma 5.5 that the
mapping $g:{\mathbb{N}}\to{\mathbb{N}}$ defined by
$g(n)=\lfloor\log_{2}(n+1)\rfloor$ is WC, contradicting Proposition 5.7 since
$g$ is unbounded and sublinear. Hence $\mathbf{Y}$, i.e.,
${\mathbb{N}}^{2}\setminus\mathbf{X}$, cannot be GVAS-definable.

##  6\. Hyper-Ackermannian GVAS

In this section we construct GVASes that weakly compute functions from the
Fast Growing Hierarchy. Our main result is the following.

######  Theorem 6.1.

The Fast Growing functions $(F_{\alpha})_{\alpha<\omega^{\omega}}$ are weakly
computable (by GVASes).

Note that these are exactly the multiply-recursive functions $F_{\alpha}$.
They include functions that are not primitive-recursive (the $F_{\alpha}$ for
$\omega\leq\alpha<\omega^{\omega}$) and that are thus not weakly computable by
VASSes (see [17, section 2]). We do not know whether $F_{\omega^{\omega}}$ is
weakly computable by a GVAS, or whether there exist WC functions that are not
multiply-recursive.

The rest of this section proves Theorem 6.1. The detailed proof illustrates
how the GVAS model makes it manageable to define complex constructions
precisely, and to formally prove their correctness. By contrast, observe how
in less abstract models e.g., the Timed-Arc Petri Nets of [14], only schematic
constructions are given for weakly computing functions, and only an outline
for a correctness proof can be provided.

We follow notation and definitions from [31] and consider functions
$F_{\alpha}:{\mathbb{N}}\to{\mathbb{N}}$ indexed by an ordinal
$\alpha<\epsilon_{0}$ (though we shall only build GVASes for functions with
$\alpha<\omega^{\omega}$). Any such ordinal can be written in Cantor normal
form (CNF) $\alpha=\omega^{\alpha_{1}}+\cdots+\omega^{\alpha_{m}}$ with
$\alpha>\alpha_{1}\geq\cdots\geq\alpha_{m}$. When $m=0$, $\alpha$ is $0$. When
$\alpha_{m}=0$, $\alpha$ is a successor of the form $\beta+\omega^{0}$, i.e.,
$\beta+1$, and when $\alpha_{m}>0$, $\alpha$ is a limit ordinal. When
$\alpha\neq 0$, we often decompose $\alpha$ under the form
$\alpha=\gamma+\omega^{\alpha_{m}}$ so that the smallest summand in $\alpha$’s
CNF is exposed. CNFs are often written more concisely using coefficients, as
in $\alpha=\omega^{\alpha_{1}}\cdot c_{1}+\cdots+\omega^{\alpha_{m}}\cdot
c_{m}$, with now $\alpha>\alpha_{1}>\cdots>\alpha_{m}$ and
$\omega>c_{1},\ldots,c_{m}>0$.

With each limit ordinal $\lambda<\epsilon_{0}$, one associates a fundamental
sequence $(\lambda(n))_{n<\omega}$ such that $\lambda=\sup_{n}\lambda(n)$.
These are defined inductively as follows.

$\displaystyle(\gamma+\omega^{\beta+1})(n)$
$\displaystyle=\gamma+\omega^{\beta}\cdot(n+1)\>,$ (L1)
$\displaystyle(\gamma+\omega^{\lambda})(n)$
$\displaystyle=\gamma+\omega^{\lambda(n)}\>.$ (LL)

For instance, Eq. (L1) gives $\omega(n)$, i.e.,
$\omega^{1}(n)=\omega^{0}\cdot(n+1)=n+1$ and $(\omega^{3}\cdot
6+\omega^{2}\cdot 3)(n)=\omega^{3}\cdot 6+\omega^{2}\cdot 2+\omega\cdot(n+1)$.
Similarly, Eq. (LL) gives
$\omega^{\omega}(n)=\omega^{\omega(n)}=\omega^{n+1}$. Note that the
fundamental sequences satisfy
$\lambda(0)<\cdots<\lambda(n)<\lambda(n+1)<\cdots<\lambda$ for any limit
ordinal $\lambda$ and index $n$.

We may now define our fast growing functions
$F_{\alpha}:{\mathbb{N}}\to{\mathbb{N}}$ for $\alpha<\epsilon_{0}$ by
induction on the $\alpha$ index.

$\displaystyle F_{0}(x)$ $\displaystyle=x+1\>,$ (F0) $\displaystyle
F_{\alpha+1}(x)$
$\displaystyle=F_{\alpha}^{\omega(x)}(x)=\overbrace{F_{\alpha}(\cdots(F_{\alpha}}^{x+1\text{
times}}(x))\cdots)\>,$ (F1) $\displaystyle F_{\lambda}(x)$
$\displaystyle=F_{\lambda(x)}(x)\>.$ (FL)

As shown —e.g., in [31]— these functions are _strictly expansive_ and
_monotonic_ , i.e., for all ordinals $\alpha<\epsilon_{0}$ and all
$n,n^{\prime}\in{\mathbb{N}}$:

$\displaystyle n<F_{\alpha}(n)\>,$ (FX) $\displaystyle n\leq
n^{\prime}\implies F_{\alpha}(n)\leq F_{\alpha}(n^{\prime})\>.$ (FM)

Given two ordinals in Cantor normal form
$\alpha=\omega^{\beta_{1}}+\cdots+\omega^{\beta_{m}}$ and
$\alpha^{\prime}=\omega^{\beta^{\prime}_{1}}+\cdots+\omega^{\beta^{\prime}_{n}}$,
we denote by $\alpha\oplus\alpha^{\prime}$ their _natural sum_
$\sum_{k=1}^{m+n}\omega^{\gamma_{k}}$, where
$\gamma_{1}\geq\ldots\geq\gamma_{m+n}$ is a reordering of
$\beta_{1},\ldots,\beta_{m},\beta^{\prime}_{1},\ldots,\beta^{\prime}_{n}$. The
$F_{\alpha}$ functions are not monotonic in the ordinal index, i.e.,
$\alpha\leq\alpha^{\prime}$ does not always entail $F_{\alpha}(n)\leq
F_{\alpha^{\prime}}(n)$, see [31, section A.2]. However, our construction
relies on similar monotonicity properties, albeit for special cases of
$\alpha$ and $\alpha^{\prime}$, that we now state.

######  Lemma 6.2.

For any ordinals $\alpha,\alpha^{\prime}<\epsilon_{0}$ and any
$n\in{\mathbb{N}}$, $F_{\alpha}(n)\leq F_{\alpha\oplus\alpha^{\prime}}(n)$.

######  Lemma 6.3.

For any ordinal $\alpha<\epsilon_{0}$ and limit ordinal
$\lambda<\omega^{\omega}$, for any $m,n\in{\mathbb{N}}$, if $m\leq n$ then
$F_{\alpha\oplus\lambda(m)}(n)\leq F_{\alpha\oplus\lambda}(n)$.

For these two results, detailed proofs are given in the appendix. We note that
Lemma 6.2 is a rewording of Lemma 2.2a from [4], however that paper uses a
different definition for the fundamental sequences
$(\lambda(n))_{n\in{\mathbb{N}}}$, resulting in slightly different
$F_{\alpha}$ functions, hence the need of an independent proof. Similarly,
Lemma 6.3 is a generalization of Lemma VI.5 from [22], using different
notation and allowing a simpler proof.

We now define weak GVAS computers for the $F_{\alpha}$ functions such that
$\alpha<\omega^{\omega}$. Our construction is in two steps: we first pick an
arbitrary exponent $d\in{\mathbb{N}}$ and define $G_{d}$, a GVAS with a
structure suitable for correctness proofs. We then obtain a weak GVAS computer
for $F_{\alpha}$ by slightly modifying $G_{d}$, provided $\alpha<\omega^{d}$.
The whole construction is an adaptation into the GVAS framework of the
pushdown VAS from [22].

The dimension of $G_{d}$ is $d+2$ and we use $d+2$ counters named
$r,\overline{r},\kappa_{0},\ldots,\kappa_{d-1}$, in this order. The set of
actions $\mathbf{A}\subseteq{\mathbb{Z}}^{d+2}$ consists of all vectors
$\mathbf{d}_{x}$ and ${\mathbf{i}}_{x}$ where $x$ is one of the $d+2$
counters: formally $\mathbf{d}_{x}$ is the vector that decrements $x$, while
${\mathbf{i}}_{x}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}-\mathbf{d}_{x}$ increments it. For instance,
$\mathbf{d}_{\kappa_{0}}=(0,0,-1,{\mathbf{0}}_{d-1})$ and
${\mathbf{i}}_{r}=(1,0,{\mathbf{0}}_{d})$. The set of non-terminals of $G_{d}$
is
$V=\\{{\mathtt{F}},{\mathtt{Rec}},{\mathtt{Pop}},{\mathtt{Lim}}_{1},\ldots,{\mathtt{Lim}}_{d-1}\\}$.
The start symbol is ${\mathtt{F}}$. The other non-terminals are used for
intermediate steps (see the rules below).

The first two counters, $r$ and $\overline{r}$, are used to manipulate the
arguments of the functions being computed. The other $d$ counters are used as
a data structure representing an ordinal $\alpha<\omega^{d}$. Formally, with
any $d$-tuple $\langle{c_{0},\ldots,c_{d-1}}\rangle$ of natural numbers, we
associate the ordinal $\alpha=\omega^{d-1}\cdot c_{d-1}+\cdots+\omega^{0}\cdot
c_{0}$. We will follow the convention of writing the contents of the counters
of our GVAS in the form $\langle{n,m,\alpha}\rangle$, where $n$ and $m$ are
the value of $r$ and $\overline{r}$, respectively, and where $\alpha$ is the
ordinal associated with the values in $\kappa_{0},\ldots,\kappa_{d-1}$.

The rules of $G_{d}$ are given below. The rules involving the
${\mathtt{Lim}}_{i}$ non-terminals are present for every
$i\in\\{1,\ldots,d-1\\}$.

$\displaystyle{\mathtt{F}}$ $\displaystyle\rightarrow{\mathbf{i}}_{r}\>,$ (R1)
$\displaystyle{\mathtt{F}}$ $\displaystyle\rightarrow\mathbf{d}_{\kappa_{0}}\
{\mathtt{Rec}}\ {\mathtt{F}}\ {\mathbf{i}}_{\kappa_{0}}\>,$ (R2)
$\displaystyle{\mathtt{F}}$
$\displaystyle\rightarrow\mathbf{d}_{\kappa_{i}}{\mathbf{i}}_{\kappa_{i-1}}\
{\mathtt{Lim}}_{i}\ \mathbf{d}_{\kappa_{i-1}}{\mathbf{i}}_{\kappa_{i}}\>,$
(R3$i$) $\displaystyle{\mathtt{Rec}}$
$\displaystyle\rightarrow{\mathtt{Pop}}\>,$ (R4) $\displaystyle{\mathtt{Rec}}$
$\displaystyle\rightarrow\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}\
{\mathtt{Rec}}\ {\mathtt{F}}\>,$ (R5) $\displaystyle{\mathtt{Pop}}$
$\displaystyle\rightarrow\varepsilon\>,$ (R6) $\displaystyle{\mathtt{Pop}}$
$\displaystyle\rightarrow{\mathbf{i}}_{r}\mathbf{d}_{\overline{r}}\
{\mathtt{Pop}}\>,$ (R7) $\displaystyle{\mathtt{Lim}}_{i}$
$\displaystyle\rightarrow{\mathtt{Pop}}\ {\mathtt{F}}\>,$ (R8$i$)
$\displaystyle{\mathtt{Lim}}_{i}$
$\displaystyle\rightarrow\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}{\mathbf{i}}_{\kappa_{i-1}}\
{\mathtt{Lim}}_{i}\ \mathbf{d}_{\kappa_{i-1}}\>.$ (R9$i$)

Our first goal is to prove that $G_{d}$ has computations of the form
$\langle{n,0,\alpha}\rangle\xrightarrow{{\mathtt{F}}}\langle{F_{\alpha}(n),0,\alpha}\rangle$,
for any $n\in{\mathbb{N}}$ and $\alpha<\omega^{d}$. We start with a lemma
exposing some specific sentential forms that can be derived from
${\mathtt{F}}$ and ${\mathtt{Pop}}$. As will be clear from the proof of Lemma
6.6, these derivations (namely (D0), (D1) and (DL)) correspond to our
inductive definition of the fast growing functions $F_{\alpha}$ (namely (F0),
(F1) and (FL)).

######  Lemma 6.4.

For every $n\in{\mathbb{N}}$ and $0<i<d$, $G_{d}$ admits the following
derivations:

$\displaystyle{\mathtt{F}}$
$\displaystyle\xLongrightarrow{*}{\mathbf{i}}_{r}\>,$ (D0)
$\displaystyle{\mathtt{F}}$
$\displaystyle\xLongrightarrow{*}\mathbf{d}_{\kappa_{0}}\
(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}})^{n}\ {\mathtt{Pop}}\
({\mathtt{F}})^{n+1}\ {\mathbf{i}}_{\kappa_{0}}\>,$ (D1)
$\displaystyle{\mathtt{F}}$
$\displaystyle\xLongrightarrow{*}\mathbf{d}_{\kappa_{i}}{\mathbf{i}}_{\kappa_{i-1}}\
(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}{\mathbf{i}}_{\kappa_{i-1}})^{n}\
{\mathtt{Pop}}\ {\mathtt{F}}\ (\mathbf{d}_{\kappa_{i-1}})^{n+1}\
{\mathbf{i}}_{\kappa_{i}}\>,$ (DL) $\displaystyle{\mathtt{Pop}}$
$\displaystyle\xLongrightarrow{*}({\mathbf{i}}_{r}\mathbf{d}_{\overline{r}})^{n}\>.$
(DP)

######  Proof 6.5.

Derivation (D0) is an immediate consequence of rule (R1) and derivation (DP)
similarly follows from rules (R6) and (R7). To prove derivation (D1), we use

$\displaystyle{\mathtt{F}}\xLongrightarrow{\eqref{ruleF+1}}\mathbf{d}_{\kappa_{0}}\
{\mathtt{Rec}}\ {\mathtt{F}}\
{\mathbf{i}}_{\kappa_{0}}\xLongrightarrow{\eqref{ruleRec1}}\cdots$
$\displaystyle\xLongrightarrow{\eqref{ruleRec1}}\mathbf{d}_{\kappa_{0}}\
(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}})^{n}\ {\mathtt{Rec}}\
({\mathtt{F}})^{n}\ {\mathtt{F}}\ {\mathbf{i}}_{\kappa_{0}}$
$\displaystyle\xLongrightarrow{\eqref{ruleRec0}}\mathbf{d}_{\kappa_{0}}\
(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}})^{n}\ {\mathtt{Pop}}\
({\mathtt{F}})^{n+1}\ {\mathbf{i}}_{\kappa_{0}}\>.$

Finally, derivation (DL) is obtained with

$\displaystyle{\mathtt{F}}$
$\displaystyle\xLongrightarrow{\eqref{ruleFlim}}\mathbf{d}_{\kappa_{i}}{\mathbf{i}}_{\kappa_{i-1}}\
{\mathtt{Lim}}_{i}\ \mathbf{d}_{\kappa_{i-1}}{\mathbf{i}}_{\kappa_{i}}$
$\displaystyle\xLongrightarrow{\eqref{ruleLim1}}\cdots\xLongrightarrow{\eqref{ruleLim1}}\mathbf{d}_{\kappa_{i}}{\mathbf{i}}_{\kappa_{i-1}}\
(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}{\mathbf{i}}_{\kappa_{i-1}})^{n}\
{\mathtt{Lim}}_{i}\ (\mathbf{d}_{\kappa_{i-1}})^{n}\
\mathbf{d}_{\kappa_{i-1}}{\mathbf{i}}_{\kappa_{i}}$
$\displaystyle\xLongrightarrow{\eqref{ruleLim0}}\mathbf{d}_{\kappa_{i}}{\mathbf{i}}_{\kappa_{i-1}}\
(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}{\mathbf{i}}_{\kappa_{i-1}})^{n}\
{\mathtt{Pop}}\ {\mathtt{F}}\ (\mathbf{d}_{\kappa_{i-1}})^{n+1}\
{\mathbf{i}}_{\kappa_{i}}\>.$

######  Lemma 6.6.

For every ordinal $\alpha<\omega^{d}$ and every $n\in{\mathbb{N}}$, $G_{d}$
has a computation
$\langle{n,0,\alpha}\rangle\xrightarrow{{\mathtt{F}}}\langle{F_{\alpha}(n),0,\alpha}\rangle$.

######  Proof 6.7.

We first observe that $G_{d}$ has a computation
$\langle{0,n,\alpha}\rangle\xrightarrow{{\mathtt{Pop}}}\langle{n,0,\alpha}\rangle$
for every ordinal $\alpha<\omega^{d}$ and every $n\in{\mathbb{N}}$. This
computation exists because $G_{d}$ admits derivation (DP), i.e.,
${\mathtt{Pop}}\xLongrightarrow{*}({\mathbf{i}}_{r}\mathbf{d}_{\overline{r}})^{n}$.
We now prove the lemma by induction on $\alpha$.

For the base case $\alpha=0$, we use derivation (D0), i.e.,
${\mathtt{F}}\xLongrightarrow{*}{\mathbf{i}}_{r}$, yielding the following
computation:

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
0\\\\[-5.0pt] \scriptstyle
0\end{array}\Bigr{)}\xrightarrow{{\mathtt{F}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n+1\\\\[-5.0pt] \scriptstyle 0\\\\[-5.0pt] \scriptstyle
0\end{array}\Bigr{)}=\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{0}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt] \scriptstyle
0\end{array}\Bigr{)}\>.$

In the case of a successor ordinal $\alpha=\beta+1$, we use derivation (D1),
i.e., ${\mathtt{F}}\xLongrightarrow{*}\mathbf{d}_{\kappa_{0}}\
(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}})^{n}\ {\mathtt{Pop}}\
({\mathtt{F}})^{n+1}\ {\mathbf{i}}_{\kappa_{0}}$, leading to the following
computation (recall that $F_{\alpha}(n)=F_{\beta}^{n+1}(n)$ by Eq. (F1)):

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
0\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{\mathbf{d}_{\kappa_{0}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\beta\end{array}\Bigr{)}\xrightarrow{(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}})^{n}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
0\\\\[-5.0pt] \scriptstyle n\\\\[-5.0pt]
\scriptstyle\beta\end{array}\Bigr{)}\xrightarrow{{\mathtt{Pop}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\beta\end{array}\Bigr{)}\xrightarrow[\text{ind.\
hyp.}]{{\mathtt{F}}^{n+1}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{\beta}^{n+1}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\beta\end{array}\Bigr{)}\xrightarrow{{\mathbf{i}}_{\kappa_{0}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{\beta}^{n+1}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\beta+1\end{array}\Bigr{)}=\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{\alpha}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\>.$

Finally, in the case of a limit ordinal $\alpha=\lambda$, say of the form
$\lambda=\gamma+\omega^{i}$ where $0<i<d$, we use derivation (DL), i.e.,
${\mathtt{F}}\xLongrightarrow{*}\mathbf{d}_{\kappa_{i}}{\mathbf{i}}_{\kappa_{i-1}}\
(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}{\mathbf{i}}_{\kappa_{i-1}})^{n}\
{\mathtt{Pop}}\ {\mathtt{F}}\ (\mathbf{d}_{\kappa_{i-1}})^{n+1}\
{\mathbf{i}}_{\kappa_{i}}$. Before inspecting the computation below, note that
if $\lambda=\gamma+\omega^{i}$ is represented by the values in
$\kappa_{0},\ldots,\kappa_{d-1}$, then one obtains a representation for
$\gamma$ by decrementing $\kappa_{i}$. Then, by incrementing $(n+1)$ times
$\kappa_{i-1}$, one obtains $\gamma+\omega^{i-1}\cdot(n+1)$ which is
$\lambda(n)$ by (L1). This leads to the following computation (recall that
$F_{\lambda}(n)=F_{\lambda(n)}(n)$ by Eq. (FL)):

$\displaystyle\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt]
\scriptstyle 0\\\\[-5.0pt]
\scriptstyle\lambda\end{array}\Bigr{)}\xrightarrow{\mathbf{d}_{\kappa_{i}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\gamma\end{array}\Bigr{)}\xrightarrow{{\mathbf{i}}_{\kappa_{i-1}}(\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}{\mathbf{i}}_{\kappa_{i-1}})^{n}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
0\\\\[-5.0pt] \scriptstyle n\\\\[-5.0pt]
\scriptstyle\lambda(n)\end{array}\Bigr{)}\xrightarrow{{\mathtt{Pop}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\lambda(n)\end{array}\Bigr{)}\xrightarrow[\text{ind.\
hyp.}]{{\mathtt{F}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{\lambda(n)}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\lambda(n)\end{array}\Bigr{)}\>,\text{ and}$
$\displaystyle\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{\lambda(n)}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\lambda(n)\end{array}\Bigr{)}=\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{\lambda}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\lambda(n)\end{array}\Bigr{)}\xrightarrow{(\mathbf{d}_{\kappa_{i-1}})^{n+1}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{\lambda}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\gamma\end{array}\Bigr{)}\xrightarrow{{\mathbf{i}}_{\kappa_{i}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
F_{\lambda}(n)\\\\[-3.99994pt] \scriptstyle 0\\\\[-5.0pt]
\scriptstyle\lambda\end{array}\Bigr{)}\>.$

In all three cases, $G_{d}$ has a computation
$\langle{n,0,\alpha}\rangle\xrightarrow{{\mathtt{F}}}\langle{F_{\alpha}(n),0,\alpha}\rangle$.

We showed in Lemma 6.6 that there are computations of $G_{d}$ that end in
$F_{\alpha}(n)$. This corresponds to the completeness of weak computers. We
will now show the safety part, i.e., that no successful computation of $G_{d}$
may reach a value greater than $F_{\alpha}(n)$.

######  Lemma 6.8.

For all $n,n^{\prime},m,m^{\prime}\in{\mathbb{N}}$,
$\alpha,\alpha^{\prime}<\omega^{d}$, and $0<i<d$, the following hold:

$\displaystyle\langle{n,m,\alpha}\rangle\xrightarrow{{\mathtt{F}}}\langle{n^{\prime},m^{\prime},\alpha^{\prime}}\rangle$
$\displaystyle\implies\alpha^{\prime}=\alpha\land n^{\prime}+m^{\prime}\leq
F_{\alpha}(n+m)\>,$ (6)
$\displaystyle\langle{n,m,\alpha}\rangle\xrightarrow{{\mathtt{Rec}}}\langle{n^{\prime},m^{\prime},\alpha^{\prime}}\rangle$
$\displaystyle\implies\alpha^{\prime}=\alpha\land n^{\prime}+m^{\prime}\leq
F^{n}_{\alpha}(n+m)\>,$ (7)
$\displaystyle\langle{n,m,\alpha}\rangle\xrightarrow{{\mathtt{Pop}}}\langle{n^{\prime},m^{\prime},\alpha^{\prime}}\rangle$
$\displaystyle\implies\alpha^{\prime}=\alpha\land
n^{\prime}+m^{\prime}=n+m\>,$ (8)
$\displaystyle\langle{n,m,\alpha}\rangle\xrightarrow{{\mathtt{Lim}}_{i}}\langle{n^{\prime},m^{\prime},\alpha^{\prime}}\rangle$
$\displaystyle\implies\alpha^{\prime}=\alpha\land n^{\prime}+m^{\prime}\leq
F_{\alpha\oplus(\omega^{i-1}\cdot n)}(n+m)\>.$ (9)

######  Proof 6.9.

By structural induction on the flow trees witnessing the transitions.

Top rule is (R1) ${\mathtt{F}}\rightarrow{\mathbf{i}}_{r}$:

Then the flow tree has the following shape (in this and following
illustrations, _we only display the top node of each immediate subtree_ of the
flow tree under consideration):

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{F}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathbf{i}}_{r}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$

Using action ${\mathbf{i}}_{r}$ in the subtree implies $n^{\prime}=n+1$, and
also $\alpha^{\prime}=\alpha$ and $m^{\prime}=m$. With (FX), we deduce
$n^{\prime}+m^{\prime}=n+m+1\leq F_{\alpha}(n+m)$ as required by (6).

Top rule is (R2) ${\mathtt{F}}\rightarrow\mathbf{d}_{\kappa_{0}}\
{\mathtt{Rec}}\ {\mathtt{F}}\ {\mathbf{i}}_{\kappa_{0}}$:

We note that the first action, $\mathbf{d}_{\kappa_{0}}$, can only be fired if
$\alpha$ is a successor ordinal $\beta+1$. Then decrementing $\kappa_{0}$
transforms $\alpha$ into $\beta$, and the flow tree has the following form.

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{F}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\beta^{\prime}+1\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{\mathbf{d}_{\kappa_{0}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\beta\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\beta\end{array}\Bigr{)}\xrightarrow{{\mathtt{Rec}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\beta_{1}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\beta_{1}\end{array}\Bigr{)}\xrightarrow{{\mathtt{F}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\beta^{\prime}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\beta^{\prime}\end{array}\Bigr{)}\xrightarrow{{\mathbf{i}}_{\kappa_{0}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\beta^{\prime}+1\end{array}\Bigr{)}$

Invoking the induction hypothesis on the second and third subtrees yields

$\displaystyle\beta_{1}$ $\displaystyle=\beta\>,$ $\displaystyle n_{1}+m_{1}$
$\displaystyle\leq F^{n}_{\beta}(n+m)\>,$ $\displaystyle\beta^{\prime}$
$\displaystyle=\beta_{1}\>,$ $\displaystyle n^{\prime}+m^{\prime}$
$\displaystyle\leq F_{\beta_{1}}(n_{1}+m_{1})\>.$

Combining these results, we obtain $\beta^{\prime}+1=\alpha$ as needed, and

$\displaystyle n^{\prime}+m^{\prime}\leq F_{\beta_{1}}(n_{1}+m_{1})$
$\displaystyle\leq F_{\beta_{1}}(F^{n}_{\beta}(n+m))$ by (FM)
$\displaystyle=F^{n+1}_{\beta}(n+m)$ $\displaystyle\leq
F^{n+m+1}_{\beta}(n+m)$ by (FX)
$\displaystyle=F_{\beta+1}(n+m)=F_{\alpha}(n+m)\>.$ by (F1)

Finally, $n^{\prime}+m^{\prime}\leq F_{\alpha}(n+m)$ as required by (6).

Top rule is (R3$i$)
${\mathtt{F}}\rightarrow\mathbf{d}_{\kappa_{i}}{\mathbf{i}}_{\kappa_{i-1}}\
{\mathtt{Lim}}_{i}\ \mathbf{d}_{\kappa_{i-1}}{\mathbf{i}}_{\kappa_{i}}$:

The flow tree has the following form.

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{F}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{\mathbf{d}_{\kappa_{i}}{\mathbf{i}}_{\kappa_{i-1}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\alpha_{1}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\alpha_{1}\end{array}\Bigr{)}\xrightarrow{{\mathtt{Lim}}_{i}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{2}\\\\[-5.0pt] \scriptstyle m_{2}\\\\[-5.0pt]
\scriptstyle\alpha_{2}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{2}\\\\[-5.0pt] \scriptstyle m_{2}\\\\[-5.0pt]
\scriptstyle\alpha_{2}\end{array}\Bigr{)}\xrightarrow{\mathbf{d}_{\kappa_{i-1}}{\mathbf{i}}_{\kappa_{i}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$

Firing the first two actions requires decrementing $\kappa_{i}$, hence
$\alpha$ is some $\alpha_{0}\oplus\omega^{i}$. After these actions, one has
$n_{1}=n$, $m_{1}=m$ and $\alpha_{1}=\alpha_{0}\oplus\omega^{i-1}$. Similarly,
the last two actions require decrementing $\kappa_{i-1}$, hence $\alpha_{2}$
is some $\alpha_{3}\oplus\omega^{i-1}$ and one has $n^{\prime}=n_{2}$,
$m^{\prime}=m_{2}$ and $\alpha^{\prime}=\alpha_{3}\oplus\omega^{i}$. One
obtains $\alpha_{1}=\alpha_{2}$, hence $\alpha^{\prime}=\alpha$, with the
induction hypothesis, as well as

$\displaystyle n^{\prime}+m^{\prime}=n_{2}+m_{2}$ $\displaystyle\leq
F_{\alpha_{1}\oplus(\omega^{i-1}\cdot n_{1})}(n_{1}+m_{1})$ by ind. hyp.
$\displaystyle=F_{(\alpha_{0}\oplus\omega^{i-1})\oplus(\omega^{i-1}\cdot
n)}(n+m)$ $\displaystyle=F_{\alpha_{0}\oplus(\omega^{i}(n))}(n+m)$
$\displaystyle\leq F_{\alpha_{0}\oplus\omega^{i}}(n+m)$ by Lemma 6.3
$\displaystyle=F_{\alpha}(n+m)\>,$

as required by (6).

Top rule is (R4) ${\mathtt{Rec}}\rightarrow{\mathtt{Pop}}$:

Then the flow tree has the following form.

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Rec}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Pop}}}{\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}}$

The induction hypothesis gives $\alpha^{\prime}=\alpha$ and
$n^{\prime}+m^{\prime}=n+m$. We deduce $n^{\prime}+m^{\prime}\leq
F_{\alpha}^{n}(n+m)$, as required by (7), by invoking (FX).

Top rule is (R5)
${\mathtt{Rec}}\rightarrow\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}\
{\mathtt{Rec}}\ {\mathtt{F}}$:

Then $n>0$ and the flow tree has the following form.

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Rec}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\beta\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n-1\\\\[-5.0pt] \scriptstyle m+1\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n-1\\\\[-5.0pt] \scriptstyle m+1\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Rec}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\beta_{1}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\beta_{1}\end{array}\Bigr{)}\xrightarrow{{\mathtt{F}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\beta\end{array}\Bigr{)}$

Here we can use the induction hypothesis on the second subtree, yielding

$\displaystyle\beta_{1}$ $\displaystyle=\alpha\>,$ $\displaystyle n_{1}+m_{1}$
$\displaystyle\leq F_{\alpha}^{n-1}(n-1+m+1)=F_{\alpha}^{n-1}(n+m)\>,$

and on the third subtree, yielding

$\displaystyle\beta$ $\displaystyle=\beta_{1}\>,$ $\displaystyle
n^{\prime}+m^{\prime}$ $\displaystyle\leq
F_{\beta_{1}}(n_{1}+m_{1})=F_{\alpha}(n_{1}+m_{1})\>.$

Combining these and invoking (FM), yields $\beta=\alpha$ and
$n^{\prime}+m^{\prime}\leq F_{\alpha}(n_{1}+m_{1})\leq
F_{\alpha}(F_{\alpha}^{n-1}(n+m))=F_{\alpha}^{n}(n+m)$ as required by (7).

Top rule is (R6) ${\mathtt{Pop}}\rightarrow\varepsilon$:

Then the flow tree
$(n,m,\alpha)\xrightarrow{{\mathtt{Pop}}}(n^{\prime},m^{\prime},\alpha^{\prime})$
is a leaf, entailing $\alpha^{\prime}=\alpha$ and $n^{\prime}+m^{\prime}=n+m$
as required by (8).

Top rule is (R7)
${\mathtt{Pop}}\rightarrow{\mathbf{i}}_{r}\mathbf{d}_{\overline{r}}\
{\mathtt{Pop}}$:

Then the flow tree has the form.

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Pop}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathbf{i}}_{r}\mathbf{d}_{\overline{r}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n+1\\\\[-5.0pt] \scriptstyle m-1\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n+1\\\\[-5.0pt] \scriptstyle m-1\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Pop}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$

The induction hypothesis on the second subtree gives $\alpha^{\prime}=\alpha$
and $n^{\prime}+m^{\prime}=n+1+m-1=n+m$ as required by (8).

Top rule is (R8$i$) ${\mathtt{Lim}}_{i}\rightarrow{\mathtt{Pop}}\
{\mathtt{F}}$:

The flow tree has the following form.

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Lim}}_{i}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Pop}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\alpha_{1}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\alpha_{1}\end{array}\Bigr{)}\xrightarrow{{\mathtt{F}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$

On these subtrees, the induction hypothesis yields
$\alpha^{\prime}=\alpha_{1}=\alpha$ and $n_{1}+m_{1}=n+m$. Furthermore we have

$\displaystyle n^{\prime}+m^{\prime}$ $\displaystyle\leq
F_{\alpha_{1}}(n_{1}+m_{1})$ by ind. hyp. $\displaystyle\leq
F_{\alpha\oplus(\omega^{i-1}\cdot n)}(n+m)\>,$ by Lemma 6.2

as required by (9).

Top rule is (R9$i$)
${\mathtt{Lim}}_{i}\rightarrow\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}{\mathbf{i}}_{\kappa_{i-1}}\
{\mathtt{Lim}}_{i}\ \mathbf{d}_{\kappa_{i-1}}$:

The flow tree has the following form.

$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle n\\\\[-5.0pt] \scriptstyle
m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{{\mathtt{Lim}}_{i}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n\\\\[-5.0pt] \scriptstyle m\\\\[-5.0pt]
\scriptstyle\alpha\end{array}\Bigr{)}\xrightarrow{\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}{\mathbf{i}}_{\kappa_{i-1}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\alpha_{1}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{1}\\\\[-5.0pt] \scriptstyle m_{1}\\\\[-5.0pt]
\scriptstyle\alpha_{1}\end{array}\Bigr{)}\xrightarrow{{\mathtt{Lim}}_{i}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{2}\\\\[-5.0pt] \scriptstyle m_{2}\\\\[-5.0pt]
\scriptstyle\alpha_{2}\end{array}\Bigr{)}$$\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n_{2}\\\\[-5.0pt] \scriptstyle m_{2}\\\\[-5.0pt]
\scriptstyle\alpha_{2}\end{array}\Bigr{)}\xrightarrow{\mathbf{d}_{\kappa_{i-1}}}\Bigl{(}\begin{array}[]{@{}c@{}}\scriptstyle
n^{\prime}\\\\[-5.0pt] \scriptstyle m^{\prime}\\\\[-5.0pt]
\scriptstyle\alpha^{\prime}\end{array}\Bigr{)}$

With its three actions, the first subtree implies

$\displaystyle n_{1}$ $\displaystyle=n-1\>,$ $\displaystyle m_{1}$
$\displaystyle=m+1\>,$ $\displaystyle\alpha_{1}$
$\displaystyle=\alpha\oplus\omega^{i-1}\>.$

Similarly, the last subtree yields

$\displaystyle n^{\prime}$ $\displaystyle=n_{2}\>,$ $\displaystyle m^{\prime}$
$\displaystyle=m_{2}\>,$ $\displaystyle\alpha_{2}$
$\displaystyle=\alpha^{\prime}\oplus\omega^{i-1}\>.$

With the second subtree, the induction hypothesis yields
$\alpha_{2}=\alpha_{1}$ and $n_{2}+m_{2}\leq
F_{\alpha_{1}\oplus(\omega^{i-1}\cdot n_{1})}(n_{1}+m_{1})$. Combining these
gives $\alpha^{\prime}=\alpha$ and $n^{\prime}+m^{\prime}=n_{2}+m_{2}\leq
F_{\alpha_{1}\oplus(\omega^{i-1}\cdot
n_{1})}(n_{1}+m_{1})=F_{(\alpha\oplus\omega^{i-1})\oplus(\omega^{i-1}\cdot(n-1))}(n+m)=F_{\alpha\oplus(\omega^{i-1}\cdot
n)}(n+m)$ as required by (9).

Now, for any ordinal $\alpha<\omega^{d}$, we may extend $G_{d}$ and obtain a
GVAS $G_{F_{\alpha}}$ that weakly computes $F_{\alpha}$. This new GVAS
inherits the counters, actions, non-terminals and rules of $G_{d}$. It
furthermore includes two additional non-terminals, ${\mathtt{S}}$ and
${\mathtt{Pop}}^{\prime}$, and associated rules. The start symbol will be
${\mathtt{S}}$ and, if $\alpha$’s CNF is $\sum_{i=d-1}^{0}\omega^{i}\cdot
c_{i}$, the extra rules are:

$\displaystyle{\mathtt{S}}$
$\displaystyle\rightarrow{\mathbf{i}}_{\kappa_{0}}^{c_{0}}{\mathbf{i}}_{\kappa_{1}}^{c_{1}}\cdots{\mathbf{i}}_{\kappa_{d-1}}^{c_{d-1}}\
{\mathtt{F}}\ {\mathtt{Pop}}^{\prime}\>,$ (R0)
$\displaystyle{\mathtt{Pop}}^{\prime}$
$\displaystyle\rightarrow\varepsilon\>,$ (R10)
$\displaystyle{\mathtt{Pop}}^{\prime}$
$\displaystyle\rightarrow\mathbf{d}_{r}{\mathbf{i}}_{\overline{r}}\
{\mathtt{Pop}}^{\prime}\>.$ (R11)

It is clear that, since there are no new rules for the non-terminals inherited
from $G_{d}$, the properties stated in Lemmas 6.4 to 6.8 hold for
$G_{F_{\alpha}}$ as they hold for $G_{d}$. Note also that
${\mathtt{Pop}}^{\prime}$ behaves as ${\mathtt{Pop}}$ but exchanging the roles
of $r$ and $\overline{r}$.

######  Lemma 6.10.

$G_{F_{\alpha}}$ weakly computes $F_{\alpha}$.

######  Proof 6.11.

We start with the completeness part of Definition 5.1. For this it is needed
to show that, for any $n\in{\mathbb{N}}$, $G_{F_{\alpha}}$ has a computation
of the form
$(n,0,{\mathbf{0}}_{d})\xrightarrow{{\mathtt{S}}}(n^{\prime},F_{\alpha}(n),\mathbf{e})$.
For this we use the rule (R0) and exhibit the following computation:

$(n,0,{\mathbf{0}}_{d})\xrightarrow{{\mathbf{i}}_{\kappa_{0}}^{c_{0}}{\mathbf{i}}_{\kappa_{1}}^{c_{1}}\cdots{\mathbf{i}}_{\kappa_{d-1}}^{c_{d-1}}}(n,0,\alpha)\xrightarrow{{\mathtt{F}}}(F_{\alpha}(n),0,\alpha)\xrightarrow{{\mathtt{Pop}}^{\prime}}(0,F_{\alpha}(n),\alpha)\>.$

The first part of that computation just relies on our convention for reading
$\kappa_{d-1},\ldots,\kappa_{0}$ as the encoding of an ordinal, the second
(crucial) part is given by Lemma 6.6, and the last part is by an analog of
derivation (DP) for ${\mathtt{Pop}}^{\prime}$.

For the safety part, we consider an arbitrary computation of the form
$(n,0,{\mathbf{0}}_{d})\xrightarrow{{\mathtt{S}}}(n^{\prime},r,\mathbf{e})$.
The only rule for ${\mathtt{S}}$ is (R0), so there must exist some steps of
the form

$(n,0,{\mathbf{0}}_{d})\xrightarrow{{\mathbf{i}}_{\kappa_{0}}^{c_{0}}{\mathbf{i}}_{\kappa_{1}}^{c_{1}}\cdots{\mathbf{i}}_{\kappa_{d-1}}^{c_{d-1}}}(n,0,\alpha)\xrightarrow{{\mathtt{F}}}(n^{\prime},m^{\prime},\alpha^{\prime})\xrightarrow{{\mathtt{Pop}}^{\prime}}(n^{\prime\prime},r,\mathbf{e})\>.$

Necessarily, this satisfies $n^{\prime}+m^{\prime}\leq F_{\alpha}(n)$ by (6).
And since ${\mathtt{Pop}}^{\prime}$ behaves like ${\mathtt{Pop}}$, we have
$n^{\prime\prime}+r=n^{\prime}+m^{\prime}$, as in (8). All this entails $r\leq
F_{\alpha}(n)$ as required by (SA).

##  7\. Concluding Remarks

We proved that Grammar-controlled VASes or Pushdown VASes cannot weakly
compute numerical functions that are sublinear. This was recently shown for
plain VASes [24]. We also proved that GVASes can weakly compute the fast-
growing functions $F_{\alpha}$ for all $\alpha<\omega^{\omega}$ while VASes
can only weakly compute $F_{\alpha}$ for $\alpha<\omega$.

This research is motivated by verification questions for well-structured
systems, in particular VASes and their extensions. In this area, weakly
computable functions have traditionally been used to prove hardness results.
Recent hardness proofs for well-structured systems crucially rely on the
ability to weakly compute both fast-growing and slow-growing functions.

This work raises some new questions that are left for future work, including
whether GVASes can weakly compute $F_{\omega^{\omega}}$ and whether slow-
growing functions can be weakly computed in other VAS extensions like the
VASes with nested zero-tests of [30].

Another open question is the decidability of the boundedness problem for
GVASes. Boundedness is decidable for PVASes [22] but the two problems do not
coincide: on the one hand, in GVASes we only consider sequences of actions
that are the yields of complete derivation trees of a grammar, corresponding
to configurations in PVAS that have empty stack content; on the other hand
unboundedness in PVASes can come from unbounded counters or unbounded stack,
while in GVASes only counters are measured. Indeed, the counter-boundedness
problem for PVASes reduces to the boundedness problem for GVASes and is still
open, while the stack-boundedness problem was shown decidable in [25].

The reachability problem for GVASes is also a source of open problems.
Recently, the complexity of the reachability problem for plain VASes was
proved to be between $\mathbf{F}_{3}$ and $\mathbf{F}_{\omega}$ [5, 23] in the
complexity hierarchy set up by Schmitz [31]. Improving the $\mathbf{F}_{3}$
lower bound in the case of GVASes is an open question, as is the decidability
status of the reachability problem.

## References

  * [1] P. A. Abdulla, K. Čerāns, B. Jonsson, and Yih-Kuen Tsay.  Algorithmic analysis of programs with well quasi-ordered domains.  Information & Computation, 160(1–2):109–127, 2000.
  * [2] M. F. Atig and P. Ganty.  Approximating Petri net reachability along context-free traces.  In FSTTCS 2011, volume 13 of LIPIcs, pages 152–163. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
  * [3] A. Bouajjani and M. Emmi.  Analysis of recursively parallel programs.  In POPL 2012, pages 203–214. ACM, 2012.
  * [4] P. Chambart and Ph. Schnoebelen.  The ordinal recursive complexity of lossy channel systems.  In LICS 2008, pages 205–216. IEEE, 2008.
  * [5] W. Czerwiński, S. Lasota, R. Lazic, J. Leroux, and F. Mazowiecki.  The reachability problem for Petri nets is not elementary.  In STOC 2019, pages 24–33. ACM, 2019.
  * [6] S. Demri, D. Figueira, and M. Praveen.  Reasoning about data repetitions with counter systems.  In LICS 2013, pages 33–42. IEEE, 2013.
  * [7] S. Demri, M. Jurdziński, O. Lachish, and R. Lazić.  The covering and boundedness problems for branching vector addition systems.  Journal of Computer and System Sciences, 79(1):23–38, 2013.
  * [8] A. Finkel and Ph. Schnoebelen.  Well-structured transition systems everywhere!  Theoretical Computer Science, 256(1–2):63–92, 2001.
  * [9] S. Ginsburg and E. H. Spanier.  Semigroups, Presburger formulas, and languages.  Pacific J. Math., 16(2):285–296, 1966.
  * [10] S. A. Greibach.  Remarks on blind and partially blind one-way multicounter machines.  Theoretical Computer Science, 7:311–324, 1978.
  * [11] Ch. Haase, S. Schmitz, and Ph. Schnoebelen.  The power of priority channel systems.  Logical Methods in Comp. Science, 10(4:4), 2014.
  * [12] M. Hack.  The equality problem for vector addition systems is undecidable.  Theoretical Computer Science, 2(1):77–95, 1976.
  * [13] S. Haddad and D. Poitrenaud.  Recursive Petri nets: Theory and application to discrete event systems.  Acta Informatica, 44(7–8):463–508, 2007.
  * [14] S. Haddad, S. Schmitz, and Ph. Schnoebelen.  The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets.  In LICS 2012, pages 355–364. IEEE, 2012.
  * [15] P. Jančar.  Decidability of a temporal logic problem for Petri nets.  Theoretical Computer Science, 74(1):71–93, 1990.
  * [16] P. Jančar.  Nonprimitive recursive complexity and undecidability for Petri net equivalences.  Theoretical Computer Science, 256(1–2):23–30, 2001.
  * [17] M. Jantzen and R. Valk.  Formal properties of Place/Transition nets.  In Net Theory and Applications, volume 84 of Lect. Notes Comp. Sci., pages 165–212. Springer, 1980.
  * [18] J. B. Kruskal.  Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture.  Trans. Amer. Math. Soc., 95(2):210–225, 1960.
  * [19] R. Lazić.  The reachability problem for vector addition systems with a stack is not elementary.  CoRR, abs/1310.1767, 2013.
  * [20] R. Lazić, T. Newcomb, J. Ouaknine, A. W. Roscoe, and J. Worrell.  Nets with tokens which carry data.  Fundamenta Informaticae, 88(3):251–274, 2008.
  * [21] R. Lazić and P. Totzke.  What makes Petri nets harder to verify: Stack or data?  In Concurrency, Security, and Puzzles, volume 10160 of Lect. Notes Comp. Sci., pages 144–161. Springer, 2017.
  * [22] J. Leroux, M. Praveen, and G. Sutre.  Hyper-Ackermannian bounds for pushdown vector addition systems.  In CSL-LICS 2014, pages 63:1–63:10. ACM, 2014.
  * [23] J. Leroux and S. Schmitz.  Reachability in vector addition systems is primitive-recursive in fixed dimension.  In LICS 2019. IEEE, 2019.
  * [24] J. Leroux and Ph. Schnoebelen.  On functions weakly computable by Petri Nets and Vector Addition Systems.  In RP 2014, volume 8762 of Lect. Notes Comp. Sci., pages 190–202. Springer, 2014.
  * [25] J. Leroux, G. Sutre, and P. Totzke.  On boundedness problems for pushdown vector addition systems.  In RP 2015, volume 9328 of Lecture Notes in Computer Science, pages 101–113. Springer, 2015.
  * [26] J. Leroux, G. Sutre, and P. Totzke.  On the coverability problem for pushdown vector addition systems in one dimension.  In ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 324–336. Springer, 2015.
  * [27] Jérôme Leroux.  Vector addition system reachability problem: a short self-contained proof.  In POPL, pages 307–316. ACM, 2011.
  * [28] E. W. Mayr and A. R. Meyer.  The complexity of the finite containment problem for Petri nets.  Journal of the ACM, 28(3):561–576, 1981.
  * [29] R. Mayr.  Process rewrite systems.  Information and Computation, 156(1/2):264–286, 2000.
  * [30] K. Reinhardt.  Reachability in Petri nets with inhibitor arcs.  Electr. Notes Theor. Comput. Sci., 223:239–264, 2008.
  * [31] S. Schmitz.  Complexity hierarchies beyond Elementary.  ACM Trans. Computation Theory, 8(1), 2016.
  * [32] Ph. Schnoebelen.  Verifying lossy channel systems has nonprimitive recursive complexity.  Information Processing Letters, 83(5):251–261, 2002.
  * [33] Ph. Schnoebelen.  Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets.  In MFCS 2010, volume 6281 of Lect. Notes Comp. Sci., pages 616–628. Springer, 2010.
  * [34] K. Sen and M. Viswanathan.  Model checking multithreaded programs with asynchronous atomic methods.  In CAV 2006, volume 4144 of Lect. Notes Comp. Sci., pages 300–314. Springer, 2006.

##  Appendix A Well-quasi-ordering flow trees

We now prove Lemma 3.5, stating that $\leq_{G}$ is a well-quasi-ordering of
$F(G)$, this for any GVASS $G$. A simple way to prove this is to reformulate
$\leq_{G}$ as an homeomorphic embedding on flow trees labeled with enriched
information equipped with further labels.

With a flow tree $t=\sigma[t_{1},\ldots,t_{k}]$ we associate a tree
$\operatorname{adorn}(t)$ made of a root labeled with
$\langle\operatorname{root}(t),\operatorname{root}(t_{1}),\ldots,\operatorname{root}(t_{k})\rangle$
and having $\operatorname{adorn}(t_{1}),\ldots,\operatorname{adorn}(t_{k})$ as
immediate subtrees. The nodes of $\operatorname{adorn}(t)$ are labeled by
tuples of the form
$\langle({\mathbf{c}}_{0},X,{\mathbf{c}}_{k}),({\mathbf{c}}_{0},X_{1},{\mathbf{c}}_{1}),\ldots,({\mathbf{c}}_{k-1},X_{k},{\mathbf{c}}_{k})\rangle$
where ${\mathbf{c}}_{0},\ldots,{\mathbf{c}}_{k}\in{\mathbb{N}}^{d}$ are
configurations and where $X$ is a rule in $R$, or $X\in\mathbf{A}$ is a
terminal action and $k=0$. Such a tuple is called an _instance_ of the rule
$X$ (or of the action $X\in\mathbf{A}$). Given two instances
$\lambda=\langle({\mathbf{c}}_{0},X,{\mathbf{c}}_{k}),({\mathbf{c}}_{0},X_{1},{\mathbf{c}}_{1}),\ldots,({\mathbf{c}}_{k-1},X_{k},{\mathbf{c}}_{k})\rangle$
and
$\lambda^{\prime}=\langle({\mathbf{d}}_{0},Y,{\mathbf{d}}_{\ell}),({\mathbf{d}}_{0},Y_{1},{\mathbf{d}}_{1}),\ldots,({\mathbf{d}}_{\ell-1},Y_{\ell},{\mathbf{d}}_{\ell})\rangle$,
we write $\lambda\leq\lambda^{\prime}$ when $(X$ and $(Y$ are the same rule or
action —entailing $k=\ell$— and when ${\mathbf{c}}_{j}\leq{\mathbf{d}}_{j}$
for all $1\leq j\leq k$. Suppose $s$ is a flow tree with immediate subtrees
$s_{1},\ldots,s_{k}$. We write
$\operatorname{adorn}(s)\sqsubseteq\operatorname{adorn}(t)$ if there is a
subtree $t^{\prime}$ of $t$ with immediate subtrees $t_{1},\ldots,t_{l}$ such
that
$\operatorname{root}(\operatorname{adorn}(s))\leq\operatorname{root}(\operatorname{adorn}(t^{\prime}))$
(entailing $k=l$) and inductively
$\operatorname{adorn}(s_{j})\sqsubseteq\operatorname{adorn}(t_{j})$ for all
$1\leq j\leq k$. It is easy to see that on derived trees of flow trees,
$\sqsubseteq$ coincides with the standard homeomorphic embedding of labeled
trees.

######  Lemma A.5.

$s\leq_{G}t$ if, and only if,
$\operatorname{root}(s)\leq\operatorname{root}(t)\land\operatorname{adorn}(s)\sqsubseteq\operatorname{adorn}(t)$.

######  Proof A.6.

We assume $s=\sigma[s_{1},\ldots,s_{k}]$, $t=\theta[t_{1},\ldots,t_{\ell}]$
and prove the claim by structural induction.
${\implies}$: Assume $s\leq_{G}t$. Thus
$\operatorname{root}(s)\leq\operatorname{root}(t)$ and, by definition of
$\leq_{G}$, $t$ contains a subtree
$t^{\prime}=\theta^{\prime}[t^{\prime}_{1},\ldots,t^{\prime}_{k}]$ with

$\sigma\leq\theta^{\prime}\land s_{1}\leq_{G}t^{\prime}_{1}\land\cdots\land
s_{k}\leq_{G}t^{\prime}_{k}\>.$

Now this entails $\operatorname{root}(s)\leq\operatorname{root}(t^{\prime})$
and $\operatorname{root}(s_{i})\leq\operatorname{root}(t^{\prime}_{i})$ for
all $i$, as well as (by ind. hyp.)
$\operatorname{adorn}(s_{i})\sqsubseteq\operatorname{adorn}(t^{\prime}_{i})$
for all $i$. Hence
$\operatorname{adorn}(s)\sqsubseteq\operatorname{adorn}(t^{\prime})$,
entailing $\operatorname{adorn}(s)\sqsubseteq\operatorname{adorn}(t)$.

${\impliedby}$: We assume $\operatorname{root}(s)\leq\operatorname{root}(t)$
and $\operatorname{adorn}(s)\sqsubseteq\operatorname{adorn}(t)$. Hence there
is a subtree $t^{\prime}$ of $t$ with immediate subtrees
$t^{\prime}_{1},\ldots,t^{\prime}_{k}$ such that
$\operatorname{root}(\operatorname{adorn}(s))\leq\operatorname{root}(\operatorname{adorn}(t^{\prime}))$
and
$\operatorname{adorn}(s_{i})\sqsubseteq\operatorname{adorn}(t^{\prime}_{i})$
for all $i=1,\ldots,k$. From
$\operatorname{root}(\operatorname{adorn}(s))\leq\operatorname{root}(\operatorname{adorn}(t^{\prime}))$,
we infer that
$\operatorname{root}(s_{i})\leq\operatorname{root}(t^{\prime}_{i})$ for all
$i=1,\ldots,k$. Now one witnesses $s\leq_{G}t$ by observing that
$s_{i}\leq_{G}t_{i}$ by ind. hyp.

Since the instances of rules are well-quasi-ordered by $\leq$ (there are only
finitely many rules), $\sqsubseteq$ is a well-quasi-ordering by Kruskal’s Tree
Theorem [18]. With Lemma A.5 we immediately infer that $\leq_{G}$ is a well-
quasi-ordering.

##  Appendix B Monotonicity for Fast-Growing functions

We give detailed proofs for the two monotonicity lemmas stated after the
definitions of the $F_{\alpha}$ functions in section 6.

######  Lemma 6.1.

For any ordinals $\alpha,\alpha^{\prime}<\epsilon_{0}$ and any
$n\in{\mathbb{N}}$, $F_{\alpha}(n)\leq F_{\alpha\oplus\alpha^{\prime}}(n)$.

######  Proof 6.2.

By induction on $\alpha^{\prime}$, then on $\alpha$. We first observe that, if
the claim holds for some given $\alpha$ and $\alpha^{\prime}$, then it entails
$F^{m}_{\alpha}(n)\leq F^{m}_{\alpha\oplus\alpha^{\prime}}(n)$ for any $m>0$
as a consequence of monotonicity, i.e., (FM).

We now consider several cases for $\alpha$ and $\alpha^{\prime}$:

  * •

If $\alpha^{\prime}=0$, then $\alpha\oplus\alpha^{\prime}=\alpha$ and the
claim holds trivially.

  * •

If $\alpha=0$ then the claim becomes $F_{0}(n)\leq F_{\alpha^{\prime}}(n)$,
which holds since $F_{0}(n)=n+1$ by (F0) and $n+1\leq F_{\alpha^{\prime}}(n)$
by (FX).

  * •

If $\alpha^{\prime}=\beta^{\prime}+1$ is a successor then
$\alpha\oplus\alpha^{\prime}$ is $(\alpha\oplus\beta^{\prime})+1$ and we have
$F_{\alpha}(n)\leq F_{\alpha\oplus\beta^{\prime}}(n)$ by ind. hyp., $\leq
F_{\alpha\oplus\beta^{\prime}}^{n+1}(n)$ by (FX),
$=F_{\alpha\oplus\beta^{\prime}+1}(n)=F_{\alpha\oplus\alpha^{\prime}}(n)$, and
we are done.

  * •

If $\alpha=\beta+1$ is a successor then $\alpha\oplus\alpha^{\prime}$ is
$(\beta\oplus\alpha^{\prime})+1$ and we have
$F_{\alpha}(n)=F_{\beta}^{n+1}(n)\leq F_{\beta\oplus\alpha^{\prime}}^{n+1}(n)$
by ind. hyp., $=F_{\alpha\oplus\alpha^{\prime}}(n)$.

  * •

The only remaining possibility is that both $\alpha$ and $\alpha^{\prime}$ are
limit ordinals. Then $(\alpha\oplus\alpha^{\prime})(n)$ is
$\alpha\oplus\alpha^{\prime}(n)$ or $\alpha(n)\oplus\alpha^{\prime}$,
depending on which limit has the CNF with smallest last summand. In the first
case we have $F_{\alpha}(n)\leq F_{\alpha\oplus\alpha^{\prime}(n)}(n)$ by ind.
hyp. since $\alpha^{\prime}(n)<\alpha^{\prime}$,
$=F_{(\alpha\oplus\alpha^{\prime})(n)}(n)=F_{\alpha\oplus\alpha^{\prime}}(n)$.
In the second case we have $F_{\alpha}(n)=F_{\alpha(n)}(n)\leq
F_{\alpha(n)\oplus\alpha^{\prime}}(n)$ by ind. hyp. since $\alpha(n)<\alpha$,
$=F_{(\alpha\oplus\alpha^{\prime})(n)}(n)=F_{\alpha\oplus\alpha^{\prime}}(n)$.

######  Lemma 6.3.

For any ordinal $\alpha<\epsilon_{0}$ and limit ordinal
$\lambda<\omega^{\omega}$, for any $m,n\in{\mathbb{N}}$, if $m\leq n$ then
$F_{\alpha\oplus\lambda(m)}(n)\leq F_{\alpha\oplus\lambda}(n)$.

######  Proof 6.4.

Let us decompose $\lambda$ under the form $\lambda=\delta+\omega^{k+1}$ so
that $\lambda(m)=\delta+\omega^{k}\cdot(m+1)$. We prove the lemma by induction
on $\alpha$. We first observe that, if the claim holds for some given
$\alpha$, then $F^{p}_{\alpha\oplus\lambda(m)}(n)\leq
F^{p}_{\alpha\oplus\lambda}(n)$ for every $p>0$ and every $m,n\in{\mathbb{N}}$
such that $m\leq n$. This observation, which is easily proved by induction on
$p$, is a consequence of strict expansivity and monotonicity, i.e., (FX) and
(FM), respectively.

  * •

If $\alpha=0$ we have $F_{\alpha\oplus\lambda(m)}(n)=F_{\lambda(m)}(n)\leq
F_{\lambda(n)}(n)$ by Lemma 6.2 since
$\lambda(n)=\lambda(m)\oplus\omega^{k}\cdot(n-m)$,
$=F_{\lambda}(n)=F_{\alpha\oplus\lambda}(n)$ by (FL).

  * •

If $\alpha=\beta+1$ is a successor, we have
$F_{\alpha\oplus\lambda(m)}(n)=F_{(\beta\oplus\lambda(m))+1}(n)=F^{n+1}_{\beta\oplus\lambda(m)}(n)$
by (F1), $\leq F^{n+1}_{\beta\oplus\lambda}(n)$ by ind. hyp.,
$=F_{(\beta\oplus\lambda)+1}(n)=F_{\alpha\oplus\lambda}(n)$ again by (F1).

  * •

If $\alpha=\gamma+\omega^{\beta}$ is a limit, then $\alpha\oplus\lambda$ is a
limit too and we can compare $\omega^{\beta}$ and $\omega^{k+1}$, the last
summands of $\alpha$ and $\lambda$. There are two subcases:

    * –

If $0<\beta\leq k$ then $(\alpha\oplus\lambda)(n)=\alpha(n)\oplus\lambda$.
Moreover, $\alpha\oplus\lambda(m)$ is a limit since $0<k$, and
$(\alpha\oplus\lambda(m))(n)=\alpha(n)\oplus\lambda(m)$. We deduce
$F_{\alpha\oplus\lambda(m)}(n)=F_{\alpha(n)\oplus\lambda(m)}(n)$ by (FL),
$\leq F_{\alpha(n)\oplus\lambda}(n)$ by ind. hyp.,
$=F_{(\alpha\oplus\lambda)(n)}(n)=F_{\alpha\oplus\lambda}(n)$ again by (FL).

    * –

If $k+1\leq\beta$ then $(\alpha\oplus\lambda)(n)=\alpha\oplus\lambda(n)$. We
deduce $F_{\alpha\oplus\lambda(m)}(n)\leq F_{\alpha\oplus\lambda(n)}(n)$ by
Lemma 6.2 since $m\leq n$,
$=F_{(\alpha\oplus\lambda)(n)}(n)=F_{\alpha\oplus\lambda}(n)$ by (FL) and we
are done.