Abstract-We show how to reliably compute fast-growing functions with timed-arc Petri nets and data nets. This construction provides ordinal-recursive lower bounds on the complexity of the main decidable properties (safety, termination, regular simulation, etc.) of these models. Since these new lower bounds match the upper bounds that one can derive from wqo theory, they precisely characterise the computational power of these socalled "enriched" nets.

Index Terms-Complexity theory, fast-growing hierarchy, formal verification, Petri nets, well-structured systems

I. INTRODUCTION

We call enriched nets a handful of Petri net extensions where tokens are coloured with data values, that still enjoy decidable verification problems: timed-arc Petri nets (TPN) where tokens carry real-valued clocks [START_REF] Bolognesi | From timed Petri nets to timed LOTOS[END_REF], data nets (DN) and Petri data nets (PDN) where they carry a datum from some dense domain [START_REF] Lazić | Nets with tokens which carry data[END_REF], and constrained multiset rewriting systems (CMRS) where they carry positive integers [START_REF] Abdulla | On the coverability problem for constrained multiset rewriting[END_REF]. Their richer structure makes enriched nets a natural choice when modelling for instance parameterised systems, protocols, workflows, or real-time systems-in fact, timed extensions of Petri nets have been in use since the 1970's for such modelling tasks. In spite of the presence of two "sources" of infiniteness, the number of tokens and their colours, enriched nets can be handled by the now standard toolkit of well quasi-orders (wqo) and well-structured transition systems (WSTS) [START_REF] Abdulla | Algorithmic analysis of programs with well quasiordered domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF] so that e.g. safety-which in this context corresponds to the coverability problem-and other properties are decidable [START_REF] Abdulla | Timed Petri nets and BQOs[END_REF][START_REF] Abdulla | Dense-timed Petri nets: Checking Zenoness, token liveness and boundedness[END_REF][START_REF] Bouyer | Timed Petri nets and timed automata: On the discriminating power of Zeno sequences[END_REF].

Recent investigations [START_REF] Abdulla | A classification of the expressive power of well-structured transition systems[END_REF][START_REF] Bonnet | Comparing Petri Data Nets and Timed Petri Nets[END_REF] have shown that all these formalisms are expressively equivalent, i.e. they define the same class of so-called coverability languages, and thus in particular their coverability problems are inter-reducible. Their computational complexity, however, has rarely been analysed. The employed wqo and WSTS techniques are generally seen as non-constructive, hence the aforementioned works do not provide any complexity analysis of the algorithms they propose [START_REF] Lazić | Nets with tokens which carry data[END_REF]Prop. 3.2] gives a lower bound: PDNs can simulate lossy channel systems and hence inherit at least their F ω ω complexity [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF], but this is far from optimal). We prove in this paper that the complexity of enriched nets is exactly at level F ω ω ω in the fast-growing hierarchy.

1) The upper bound is a consequence of a generic technique described in [START_REF] Schmitz | Multiply-recursive bounds with Higman's Lemma[END_REF]: the length-function theorem for elementary wqos, here instantiated with (N k ) * as the underlying wqo. It applies uniformly to DN, PDNs, TPNs, CMRSs (and to some further extensions); see Sec. IV.

2) The matching lower bound is our main contribution: it relies on the construction of PDNs with O(k) unbounded places that can compute in a weak sense the fast-growing functions F ω ω k and their inverses and therefore simulate F ω ω kbounded computations (see Sec. V for an overview). This construction relies on several intermediate steps: we first define in Sec. VI-A a cumulative encoding of ordinals below ω ω ω k in sequences of vectors of integers (or "codes") along with rewriting rules over codes implementing fast-growing computations and their inverses (see Sec. VI-B). Because this encoding is robust, i.e. safe wrt. Higman's ordering on codes, any weak implementation of the rewriting rules will yield the desired behaviour (Sec. VI-C); in particular, a weak PDN implementation is possible, as shown in Sec. VII. Once established for PDNs, the new lower bound automatically applies to TPNs and DNs.

3) Beyond the complexity of verification problems, our techniques are easily applied to the study of the coverability languages of WSTS models [START_REF] Geeraerts | Wellstructured languages[END_REF]. Here our construction directly yields separation results; see Sec. VIII.

The details of the proofs and of the construction of PDNs can be found in the long version of the paper.

II. PETRI DATA NETS

Although the complexity of decision problems in timedarc Petri nets provided our prime motivation-an important body of literature is dedicated to their analysis [START_REF] Bolognesi | From timed Petri nets to timed LOTOS[END_REF][START_REF] Abdulla | Timed Petri nets and BQOs[END_REF][START_REF] Abdulla | Dense-timed Petri nets: Checking Zenoness, token liveness and boundedness[END_REF][START_REF] Bouyer | Timed Petri nets and timed automata: On the discriminating power of Zeno sequences[END_REF] and they are actually employed in tools [e.g. 18]-, we will work exclusively with Petri data nets, which proved easier to manipulate, and rely on known interreducibility results [START_REF] Bonnet | Comparing Petri Data Nets and Timed Petri Nets[END_REF][START_REF] Abdulla | A classification of the expressive power of well-structured transition systems[END_REF] to capture the other classes of enriched nets.

A. Definitions

We denote by 0 the null vector in N k for any k, and for a word w = x 1 • • • x n we write |w| = n and w(i) = x i .

A Petri Data Net (PDN) is a Petri net where each token carries an identity from a linearly ordered and dense domain D. A marking s of a PDN with P as set of places could be seen, e.g., as a multiset of pairs in D × P , or as a map s ∈ (N P ) D . However, two key features of PDNs will guide our choice of (N |P | \ 0) * for representing markings:

1) a marking s only has finitely many tokens, thus denoting d 1 < • • • < d m the identities that occur in s and gathering all the tokens that carry the same identity d i , one obtains a (non-null) place vector v i in N |P | \ 0: s can be written as a sequence (d 1 , v 1 ) • • • (d m , v m ), implicitly associating the null vector 0 with any d ∈ D \ {d 1 , . . . , d m }; 2) the concrete identities d i are irrelevant, and only their relative order is useful wrt. the dynamics of the net, thus s can safely be abstracted as the sequence

v 1 • • • v m in (N |P | \ 0) * .
(Also the choice of the concrete set D is irrelevant.) Every transition t of a PDN specifies a sequence of n ordered potential identities and for any such identity specifies the tokens cons to be consumed and prod to be produced. Thus cons(t) and prod (t) are two sequences of n (possibly null) place vectors.

Definition 1 (Petri Data Nets). A k-dimensional Petri Data Net (k-PDN) is a tuple N = (P, T, cons, prod , s 0 ) where

• P is a finite set of k = |P | places,

• T is a finite set of transitions with P ∩ T = ∅,

• for every t in T , cons(t) and prod (t) are finite sequences in (N k ) * with |cons(t)| = |prod (t)|, and

• s 0 is an initial marking in (N k \ 0) * . Consider now a marking s ∈ (N k \ 0) * . In order to fire a transition t with |cons(t)| = n, nondeterministically select n identities, consume some of their tokens as indicated by cons(t), and produce new tokens with the identities specified by prod (t). However, some of these n identities might not be present in s, and we should introduce null vectors wherever necessary: s ∈ (N k ) * is a 0-extension of s ∈ (N k \ 0) * (or s is the 0-contraction of s ) def ⇔ s is obtained by removing all 0's from s . Once an extension s is built, select in it a subword of n vectors x 1 , . . . , x n s.t. every vector contains enough tokens, i.e. with x i ≥ cons(t)(i). If the condition is fulfilled, the corresponding tokens are consumed and prod (t)(i) is added to the resulting vector, yielding a new sequence s . This s may contain null vectors, e.g. when all tokens with some identity have been consumed, hence the reached marking really is the 0-contraction of s . Note that any way of firing t requires at most n insertions. Examples of PDNs will be found in Section VII.

Definition 2 (Semantics of PDNs). The transition system associated with a k-PDN N = (P, T, cons, prod , s 0 ) is (S, s 0 , →) with state set S def = (N k \ 0) * and transition relation

→ def = t∈T t - →, where s t - → s for t ∈ T iff, letting n = |cons(t)|: • there exists u 0 x 1 u 1 • • • u n-1 x n u n a 0-extension of s with for all i, u i ∈ (N k ) * and x i ∈ N k ;
• for i in {1, . . . , n}, x i ≥ cons(t)(i);

• and defining

y i = x i -cons(t)(i) + prod (t)(i), s is the 0-contraction of u 0 y 1 u 1 • • • u n-1 y n u n .
Below we consider three decision problems for PDNs:

(Strong) Coverability: Given N and p ∈ P , can we reach a configuration where p holds at least one token? Boundedness: Given N , is the set of reachable configurations in S finite? Termination: Given N , is every run finite?

B. PDNs as Well-Structured Transition Systems

A wqo (A, ≤) is a set A endowed with a transitive and reflexive relation ≤ s.t. every infinite sequence σ = a 0 , a 1 , • • • of elements of A contains a pair a i ≤ a j for some i < j. Some classical examples of wqos are Dickson's Lemma: (N k , ≤) with the product ordering defined by

x ≤ y def ⇔ ∀0 ≤ j < k, x[j] ≤ y[j], Higman's Lemma: if (A, ≤) is a wqo, then (A * , ≤ * ) the set
of finite sequences of elements of A along with the subword embedding ordering is also a wqo, where

≤ * is defined by s ≤ * s def ⇔ s = a 1 • • • a n , s = x 0 b 1 x 1 • • • b n x n with x 0 , . . . , x n in A * and a i ≤ b i for all 1 ≤ i ≤ n.
The transition system associated with a PDN (see Definition 2) is well-structured [START_REF] Abdulla | Algorithmic analysis of programs with well quasiordered domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF] for the wqo (S, ≤ * ): if s 1 t -→ s 2 and s 1 ≤ * s 3 , then there exists s 4 s.t. s 2 ≤ * s 4 and s 3 t -→ s 4 . This (strict) compatibility of the transition relation with the ordering allows to employ generic algorithms for deciding coverability, boundedness, and termination. In fact, the same generic WSTS algorithms show that coverability, boundedness and termination are decidable

• for TPNs [START_REF] Abdulla | Dense-timed Petri nets: Checking Zenoness, token liveness and boundedness[END_REF], even when extended with read arcs [START_REF] Bouyer | Timed Petri nets and timed automata: On the discriminating power of Zeno sequences[END_REF] or transport arcs [START_REF] Jacobsen | Verification of timed-arc Petri nets[END_REF], • for CMRSs [START_REF] Abdulla | On the coverability problem for constrained multiset rewriting[END_REF], and • as far as coverability and termination are concerned, for DNs [START_REF] Lazić | Nets with tokens which carry data[END_REF]. Compared to PDNs, these allow so-called whole-place operations that can e.g. duplicate or erase the whole contents of some places, and/or transfer them to other places, which makes their compatibility non-strictand indeed their boundedness problem is undecidable.

III. ORDINAL RECURSIVE COMPLEXITY

The enormous complexity of some decidable problems on WSTSs requires the introduction of complexity classes spanning way beyond the usual polynomial or exponential hierarchies. The complexity classes we consider are generated by ordinal-indexed subrecursive hierarchies, like the Hardy hierarchy and the fast-growing hierarchy. See [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF] for a selfcontained presentation; we only recall below the notions and notations that are required for our construction in Section VI.

It is well-known that any ordinal α < ε 0 can be written uniquely in Cantor Normal Form (CNF). In this paper we use a dotted addition symbol " +" when we want to stress that an ordinal term is in CNF. Thus, when we write

α = ω α1 + • • • + ω αp , (1)
we mean that not only the equality (1) holds, but also that α p ≤ . . . ≤ α 1 < α, as required by CNF. (NB: we allow writing α + α when α or α is 0.) Subrecursive hierarchies are defined through assignments of fundamental sequences (λ n ) n<ω for limit ordinals λ < ε 0 , verifying λ n < λ for all x and λ = sup n λ n . A standard assignment is defined by:

γ + ω α+1 n def = γ + ω α • ω n , γ + ω λ n def = γ + ω λn , (2)
together with ω n def = n. Writing Ω for the ordinal ω ω ω ω , this yields for instance

Ω k = ω ω ω k and (Ω k ) k = ω ω ω k-1 •k .
The Hardy hierarchy (H α : N → N) α<ε0 is defined by

H 0 (n) def = n and H α+1 (n) def = H α (n + 1), H λ (n) def = H λn (n). (3)
Observe that H 1 is the successor function, and more generally H α is the αth iterate of the successor function, using diagonalisation to treat limit ordinals. The fast growing hierarchy (F α : N → N) α<ε0 can be defined by

F α def = H ω α , resulting in F 0 (n) = H 1 (n) = n + 1, F 1 (n) = H ω (n) = H n (n) = 2n, F 2 (n) = H ω 2 (n) = 2 n n
being exponential, F 3 nonelementary, and F ω an Ackermannian function.

By applying elementary closure operations to the collection of functions (F β ) β≤α along with the addition, projection and zero functions, one obtains a hierarchy (F α ) α known as the extended Grzegorczyck hierarchy [START_REF] Löb | Hierarchies of number theoretic functions, I[END_REF], which characterises several natural classes of functions; for instance F 0 = F 1 is the class of linear functions, F 2 that of elementary ones, k∈N F k of primitive-recursive ones, and k∈N F ω k of multiply-recursive ones. The hierarchy is strict for all 0 < α < α :

F α F α , in particular because F α ∈ F α .
The (F α ) α hierarchy provides a more abstract packaging of the main stops in the extended Grzegorczyk hierarchy and requires lighter notation than the Hardy hierarchy (H α ) α . However, with its tail-recursive definition, the Hardy hierarchy is easier to implement as a while-program or as a counter machine. Below we weakly implement Hardy computations with PDNs. Formally, a (forward) Hardy computation is a sequence α

0 , n 0 - → α 1 , n 1 - → α 2 , n 2 - → • • • - → α , n of evaluation steps implementing Eq. (3) seen as left-to-right rewrite rules. It guarantees α 0 > α 1 > α 2 > • • • and n 0 ≤ n 1 ≤ n 2 ≤ • • • and keeps H αi (n i ) invariant.
We say it is complete when α = 0 and then n = H α0 (n 0 ) (we also consider incomplete computations). A backward Hardy computation is obtained by using Eq. ( 3) as right-to-left rules. For instance, Ω, k → Ω k , k → (Ω k ) k , k constitute the first three steps of the forward Hardy computation starting from Ω, k if k > 0.

IV. COMPLEXITY UPPER BOUNDS

A key insight for the complexity analysis of WSTS algorithms is that the use of wqos yields not only algorithm termination, but also upper complexity bounds: Theorem 3 (Upper Bound). Coverability and termination for PDNs, DNs, TPNs, and CMRSs, are in F ω ω ω n + O [START_REF] Abdulla | A classification of the expressive power of well-structured transition systems[END_REF] .

For this result, as explained in [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's Lemma[END_REF][START_REF] Schmitz | Multiply-recursive bounds with Higman's Lemma[END_REF], we merely need to find out [START_REF] Abdulla | A classification of the expressive power of well-structured transition systems[END_REF] what is the complexity of a step of the WSTS (in the case of PDNs, transitions perform simple affine operations in F 1 ), and (2) the maximal order type of the wqo, which is a measure of its complexity (this is Ω k for a k-PDN). By the length function theorem for elementary wqos (see full version of [START_REF] Schmitz | Multiply-recursive bounds with Higman's Lemma[END_REF]), we then obtain a parameterised upper bound in F ω ω k for the decision problems of k-PDNs mentioned in Section II-B, and a uniform F ω ω ω upper bound (which asymptotically majorises every function in k F ω ω k ) when the dimension is not fixed.

These upper bounds hold more generally for k-DNs, as they have the same order type and their extra whole-place operations are still in F 1 . Regarding TPNs and CMRSs, the F ω ω ω upper bound also holds; however here the main parameter in the parameterised complexity-which appears as the exponent on top of the tower of ω's-is not simply the dimension k but km where m is the maximal constant that appears in the constraints put on transitions or in the initial marking.

V. COMPLEXITY LOWER BOUNDS

We now describe the proof plan for our main result.

Theorem 4 (Lower Bound). Coverability and termination for PDNs are F ω ω ω -hard.

This follows from a reduction from the halting problem for Minsky machines (MM) M with counters bounded by F ω ω ω (|M |). The proof is done by assembling two constructions (described in the following sections). The schematics (see Fig. 1) are similar to earlier constructions for lossy channel systems or counter machines and the reader can refer to [START_REF] Ph | Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets[END_REF][START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF] where more lower-level details are given. We outline it as a motivation for the following sections. 1) Direct Computation: For a provided size k, we first construct (see Section VII) a PDN N H [k] initialised with a pair α 0 , n

N H [k] =(Ω k ) k ,k α 0 , n 0 r -→ • • • r -→ α i , n i r -→ • • • r -→ α ℓ , ≤H α 0 (n0) n ℓ p start p rewr p halt t rewr N H -1 [k] 0, m 0 r -→ -1 • • • r -→ -1 α, n p ′′ start p ′′ rewr p ′′ halt t ′′ rewr N M p ′ start p ′ halt simulate M using cpt as a budget cpt c M 1 c M r
0 def = (Ω k ) k , k and that tries to rewrite it α 0 , n 0 - → α 1 , n 1 - → • • • - → α
, n in a way that reflects precisely the complete Hardy derivation issuing from α 0 , n 0 , thus computing n = H α0 (n 0 ) = H Ω (k). There are two difficulties here. First, one has to encode ordinals in sequences of vectors (i.e. in PDN configurations) and this is the topic of Section VI. Secondly, our PDN only performs Hardy computations in a weak sense. What is guaranteed is the following:

Lemma 5 (See Section VII). N H [k] is "complete": Starting with α 0 = (Ω k ) k , N H [k]
can perform the exact Hardy computation and halt with α = 0 and n = H Ω (k). N H [k] is "safe": Any halting computation in N H [k], correct or incorrect, has n ≤ H Ω (k).

2) Simulation: Now consider some MM M of size k. An easy (see [11, §7]

: if M halts, n f = n is indeed feasible).
3) Inverse Computation: We now connect N H [k], N M and N H -1 [k] so that they run sequentially. Here N H -1 [k] is a PDN for backward Hardy computations. It starts with α 0 = 0 and m 0 = n f (passed on by N M ). Its backward computation may reach (Ω k ) k , k if m 0 = H Ω (k). Here too, the PDN only computes H -1 in a weak sense but it is guaranteed that it can do exact backward computations (completeness) and that incorrect backward computations halting on (Ω k ) k , n have

H (Ω k ) k (n) ≤ m 0 (safety).
As a consequence, the resulting full PDN started with (Ω k ) k , k can reach a configuration with p halt and a pair α, n that covers (Ω k ) k , k (in terms of the places that store the current Hardy pair) if, and only if, the Minsky machine M with space bounded by H Ω (k) = F ω ω ω (k) halts.

Indeed, if M halts within the space bound, the PDN may reach the required p halt , α, n by chaining exact Hardy computations and the simulation of M by N M . More interestingly, if the required α, n is reached, we know, letting

h def = H Ω (k), that n ≤ h (safety of N H ), that n ≥ n f = m 0 (budget of N M ), that H α (n) ≤ m 0 (safety of N H -1 ), and that H α (n) ≥ h (α, n covers (Ω k ) k , k). Thus h ≤ H α (n) ≤ m 0 = n f ≤ n ≤ h.
Necessarily n = n f , witnessing that M halts, and n = h, witnessing that M runs in space bounded by h = F ω ω ω (k).

In conclusion, the construction provides a (logspace) manyone reduction from the halting problem for Minsky machines running in space bounded by F ω ω ω (k) where k = |M | is the size of the MM description. Using standard complexitytheoretical arguments, Theorem 4 (for Coverability) follows.

4) Termination: Regarding termination, a similar reduction works. One makes sure that N H [k] always halts or deadlocks (it does) and stores two copies of n : one is a time budget that ensures the eventual halting-or-deadlock of N M , and the other witnesses n f = n as earlier. In the end, the whole system has to eventually stop, unless it can cover (Ω k ) k , k with α, n, finally enabling an infinite loop. This reduces the same MM problem to termination for PDNs. More details can be found in [23, §7] where the same adaptation is done.

Using the simulations of PDNs by TPNs of [START_REF] Bonnet | Comparing Petri Data Nets and Timed Petri Nets[END_REF] and of DNs by CMRSs of [1, §5], we conclude: Corollary 6. Coverability and Termination for TPNs, DNs, and CMRSs are F ω ω ω -hard.

VI. ENCODING HARDY COMPUTATIONS

We define in this section a so-called "cumulative" encoding of ordinals as codes (Section VI-A) and a rewriting system r -→ operating on codes that performs Hardy computations (Section VI-B). Its crucial property is its robustness, which entails that weak implementations, like the PDN implementation we present in Section VII, are correct (see Section VI-C).

A. Encoding Ordinals as Cumulative Vector Sequences

Fix k ∈ N. An ordinal < ω k is "small" and we use β, β , . . . to denote small ordinals; an ordinal < ω ω k is "medium" and we use α, α , . . . for such ordinals; finally, an ordinal < Ω k is "large" and we use π, π , . . . for such ordinals. A medium ordinal can be written in CNF as α = ω β1 + • • • + ω βp where β 1 , . . . , β p are small ordinals, and a large ordinal can be written as π = ω α1 + • • • + ω αm where α 1 , . . . , α m are medium ordinals.

We now introduce an encoding of large ordinals that will allow the computation of the Hardy functions with PDNs. These data structures are 1) k-dimensional vectors in N k for small ordinals, 2) vector sequences in (N k ) * for medium ordinals, and 3) cumulative encodings in (N k {#}) * for large ordinals, where # is a fresh tally symbol.

1) Small Ordinals as Vectors

: For v ∈ N k and an index 0 ≤ i < k, let v[i] ∈ N denote the i-th component of v.
We use two different orderings over N k : the product ordering, denoted v ≤ v and the lexicographic ordering, denoted v ≤ lex v , with most significant component at index k -1. Recall that ≤ is a wqo, and that ≤ lex is a linearization of ≤.

With a vector v ∈ N k , we associate the small ordinal

β(v) def = ω k-1 • v[k -1] + • • • + ω 0 • v[0] . (4)
This establishes a bijective correspondence between N k and small ordinals, and we write v(β) for β -1 (β). We write 1 i for the vector with v[i] = 1 and v[j] = 0 for all j = i. Hence

β(0) = 0 and β(1 i ) = ω i .
The bijection relates the two linear orderings of small ordinals and of vectors in

N k since v ≤ lex v iff β(v) ≤ β(v ) . (5)
2) Medium Ordinals as Vector Sequences: With a finite sequence

V = v 1 v 2 • • • v p ∈ N k * , we associate the ordinal α(V) = α(v 1 v 2 • • • v p ) def = ω β(v1) + • • • + ω β(vp) . (6) This surjective 1 embedding of N k * into ω ω k satisfies α(VV ) = α(V) + α(V ). Write ε for the empty sequence in N k * . Then α(V) = 0 iff V = ε, and α(V) = 1 iff V = 0. Example 7. Consider k = 2: α(1 0 ) = α(| 0 1 ) = ω β(10) = ω ω 0 •1 = ω 1 = ω, thus α(| 0 1 | 0 1 ) = ω • 2, while α(2 × 1 0 ) = α(| 0 2 ) = ω ω 0 •2 = ω 2 .
We order vector sequences with ≤ * , the sequence extension of ≤: it is a wqo since ≤ is.

We

say that V = v 1 • • • v p is pure if v 1 ≥ lex v 2 ≥ lex • • • ≥ lex v p
: restricted to pure vector sequences, the embedding in ( 6) is bijective since the expression giving α(V) in Eq. ( 6) is in CNF. We write pure(V) for the only pure V such that α(V) = α(V ): one obtains pure(V) by removing in

V = v 1 • • • v p any v i such that v i < lex v j for some j > i. Hence pure(V) ≤ * V.
3) Cumulative Encodings for Large Ordinals: Fix a special tally symbol # and let N k

# def = N k ∪{#}. A cumulative ordinal description, or simple a "code", is a sequence x in N k # * . Below we see them as sequences in [N k * #] * N k * , i.e.
we single out the tally symbols and factor codes under the form

x = V 1 #V 2 # • • • #V m #V rest , (7)
where the V i 's are vector sequences. We extend ≤ * from vector sequences to codes in the natural way, by requiring that a # embeds into a #: this is still a wqo. With x we associate a large ordinal π(x) via the following

π(V 1 #V 2 # • • • #V m #V rest ) def = ω α(V1V2•••Vm) + • • • + ω α(V1V2) + ω α(V1) . (8)
The above definition explains why codes are called cumulative. One can also define π inductively by

π(V) = 0 , π(V#x) = ω α(V) • π(x) + ω α(V) . (9)
We say that x is pure if each V i , i = 1, . . . , m, is pure, and if in addition

V rest = ε. (NB: purity of, e.g., V 1 #V 2 #, does not guarantee purity of V 1 V 2 .
) For a code x, the unique pure x such that π(x) = π(x ), denoted x = pure(x), is given by

pure(V 1 #V 2 # • • • #V m #V rest ) = pure(V 1 )#pure(V 2 )# • • • #pure(V m )#ε . ( 10
) Lemma 8. x ≤ * x implies pure(x) ≤ * pure(x ).
Lemma 9 (Bijection). Pure codes in N k # * and large ordinals in Ω k are in bijection by π.

ω β(v ) = α(v ) = ω β(v ) + ω β(v) .
If we write V (x) for the vector sequence obtained by removing all tally symbols from x, i.e. the result of the projection # → ε applied to x, then

π(x 1 #x 2 ) = π(pure(V (x 1 )x 2 )) + π(x 1 #) . (11)
Example 10. Let k > 1; the initial Hardy computation step x 0 , k → x 1 , k with pure codes x 0 , x 1 is defined by

x 0 def = (1 k-1 ) k # ; π(x 0 ) = (Ω k ) k ; x 1 def = (1 k-1 ) k-1 (1 k-2 ) k # ; π(x 1 ) = ω ω ω k-1 •(k-1)+ω k-2 •k .

B. Rewriting of Ordinal Codes

Let us turn to the encoding of Hardy computations (below Ω k ) as rewriting rules on codes. Such a system should e.g. map x 0 to x 1 in Example 10. It turns out that the bulk of the task when computing Hardy functions lies in computing the elements in the fundamental sequences of limit ordinals.

1) Limit Ordinals: Observe that a code denotes a successor ordinal if it is of the form #x, as indeed Vv) ) n . We want to define a similar mapping (.) n from codes to codes s.t. π (x) n = π(x) n ; this mapping essentially needs to treat the head Vv, which contributes the smallest term ω α(Vv) to the encoded ordinal. Several cases arise depending on v:

π(#x) = ω 0 • π(x) + ω 0 = π(x) + 1. Conversely, a pure code of form Vv#x denotes a limit ordinal π(Vvx) + ω α(Vv) s.t. π(Vv#x) n = π(Vvx) + (ω α(
• if v = 0, i.e. ω β(v) = 1, then ω α(V0) = ω α(V)+1 verifies (ω α(V0) ) n = ω α(V) • n, encoded through (V0) n def = V# n . ( 12
)
Thus we verify

π (V0#x) n def = π(V# n 0x) (13) = π(V0x) + ω α(V) • n = π(V0#x) n . • if v = 0 then (ω α(Vv) ) n = ω α(V) +(ω β(v) )n (recall that Vv is pure) is encoded by (Vv) n def = V(v) n # , (14)
and we need to further distinguish two cases: let i ∈ {0, . . . , k -1} be the smallest index with v[i] > 0. Then β(v) is a successor ordinal if i = 0 and a limit ordinal otherwise, hence the definition

(v) n def = (v -1 0 ) n if i = 0, v -1 i + n • 1 i-1 otherwise. ( 15
)
Since every vector in the sequence (v) n is < lex v, this verifies

π (Vv#x) n def = π(V(v) n #vx) (16) = π(V(v) n vx) + ω α(Vv) n = π(Vvx) + ω α(Vv)
n . The definitions [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF][START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's Lemma[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF][START_REF] Finkel | A wellstructured framework for analysing Petri nets extensions[END_REF][START_REF] Friedman | Some decision problems of enormous complexity[END_REF] thus result for a pure Vv in

π (Vv#x) n = π (Vv) n vx = π(Vv#x) n . (17)
2) Rewriting System: We define a set of rewriting rules r -→ working on pairs (x, n) of a code x and a number n ∈ N, that together encode an intermediate stage H π(x) (n) in the course of a Hardy computation.

Definition 11 ( r - →). The relation x, n r - → y, m is given by rules (R1-R2) below. #x, n r - → x, n + 1 (R1) Vv#x, n r - →          (Vv) n x, n if x = ε or x = v x with v < lex v (Vv) n vx, n if x = #x or x = v x with v ≤ lex v (R2)
Rule (R2) implements the case of limit ordinals and is correct by ( 17)-the first subcase includes a purification step when π((Vv) n vx) = π((Vv) n x)-while rule (R1) handles successor ordinals:

Proposition 12 (Correctness of r - →). x, n r - → y, m and x pure imply H π(x) (n) = H π(y) (m). Remark 13 (Purity is required). A step x, n r - → y, m is not always correct when x is not pure: e.g. if k = 1, π(01#) = ω + ω ω = ω ω but 01#, n r - → 0 n+1 #, n, which encodes ω n+1 , and H ω ω (n) = H ω n (n) < H ω n+1 (n).
It is convenient to work with pure codes in proofs: the oneto-one correspondence between pure codes and ordinals in Ω k yields a one-to-one correspondence between a pair (x, n) and a snapshot of a Hardy computation H π(x) (n), allowing to transfer results from Hardy computations to r -→. More importantly, note that Proposition 12 entails the correctness of r -→ even when applied backwards: we capture both forward and backward Hardy computations with the same rewriting system.

C. Robustness of r -→ So far, our encoding of ordinals in Ω k and the rewriting system r -→ can be seen as a (rather convoluted) way of performing forward and backward Hardy computations using sequences of vectors. Their critical interest compared to more basic ordinal encodings is that r -→ is robust: if instead of computing with x, n we first decrease the configuration in an uncontrolled way to some y, m with y ≤ * x and m ≤ n, we obtain a configuration that codes a smaller value H π(y) (m) ≤ H π(x) (n). This result is subject to hygienic conditions on x, n and y, m; see Proposition 16 for the exact statement.

Remark 14 (Non-Robustness of CNF). Let us pause for a moment and consider a natural encoding χ of large ordinals. In this encoding, we use the CNF of the ordinal and separate pure vector sequences with " +" symbols s.t. Vm) ; e.g. p = 1 +0 codes χ(p) = ω ω +ω for k = 1. However, q = 10 verifies q ≤ * p and codes the much larger ordinal χ(q) = ω ω+1 , with

χ(V 1 + • • • + V m ) def = ω α(V1) +• • • +ω α(
H χ(p) (n) = H ω ω +ω (n) < H ω ω •(n-1) +ω n (n) = H χ(q) (n) when n > 0.
By contrast, with cumulative codes, "losing" a tally symbol results in the loss of a summand in the corresponding ordinal, which immediately leads to smaller Hardy values. a) Trim Codes: We introduce a restriction on codes that allows to ensure that r -→ behaves as expected, especially when performing backward computations: a pure code x is n-trim if, for any vector v occurring in x, there exists 0

≤ i < k s.t. v[i] ≤ n and for all 0 ≤ j < i, v[j] = 0 and all i < j < k, v[j] ≤ n -1 (this restricts the ordinal β(v)). A configuration x, n of r - → is trim if x is n-trim, and a computation x 0 , n 0 r -→ x 1 , n 1 r -→ • • • r -→ x m , n m is trim if every configuration x i , n i is trim. Write x , n trim --→ x, n if x ≤ * x
- → ∩ {x, n | x, n is trim} 2 ).
The next proposition states the key monotonicity property of trim computations: Proposition 16 (Robustness). Let x, x be pure codes and n > 0. If x is n -trim and x, n ≤ * x , n , then

H π(x) (n) ≤ H π(x ) (n ).
b) Weak Implementations: The efforts put into defining a robust computation for the Hardy functions pay when one tries to implement them in a "weak" model like PDNs, as we do in Section VII-but this could also be used in other models. By a weak implementation, we mean-as usual in the Petri net literature-an implementation that guarantees 1) completeness: it includes the desired behaviour, and 2) safety: it might also yield "smaller" results. In the case at hand, we provide sufficient conditions (see Definition 18) for two relations . The conditions will be easy to check on the actual implementation by PDNs of Section VII, and they entail:

Theorem 17 (Weak Implementations). If d - → is a weakening of r - → and b - → a weakening of r - → -1 , then 1) For any n 0 -trim x 0 , x 0 , n 0 d - → * ε, H π(x0) (n 0 ) and ε, H π(x0) (n 0 ) b - → * x 0 , n 0 . 2) If x 0 is n 0 -trim and x 0 , n 0 d - → * ε, n then n ≤ H π(x0) (n 0 ),
and if ε, m b - → * x, n, then H π(x) (n) ≤ m.
Note that these are exactly the two properties required in the main proof of Section V from the PDNs N H

[k] and N H -1 [k].
Here are our sufficient conditions:

Definition 18 (Weakenings). A relation d - → on codes is a weakening of r - → if rt - → ⊆ d - → ⊆ ≥ * ; trim --→; rt - →; ≥ * ; trim --→. Similarly, a relation b - → is a weakening of r - → -1 if rt - → -1 ⊆ b - → ⊆ ≥ * ; trim --→; rt - → -1 ; ≥ * ; trim --→.
Proof of Theorem 17: For (1), by Lemma 15, for an n 0 -trim

x 0 , x 0 , n 0 r - → * ε, H π(x0) (n) implies x 0 , n 0 rt - → * ε, H π(x0) (n) and ε, H π(x0) (n) ( rt - → -1 ) * x 0 , n 0 since ε is H π(x0) (n) -trim.
For (2), we reconstruct step by step pieces of a computation of

rt - → or rt - → -1 . For d - →, if x, n is trim and x, n ≥ * x , n trim --→ x , n rt - → y , m ≥ * y , m trim --→ y, m, then H π(x) (n) ≥ H π(x ) (n ) (by Prop. 16) = H π(y ) (
--→ y , m rt - → -1 x , n ≥ * x , n trim --→ x, n, then H π(y) (m) ≥ H π(y ) (m ) (by Prop. 16) = H π(x ) (n ) (by Prop. 12) ≥ H π(x) (n) , (by Prop. 16)
and we proceed again by induction.

VII. PETRI DATA NET IMPLEMENTATION

We explain in this section how to construct N H and N H -1 , the PDNs that we announced and used in Section V. They transform pairs x, n via a relation What makes PDNs relatively powerful is that they can make weak copies of a counter and even of a sequence, and they can use these weak copies for bounding the number of times a loop is executed ("weak control"). We designed codes and robustness precisely to fit this weak computational power.

In the rest of this section we explain how codes are represented in a PDN (Section VII-A) and how to perform trimming. Due to lack of space, the definitions and the implementation of

1) Counter:

The counter n is represented via two places cpt and cpt.id. Place cpt.id is an identity place for relevant tokens: the current value of the counter will be the number of tokens in cpt whose identity match cpt.id.

2) Code: For a code x of length l, distinct identities I 1 < . . . < I l identify each item in x. Every item of the code is identified by a unique identity, and the ordering of identities lets one recover the code. All the identities that have been used for items of the current and past codes are stored in two places, vect and tally, letting one distinguish between vector and # occurrences in x; note that each # occurrence has a different identity. The representation of a vector v identified by some I in a code is done via places c 0 , . . . , c k-1 : v[i] is the number of tokens in c i with identity I.

Identities evolve during a computation. In order to prevent tokens with now irrelevant identities from disturbing the computation, N H uses two identity places, low and high. We make sure that at any time each of these two places contains a single token, and we just write low or high to denote the identity carried by that single token. Initially, one has cpt.id < low < high and the identities I 1 , . . . , I l for the (current) code are exactly those with low < I < high; other identities are irrelevant for x.

When simulating an r -→ step (and except in simple cases), cpt.id is decreased, high is increased and low is set to the previous value of high. Thus tokens with (now) irrelevant identities will never match the current value of cpt.id nor belong to the open interval (low, high).

B. Counter Duplication

In most cases, r -→ requires that we iterate some operation at most n times (or n-1, or ...) where n is the current value of the counter. In N H this is systematically done in a modular way by first duplicating the counter and then consuming the tokens of the duplicate, thus controlling the number of iterations.

For this, N H uses two places, dpt and dpt.id, where it stores duplicates of the tokens in cpt and cpt.id. The net of Fig. 2 depicts the duplication. 2 Transition dp 1 performs the identity updating: cpt.id acquires a smaller identity C < C while dpt.id is updated with the previous identity of cpt.id, namely C. Then transition dp 2 transfers the tokens of cpt (corresponding to the previous identity of the counter D) both to the original counter and to the duplicated counter. Transition 2 We rely on the standard graphical depiction of enriched nets and use (pictures of) Petri nets where arcs connected to a transition t are labelled with bags of variables that must be instantiated by ordered identities. The number of these variables is exactly |cons(t)| and the ordering of the corresponding identities is carried by the transition. For concision and readability, it is convenient to allow orderings of the variables that are not total: this stands for all possible linearizations. We also use graphical conventions for better readability: control places containing black tokens are greyed or filled somehow, identity places containing at most one token per identity are represented by simple circles, and the other places, used for counters or general storage, are represented by double circles. dp 3 stops the process, and is slightly modified if we need to put n-1 rather than n in dpt. (In order to avoid a special case for the first duplication, the initial marking has dpt empty and dpt.id with the same identity as cpt.id.)

This simple mechanism must be refined for the loops in the trimming process (see below) where the value of n is used to control that every component of a vector in the code is ≤ (some value related to) n. Here one cannot just iterate the previous mechanism: since every duplication possibly decreases n and could violate the property already established for previous components. A more elaborate implementation is required: N H uses a second auxiliary counter ept and ept.id (initialised using dpt and dpt.id) for such multiple controls (as in Fig. 3). In order to avoid a clash of identities for counters, at every initialisation of ept, the new identity of dpt.id, namely D is selected by the guard C < D < D where D and C are the current identities of dpt.id and cpt.

C. Weak Trimming

During most weak rule applications, a trimming is performed on-the-fly while the exact rule is simulated, i.e. we actually weakly implement rt -→ and its inverse. This trimming consists in implementing ≥ * ; trim --→ during the selection and copy of the rule left-hand side and is simultaneously ensured from the rule right-hand side: it turns a configuration t, n into another one t , n ≤ * t, n which is trim and pure.

• N H first duplicates the counter cpt, yielding a new value n ≤ n (see Fig. 2). Below we assume that this stage is already passed.

• N H scans (in increasing order) relevant identities (the ones in vect or sharp, between low and high), purifies the code and copies it beyond high as we explain.

• It purifies, one at a time, sequences separated by #s.

• When copying a vector sequence, the first vector is copied but also duplicated in auxiliary places d 0 , . . . , d k-1 interpreted as the c i 's. The remaining vectors are also copied and duplicated. Purity is enforced by checking that any (copy of a) vector is lexicographically below the previous vector, as stored in d 0 , . . . , d k-1 .

• Finally, both vectors should fulfil the trimming constraint: for some i < k, v[i] ≤ n, and v[j] < n when j > i, and v[j] = 0 when j < i.

1) Controlling Trimming:

Let us detail how this is controlled. N H uses three additional identity places: from, to and with. The current item's identity is from, its copy after trimming has the new identity to, and the purification of a vector requires comparisons with the previous vector in the sequence, whose identity is recorded in with, letting one select the appropriate tokens in d 0 , . . . , d k-1 . Fig. 4 describes the overall control of this process, started by beg.pur, looping, and concluded by end.pur. The body of the loop copies one vector sequence followed by a #. If non empty, the sequence has just one vector, or more, requiring two different treatments. For readability, the labeling of the crucial transitions is specified in the lower part of the picture:

• At start, beg.pur produces identity tokens in from and to within the appropriate intervals (wrt. low and high), guessing the identity of an item to be copied.

• When the treatment ends, end.pur updates low and high to their new value. • After copying the first vector, efirst guesses a new identity (to be copied) in from and a new (target) identity in to, while recording the current identity in with.

• After copying a remaining vector, erem guesses fresh identities from and to, and updates the recorded identity in with.

• csharp copies a # symbol, consuming a token in sharp with identity from and producing a token with identity to (while updating from and to as usual). Observe that a bad guess in from can lead to deadlock but no infinite looping is possible (as required by the proof of Theorem 4).

2) Copy of a Vector Sequence: a) First Vector: First, in order to guarantee a trim representation, the copy of the first vector non deterministically selects a component i, which is allowed to be less than or equal to n. The rest of the process is depicted in Fig. 3. It consists for j > i in:

• setting the auxiliary counter ept to dpt;

• "updating" tokens in place c j from identity F to identity n, and at the same time in memorising the transferred tokens in place d j for j > i. With the help of the counter ept, at most n -1 tokens are transferred. This is performed by transition ts j . We then perform the same transfer for component i, but allow one more token thanks to the firing of transition ts i . No token is transferred for any component j < i.

b) Remaining Vectors: For the sake of readability, we do not represent the management of trimming, which is performed as with the first vector, but rather focus on the purity of the vector sequence.

Let us call v the vector to be copied (identified by variable F), v the last vector that has been copied (identified by W) and v ≤ v the vector to be copied (identified by T). In order for v to be lexicographically smaller than v it must satisfy:

• either for all i, v (i) ≤ v (i) • or there exists some i s.t. for all j > i, v (i) ≤ v (i) and v (i) ≤ v (i) -1. Then the simulation non deterministically selects one of these cases. The purity check is thus largely similar to the trimming one: copying is limited by some values, depending on W and cpt.

Observe that one of the possible results of weak trimming is (exact) trimming of the code, and that the other ones are trimmings of a weaker code.

VIII. ON WELL-STRUCTURED LANGUAGES

Well-structured transition systems can be seen as language acceptors (or generators). For M a class of WSTS models, e.g. M = the Data Nets, let L(M) be the class {L(M ) | M ∈ M} of languages (nondeterministically) accepted by systems in M when their transitions carry labels, possibly ε, over some alphabet, and when the set of "final", or "accepting", states is upward-closed. Geeraerts et al. [START_REF] Geeraerts | Wellstructured languages[END_REF] shows convincingly that this notion of well-structured languages (WSL), also called coverability languages, is most relevant.

A series of recent papers (see [START_REF] Geeraerts | Wellstructured languages[END_REF][START_REF] Abdulla | A classification of the expressive power of well-structured transition systems[END_REF][START_REF]Ordinal theory for expressiveness of well structured transition systems[END_REF] and the references therein) successfully use WSLs as a tool for comparing the descriptive power of varied WSTS models, showing equivalence, e.g. of PDNs and TPNs, or, separating them from the less expressive LCSs (lossy channel systems) or APNs (affine Petri nets [START_REF] Finkel | A wellstructured framework for analysing Petri nets extensions[END_REF]).

It turns out that the simulation we develop in this paper (and the matching complexity upper bounds) leads to a (relative but) precise characterisation: Let L 0 = {w# n | n = |w|} collect all words (over a two-letter alphabet) equipped with a length witness:

L 0 ⊆ (a + b) * # * is deterministic context-free. Theorem 19. 1) L ∈ L(PDN)(= L(TPN) = L(DN)) implies L ∈ k∈N TIME(F ω ω k (n)). 2) L ∈ k∈N TIME(F ω ω k (n)) implies L ∩ L 0 ∈ L(PDN).
The proof relies on the possibility of simulating a spacebounded MM. Using the simulations in [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF][START_REF] Ph | Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets[END_REF] and the upper bounds in [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's Lemma[END_REF][START_REF] Schmitz | Multiply-recursive bounds with Higman's Lemma[END_REF] we derive in a similar way: to nets with at most k places (resp., to channel systems with a k-letter internal message alphabet). These first separation results are not stronger than those of [START_REF] Abdulla | A classification of the expressive power of well-structured transition systems[END_REF][START_REF]Ordinal theory for expressiveness of well structured transition systems[END_REF], but they provide a standard measure (using Turing, or equivalently Minsky, machines) rather than a myriad of relative ones.

Theorem 20. For any L ⊆ L 0 : 1) L ∈ k∈N TIME(F ω k (n)) iff L ∈ L(LCS). 2) L ∈ k∈N TIME(F k (n)) iff L ∈ L(APN).

IX. CONCLUDING REMARKS

Theorems 3 and 4 close the open question of the complexity of decision problems over the family of "enriched" nets (our terminology), and have immediate consequences, e.g. for separating various WSTS models according to their computational power. Interestingly, we are not aware of any other natural decision problem sitting exactly at level F ω ω ω [START_REF] Friedman | Some decision problems of enormous complexity[END_REF], which makes of enriched net problems the canonical examples for this complexity class.

Our main technical contribution is the robust encoding in (N k * , ≤ * ) of ordinals in Ω k , together with rewrite rules that describe Hardy computations. Enriched nets are not the only computational model in which these rules can be weakly implemented, and one may use them for proving complexity lower bounds in other settings.

Finally, let us mention two questions raised by this work: 1) Can one improve on Theorem 20? We would prefer an exact characterisation of L(PDN), not relatively to L 0 . 2) What about ν-Petri nets [START_REF] Rosa-Velardo | Decidability and complexity of Petri nets with unordered data[END_REF] and unordered PDNs? The underlying wqo is simpler than N k * , hence we expect lower complexities.

n ≤ H α (n) , (18)
n < m implies H α (n) ≤ H α (m) . (19)
However, the Hardy functions are not monotone in the ordinal parameter:

H n+1 (n) = 2n + 1 > 2n = H n (n) = H ω (n),
though n + 1 < ω. We will introduce two ordinal orderings in Section A2 and Section A4 that ensure monotonicity of the Hardy functions.

Another handful fact is that we can decompose Hardy computations:

Fact 22 (see e.g. 22, Lemma C.7). For all α, γ in Ω, and x,

H γ +α (x) = H γ (H α (x)) . ( 20
)
2) Pointwise Ordering: The classical "pointwise at n" ordering used e.g. in [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF] and [22, Appendix C] is defined for any n ∈ N as the smallest transitive relation ≺ n s.t.

α ≺ n α + 1 , λ n ≺ n λ . (21)
inductive definition of ≺ n implies α ≺ n α iff α = β + 1 is a successor and α n β, or α = λ is a limit and α n λ n . This can be understood a "descent" through ordinals, eventually reaching predecessor ordinals, which are defined by

P n (α + 1) def = α , P n (λ) def = P n (λ n ) , (22)
and indeed

0 n α , P n (α) ≺ n α .
The interesting observation here is that the ordinals that appear in a Hardy computation α 0 , n → α 1 , n → • • • → α , n where n remains constant, i.e. no successor steps are used, are all related by ≺ n :

α 0 ≺ n α 1 ≺ n • • • ≺ n α .
The first successor step will occur with P n (α 0 ) + 1, n → P n (α 0 ), n + 1.

Obviously ≺ n is a restriction of <, the linear ordering of ordinals. For example, n = ω n ≺ n ω but n + 1 ≺ n ω. The ≺ n relations are linearly ordered themselves, and <, can be recovered in view of [see 22, Appendix C.2]:

≺ 0 ⊂ • • • ⊂ ≺ n ⊂ ≺ n+1 ⊂ • • • ⊂ n∈N ≺ n = < . (23)
Fact 23 (Congruence, see 22, Lemma C.2). For all α, α , γ and all n > 0

α ≺ n α implies γ + α ≺ n γ + α , ( 24
) α ≺ n α implies ω α ≺ n ω α . ( 25
)
Fact 24 (Monotonicity, see e.g. 22, Lemma C.9). For all α, α and n, m,

α ≺ n α implies H α (n) ≤ H α (n) . ( 26
)
Since F α = H ω α , the same statement holds for F using (25).

3) Almost Lean Ordinals: Leanness is a norm on ordinal terms used extensively in [START_REF] Schmitz | Multiply-recursive bounds with Higman's Lemma[END_REF]: Let n be in N. We say that an ordinal α < ε 0 is n-lean if it only uses coefficients < n, or, more formally, when it is written under the strict CNF

α = ω β1 • c 1 + • • • + ω βm • c m with β 1 > • • • > β m ,
α = ω β1 • c 1 + • • • + ω βm • c m be an ordinal in CNF with α > β 1 > • • • > β m and ω > c 1 , . . . , c m > 0.
We say that α is almost n-lean if either (i) c m ≤ n and both i<m ω βi and β m are n-lean, or (ii) c m ≤ n, i<m ω βi is n-lean, and β m is almost n-lean. An almost n-lean ordinal is not necessarily n-lean, but an n-lean ordinal is always almost n-lean.

The interest of almost n-leanness is that it is an invariant of the ordinals appearing during forward Hardy computations. As the initial ordinal of ( 10) is almost k-lean, this property is preserved by perfect computations. Lemma 25. If a limit ordinal λ is n-lean, then λ n is almost n-lean.

Proof: By induction on λ, letting λ = ω β1 • c 1 + • • • + ω βm • c m as above. If β m is a successor ordinal β + 1 (thus β is n-lean), λ n = ω β1 • c 1 + • • • + ω βm • (c m -1) + ω β • n is almost n-lean. If β m is a limit ordinal, λ n = ω β1 • c 1 + • • • + ω βm • (c m -1) + ω (βm)n
= ω β1 • c 1 + • • • + ω βm • (c m -1) is n-lean. The converse implication is immediate. Lemma 27. If a limit ordinal λ is almost n-lean then λ n is almost n-lean. Proof: We proceed by induction on λ, letting λ = ω β1 • c 1 + • • • + ω βm • c m as above. If β m is a successor ordinal β + 1, λ n = ω β1 • c 1 + • • • + ω βm •(c m -1)+ω β •n,
and either (i) c m ≤ n and β m is n-lean, and then λ n also verifies (i), or (ii) c m < n and β + 1 is almost n-lean and thus β is n-lean by Lemma 26, and λ n is again almost n-lean verifying condition (i). If β m is a limit ordinal, then The following lemma relates leanness, the pointwise ordering, and the linear ordinal ordering; this is a refinement of [START_REF] Schmitz | Multiply-recursive bounds with Higman's Lemma[END_REF]Lemma B.1], as it handles the almost n-lean case instead of the n-lean one: Lemma 28. Let α be almost n-lean. Then α < α iff α ≺ n α .

λ n = ω β1 • c 1 + • • • + ω βm • (c m -1) + ω (βm)n . Either (i) c m ≤ n
Proof: If α = 0, we are done so we assume α > 0 and hence n > 0,

thus α = ω β1 • c 1 + • • • + ω βm • c m in CNF with m > 0.
We prove the claim by induction on α , considering two cases:

1

) if α = α + 1 is a successor then α < α implies α ≤ α , hence α ih n α ≺ n α .
2) if α is a limit, we claim that α ≤ α n , from which we deduce α ih n α n ≺ n α . We prove the claim by induction and considering three subcases on α : a) if α = ω λ with λ a limit, then α < α implies

β 1 < λ, hence β 1 ≤ λ n by ind. hyp., applicable since β 1 is also almost n-lean. Thus α ≤ ω λn = (ω λ ) n = α n . b) if α = ω β+1 then α < α implies β 1 < β + 1, hence β 1 ≤ β. Now, since α is almost n-lean, either i) c 1 = n and m = 1, hence α = ω β1 • n ≤ ω β • n = (ω β+1 ) n = α n , or ii) c 1 < n, hence α < ω β1 • n ≤ ω β • n = (ω β+1 ) n = α n . c) if α = γ + ω β with 0 < γ, β, then either α ≤ γ,
hence α < γ + (ω β ) n = α n , or α > γ, and then α can be written as α = γ + γ with γ < ω β .

In that case γ ≤ (ω β ) n by ind. hyp., applicable since γ is also almost n-lean.

Thus α = γ + γ ≤ γ + (ω β ) n = (γ + ω β ) n = α n .
4) Embedding Ordering: We introduce a partial ordering o on ordinals, called embedding, and which can be seen as a tree embedding on CNF's that respects layers. Formally, it is defined inductively as

α o β def ⇔        α = ω α1 + • • • + ω αp β = ω β1 + • • • + ω βm α 1 o β i1 ∧ • • • ∧ α p o β ip for some i 1 < i 2 < . . . < i p . (27)
Note that 0 o α for all α, that 1 o α for all α > 0. Observe that, in general, α o ω α and λ n o λ. This ordering is obviously congruent for addition and ω-exponentiation:

α o α and β o β imply α + β o α + β , (28)
α o α implies ω α o ω α , (29)
and could in fact be defined alternatively by the axiom 0 o α and the two deduction rules (28) and (29).

When considering the encoding of small ordinals described in Section VI-A-1), the following holds:

v ≤ v implies β(v) o β(v ) . (30)
The reciprocal of (30) does not hold in general, e.g.

β(1 1 ) = ω o ω 2 = β(1 2 ) while 1 1 ≤ 1 2 .
We list a few useful consequences of the definition of o :

α o γ + ω β implies α o γ or α = γ + ω β with γ o γ and β o β , (31)
n ≤ m implies λ n o λ m , (32)
α o λ implies α o λ n or α is a limit and α n o λ n . (33)
Proof: (31): Intuitively, there are two cases when we consider an embedding α o α = γ + ω β : either the ω β summand of α is in the range of the embedding or not. If it is not, then already α o γ. If it is, then α must be some γ + ω β and ω β o ω β . (32): By induction on λ:

indeed if λ = γ + ω β+1 then λ m = γ +ω β •m by (2) which is λ n +ω β •(m-n). If λ = γ +ω µ , the i.h. gives µ n o µ m , hence λ n = γ + ω µn o γ + ω µm = λ m . (33): By induction on λ. λ is some γ + ω β with β > 0 so that λ n = γ + (ω β ) n . If α o γ, then α o λ n trivially. If α = γ + 1 is a successor, 1 o (ω β ) n and again α o λ n .
There remains the case where α = γ + ω β is a limit (i.e. β > 0) with γ o γ and β o β. If β is a limit, then by i.h. either β o β n and hence α o λ n , or β is a limit and

β n o β n , hence α n o λ n . Finally, if β = δ+1 is a successor, then either β o δ so that α o γ + ω δ o γ + ω δ • n = λ n ,
otherwise by (31), β is a successor δ + 1 with δ o δ, and then (ω

β ) n = ω δ • n o ω δ • n = (ω β ) n , hence α n o λ n .
Proposition 29 (Monotonicity).

α o β and 0 < n ≤ m imply F α (n) ≤ F β (m) , (34)
α o α implies H α (n) ≤ H α (n) . (35)
Proof of (34): We prove (34) by induction on β. There are three cases: 1. If β = 0 then α o β implies α = 0 and we are done. 2. If β = λ is a limit, then by (33) either α o λ n or α is a limit and α n o λ n . In the first case F α (n) ≤ F λn (m) by i.h., in the second case F α (n) = F αn (n) ≤ F λn (m), again by i.h. Now (32) and the i.h. entail F λn (m) ≤ F λm (m) = F λ (m) and we are done.

If

β = β + 1 is a successor, then by (31) either α o β , or α = α + 1 with α o β .
In the first case,

F α (n) ≤ F β (m) (by i.h.) ≤ F m β (m) (by expansiveness) = F β (m).
In the second case,

F α (n) = F α +1 (n) = F n α (n). Now, since α o β , the i.h. gives F k α (n) ≤ F k β (m) for all k ∈ N (by ind. on k). In particular F n α (n) ≤ F n β (m) ≤ F m β (m) (by expansiveness) = F β (n).
Proof of (35): Let us proceed by induction on a proof of α o α , based on the deduction rules (28) and (29). For the base case, 0 o α implies H 0 (n) = n ≤ H α (n) by expansiveness. For inductive step with (28), if α o α and β o β , then

H α +β (n) = H α H β (n)
(by [START_REF] Löb | Hierarchies of number theoretic functions, I[END_REF])

≤ H α H β (n) (by ind. hyp. and (19)
)

≤ H α H β (n) (by ind. hyp.) = H α +β (n) .
(by ( 20))

For the inductive step with (29),

H ω α (n) = F α (n) ≤ F α (n) = H ω α (n) by (34).

B. Monotonicity for Codes

This Appendix details the proof of Proposition 16.

1) Atomic Losses: Let us first investigate a few properties of ≤ * over pure codes. Write x ≤ 1 * x when x ≤ * x and the difference between two pure codes x and x is in some sense "minimal". 3 Formally, the relation is defined by three axioms:

x 1 x 2 ≤ 1 * x 1 #x 2 x 1 x 2 ≤ 1 * x 1 vx 2 x 1 vx 2 ≤ 1 * x 1 (v + 1 j )x 2 (36)
with 0 ≤ j < k.

It is plain that ≤ * is the reflexive and transitive closure of ≤ 1 * . The following lemma allows reducing Proposition 16 to the simpler case x ≤ 1 * x : Lemma 30. If x ≤ * x are two pure codes, then there exists

x = x 0 ≤ 1 * x 1 ≤ 1 * x 2 ≤ 1 * • • • ≤ 1 * x =
x where the x i 's are pure.

Proof idea: We explain how to build the sequence of intermediary x i 's in three steps.

1) One starts with x and adds all missing # symbols one by one: this maintains purity. 2) One then adds vectors in place where they are missing.

In order to maintain purity, an empty position is filled by duplicating the vector immediately to the right of the empty slot (or add 0 if there is a # to the right). Any such addition maintains purity. For example, assume

x = . . . #v 1 v 3 v 6 # . . . and x = . . . #v 1 v 2 v 3 v 4 v 5 v 6 v 7 # . . . with v i ≤ v i for i ∈ {1, 3, 6}. Then x can be filled (in 4 steps) with x = . . . #v 1 v 3 v 6 # . . . ≤ 1 * ≤ 1 * ≤ 1 * ≤ 1 * . . . #v 1 v 3 v 3 v 6 v 6 v 6 0# . . . If this
filling process is done from right to left, every inserted vector is smaller than the corresponding vector in x (since x is pure) hence the constructed x i+1 remains ≤ * x . 3) We have now reduced the problem to the case where x and x have same length. It suffices to add enough unit vectors to every v until we reach the corresponding v in x whenever v < v . If this is done from left to right, purity is maintained.

2) Code Honesty: We investigate in this section two restrictions on the size of representation of codes during computations. One is an upper bound on the length of the code, and is true of any forward or backward computation with r -→. The second, trimness, is a restriction on the values that can appear in the vectors of the code: it is guaranteed by our forward computation, but need to be enforced on backward ones; however there exists one "perfect" backward computation that verifies it: it suffices to reverse the forward computation! a) Length Hierarchy: We define a hierarchy of functions H α (n) that bounds the length of any pure code x s.t.

H π(x) (n) = H α (n).
The strategy we adopt is to employ the rules of Definition 11 in reverse from a configuration (ε, H α (n)), and bound the size of the resulting code. It will turn out that this hierarchy is already known in the literature as the length hierarchy [24].

We define accordingly

H 0 (n) = 0 , (37)
H α+1 (n) = H α (n + 1) + 1 , (38)
H λ (n) = H λn (n) . (39)
Observe that, indeed, ε is of length 0, thus justifying (37); that if x is of length ≤ H α (n + 1), then applying rule (R1) in reverse increments this length by 1, thus justifying (38); finally, if x is of length ≤ H λn (n), then applying rule (R2) in reverse either decreases this length, or preserves it in case of a rewrite "Vv#x, n r -→ V(v) n #x, n" with (v) n = v -1 i + n • 1 i-1 for some i > 0, justifying (39). By Proposition 12, we deduce:

Lemma 31. If x is pure and x, n r -→ * ε, H α (n), then |x| ≤ H α (n).
The length hierarchy is closely related to the Hardy hierarchy; in particular [see e.g. 22, Eq. ( 65)]:

H α (n) = H α (n) -n . (40)
An easy observation in the same line as Lemma 31 is that backward rule applications from ε, H α (n) cannot increment the values in vectors to more that the total computed value H α (n). Thus, Note that our initial code x 0 from ( 10) is almost k-lean.

Lemma 32. If x 1 vx 2 is pure and x 1 vx 2 , n r -→ * ε, H α (n), then v[j] < H α (n) for all 0 ≤ j < k.
However, almost n-leanness is not a robust property of codes: e.g.

| 2 0 | 1 0 | 1 0 | 1 0 # encodes ω ω ω 2 +ω•3 and is almost 2- lean, but the smaller code | 1 0 | 1 0 | 1 0 | 1 0 # that encodes ω ω ω•4
is not almost 2-lean. We therefore introduce a slight relaxation of almost leanness: a pure code x is n-trim if, for any decomposition x = x 1 vx 2 , the ordinal β(v) is almost n-lean, i.e. there exists 0 ≤ i < k s.t. v[i] ≤ n and for all 0 ≤ j < i, v[j] = 0 and all i < j < k, v[j] < n. By analogy with almost leanness, call a computation trim if in every configuration x i , n i the code x i is n i -trim. Unlike almost leanness, trimness is clearly preserved by ≥ * . Interestingly, it is also preserved by direct computations, as shown by Lemma 15, which is a version of Lemma 33 that restricts computations to trim ones instead of almost lean ones:

Proof of Lemma 15: Define a large n-trim ordinal as π(x) where x is n-trim. We need to prove that if π is an n-trim large ordinal and π ≺ n π , then π is n-trim. This is obvious for π = π + 1, and we turn now to the different limit cases when π = π n . If π = (γ + ω α+1 ) n = γ + ω α • n, this holds; otherwise π = (γ + ω α ) n = γ + ω αn and we only need to prove that the small ordinals in α n = ( p i=1 ω βi ) n are almost n-lean, under the hypothesis that each

β i is almost n-lean since π is n-trim. If β p = β + 1 is a successor ordinal, then α n = p-1 i=1 ω βi + ω β • n, then β is clearly almost n-lean. If β p is a limit ordinal, then α n = p-1 i=1 ω βi + ω (βp)n is s.t.
β n is almost n-lean by Lemma 27. Hence π is n-trim in all cases.

Lemma 15 implies that forward computations preserve trimness, but more importantly that we can restrict our backward rule applications to enforce trimness. Such a restriction is required because backward rule applications do not necessarily preserve trimness: for instance with k = 2, we can go from a configuration (0, n)#, n to a configuration #(0, n)#, n -1 by applying (R1), and if n is sufficiently large, later to a configuration (0, n + 1)#, n for a considerably smaller n . What Lemma 33 entails is that there is another computation that fits our needs: for this example, applying (R2) backwards on (0, n)#, n yields (1, 0)#, n instead.

3) Monotonicity in Presence of Losses: We prove a series of monotonicity results that allow to handle losses in codes. As we work with ordinals of form ω α , it is more convenient to express these results using F α = H ω α . Lemma 34. Let α, α , γ be ordinals. If γ + α is almost n-lean and α < α , then γ + α ≺ n γ + α .

Proof: Write γ = γ 1 +γ 2 +γ 3 so that γ +α = γ 1 +γ 2 +α and γ + α = γ 1 + α . Now γ 2 + α < α and γ 2 + α is almost n-lean, so that γ 2 + α ≺ n α by Lemma 28 and γ

+ α = γ 1 + γ 2 + α ≺ n γ 1 + α = γ + α by (24). Lemma 35. If γ ≺ n γ then F γ+α (n) ≤ F γ+α (n).
Proof: We proceed by induction over α.

For α = 0, γ ≺ n γ entails F γ (n) ≤ F γ (n) by (26). For α = β + 1 a successor ordinal, the ind. hyp. and [START_REF] Ph | Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets[END_REF] gives 19) and ( 18), hence F γ+β+1 (n) ≤ F γ +β+1 (n). For α = λ a limit ordinal, we immediately have

F γ+β (m) ≤ F γ +β (m) for any m ≥ n, hence F n γ+β (n) ≤ F n γ +β (n) by (
F γ+λ (n) = F γ+λn (n) ≤ F γ +λn (n) = F γ +λ (n) by ind. hyp.
We exploit Lemma 34 in the two following lemmata, which match cases 2 and 3 of atomic losses in codes:

Lemma 36. If γ is n-lean, then F γ+α +α (n) ≤ F γ+α +ω β +α (n).
Proof: If α > 0, the lemma is trivial, as putting γ = γ 1 + γ 2 and γ + α = γ 1 + α shows that γ 1 + α + α o γ 1 + α + ω β + α and we conclude by (34). Assume therefore α = 0; then Lemma 34 applies to show γ ≺ n γ + ω β since γ is almost n-lean and 0 < ω β , and applying Lemma 35 yields the result.

Lemma 37. If γ + ω β is almost n-lean and β o β , then F γ+α +ω β +α (n) ≤ F γ+α +ω β +α (n).
Proof: As in the previous proof, the case α > 0 is trivial since ω β o ω β by (29). Assume therefore α = 0, then ω β < ω β yields γ + ω β ≺ n γ + ω β by Lemma 34, and applying Lemma 35 yields the result.

The following proposition together with [START_REF] Lazić | Nets with tokens which carry data[END_REF] immediately proves Proposition 16: Proposition 38. Let x, x be pure codes and n > 0. If x is n-trim and x ≤ * x , then H π(x) (n) ≤ H π(x ) (n).

Proof: We proceed by induction on the number of ≤ 1 *steps between x and x . If x = x the result hold vacuously. Consider therefore for the induction step a pure code x with x ≤ * x and x ≤ 1 * x ; clearly x and x are also n-trim. By ind. hyp., H π(x ) (n) ≤ H π(x ) (n), and we only need to prove

H π(x) (n) ≤ H π(x ) (n).
1) The first axiom is easy to treat: if x = x 1 x 2 and x =

x 1 #x 2 , then π(x) o π(x ) and thus H π(x) (n)

≤ H π(x ) (n). This simple proof is the main rationale for our cumulative encoding of ordinals. The next two axioms require more work. In both cases, we decompose

x into x 1 #V 1 vV 2 #x 2 where v is the particular vector modified by ≤ 1 * , so that x = x 1 #V#x 2 verifies either V = V 1 V 2 (in the case of the second axiom) or V = V 1 (v - 1
j )V 2 for some 0 ≤ j < k (in the case of the third axiom). By Lemma 15, there exists a trim computation on x ; its initial phase is of form:

x 1 #VvV #x 2 , n r -→ * pure(V (x 1 )V 1 vV 2 #x 2 ), n (41)
which we reach by evaluating x 1 in full, i.e.

x 1 #, n r -→ * ε, n , (42)
where we define

n def = H π(x1#) (n) . (43)
Assume that the following claim holds for all vector sequences V and all r ≥ n :

H ω α(V (x 1 )VV ) (r) ≤ H ω α(V (x 1 )V 1 vV 2 V ) (r) . (44) Let further x 2 def = V 3 # • • • #V m #,
and consider the prefix corresponding to (41) in the computation on x: it encodes a Hardy computation

H π(x1#V#x2) (n) = H π(V (x1)VV3#•••#Vm#) H ω α(V (x 1 )V) (n )
(by [START_REF] Löb | Hierarchies of number theoretic functions, I[END_REF]) [START_REF] Löb | Hierarchies of number theoretic functions, I[END_REF] and setting 44) with V = V 3 and ( 19))

≤ H π(V (x1)VV3#•••#Vm#) H ω α(V (x 1 )V 1 vV 2 ) (n ) (by (44) with V = ε and (19)) = H π(V (x1)VV3V4#•••#Vm#) H ω α(V (x 1 )VV 3 ) (n ) (by
n def = H ω α(V (x 1 )V 1 vV 2 ) (n )) ≤H π(V (x1)VV3V4#•••#Vm#) H ω α(V (x 1 )V 1 vV 2 V 3 ) (n ) (by (
. . .

≤ H π(V (x1)V1vV2#x2) (n ) = H π(x ) (n) .
It only remains to prove the claimed (44). To this end, two comments on the prefix of the computation (41) are in order: by combining Lemma 31 and (40) on the computation (42), we deduce that |x 1 | ≤ n -n < n since n > 0, thus α(V (x 1 )) can be written as p i=1 ω βi with p < n . Using Lemma 32, each β i , which is encoded by a vector appearing in x 1 , is n -lean, hence:

α(V (x 1 )) is n -lean. ( 45
)
In the same way, since the computation is trim, β(v) is almost n -lean. Recall that the CNF of α(V (x 1 )) has p < n terms.

As it is also n -lean, adding an almost n -lean term yields an almost n -lean term:

α(V (x 1 )) + ω β(v) is almost n -lean. (46)
Note that (45) and ( 46) also hold for all r ≥ n . Turning to the two remaining axioms:

2) For the second axiom, recall that

V = V 1 V 2 . Put γ = α(V (x 1 )), α = α(V 1 ), β = β(v),
and α = α(V 2 V ). Then, by (45) and Lemma 36,

H ω γ+α +α (r) = F γ+α +α (r) ≤ F γ+α +ω β +α (r) = H ω γ+α +ω β +α (r). 3) For the third axiom, recall that V = V 1 (v -1 j )V 2 . Put γ = α(V (x 1 )), α = α(V 1 ), β = β(v -1 j ), β = β(v),
and α = α(V 2 V ). By (30), β o β , and by (46) and Lemma 37, H ω γ+α +ω β +α (r) = F γ+α +ω β +α (r) ≤ F γ+α +ω β +α (r) = H ω γ+α +ω β +α (r).

C. Proof of Theorem 20 (Section VIII)

1. If L is L(N ) for some PDN N , then the question whether w ∈ L reduces to a coverability problem for N def = w ⊗ N , a PDN obtained by a synchronized product of N and (an FSA for) w. Since |N | = O(|w|) (here N is a constant of size O(1)) and since N is k-dimensional when N is, we have reduced L to coverability for k-PDNs, a problem in TIME(F ω ω k+O(1) (n)) by Theorem 3.

2. With a Minsky machine (MM) M and some k, the construction in section V associates a PDN that simulates M with space bounded by F ω ω k (n). It is easy to modify the PDN so that it (1) guesses a word w of length n; (2) outputs w while weakly storing w# n in the work space of the MM and weakly storing n in cpt; [START_REF] Abdulla | On the coverability problem for constrained multiset rewriting[END_REF]

D. Weak Implementation of r -→

In Table I, we present the so-called "weak" rules that define d -→, a weakening of both r -→ and r -→ -1 in the sense of Theorem 17, which proves its weak correctness. Note that a general implicit condition on the rules is that they take and produce trim configurations. Rule 1 corresponds to rule (R1) but we have split the exact rule (R2) of r -→. Indeed in order to correctly define d -→, we need to make explicit the implicit different cases of rule (R2). More precisely, the application of this rule may vary depending on two criteria:

• The type of the vector that is found in front of the first #. Rules 2-5 correspond to the case of the null vector, as in [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF]. Rules 6-9 correspond to the case of a vector whose first component is non null, which is the first case in [START_REF] Finkel | A wellstructured framework for analysing Petri nets extensions[END_REF]. Rules 10-13 correspond to the remaining case of (15).

• Inside any group of rules, there are four cases depending on what follows the first #. It can be the empty sequence, a second # or a vector. This last case is again split into two subcases depending on a lexicographic relation.

This laborious presentation of all the rules has its uses, firstly because writing the weak backward rules and performing trimming on-the-fly without first breaking up the various cases turned out to be an error-prone task, and secondly because there is sufficient variation between the various cases of r -→ and especially of r -→ -1 to warrant handling them separately in a PDN implementation.

Let us repeat that these weak rules always produce a trim representation. In order to prove the correction of the the weak rules, we prove that they are weakenings as defined in Definition 18. -→ V(v + 1 i )#w t , n ∃i > 0 v(i) > 0 ∧ ∀j < i v(j) = 0, V ≤ * r, ∃v ≤ v Vv pure i > 0, ∀j < i v (j) = 0, v(i -1) ≥ n ∀j / ∈ {i -1, i} v (j) = v(j), ∃i > 0 v (i) > 0 ∧ ∀j < i v (j) = 0 ∀j > i v (j) ≤ v(i) v (i) = v(i) -1 and v (i -1) = n v ≤ v -1 i + (n )1 i-1 (v + n 1 i-1 ) < lex w ≤ w v < lex w w ≤ w v < lex w and t ≤ * t V ≤ * r and t ≤ * t

-→ Vv #, n rvs#t, n r -→ V(v + 1 i )#, n ∃i > 0 v(i) > 0 ∧ ∀j < i v(j) = 0, V ≤ * r, ∃v ≤ v Vv pure i > 0, ∀j < i v (j) = 0, v(i -1) ≥ n ∀j / ∈ {i -1, i} v (j) = v(j), ∃i > 0 v (i) > 0 ∧ ∀j < i v (j) = 0 ∀j > i v (j) ≤ v(i) v (i) = v(i) -1 and v (i -1) = n v ≤ v -1 i + (n )1 i-1 V ≤ * r Rule 11 Vv##t, n r -→ Vv #v#t, n rvs#s #t, n r -→ Vv #v #, n rvs#s us #t, n r -→ V(v + 1 i )##, n ∃i > 0 v(i) > 0 ∧ ∀j < i v(j) = 0, V ≤ * r, v ≤ v Vv pure ∃v ≤ u , ∀j < i v (j) = 0 ∧ v ≥ (v + 1 i ) ∀j / ∈ {i -1, i} v (j) = v(j), ∃i > 0 v (i) > 0 ∧ ∀j < i v (j) = 0 i > 0, v ≥ v -1 i + (n )1 i-1 v (i) = v(i) -1 and v (i -1) = n v ≤ v -1 i + (n )1 i-1 V ≤ * r Rule 12 Vv#wt, n r -→ Vv #vwt, n rvs#s wt, n r -→ Vv #v w t, n rvs#s us wt, n r -→ V(v + 1 i )#w t , n ∃i > 0 v(i) > 0 ∧ ∀j < i v(j) = 0, V ≤ * r, v ≤ v Vv pure ∃v ≤ u , ∀j < i v (j) = 0 ∧ v ≥ (v + 1 i ) ∀j / ∈ {i -1, i} v (j) = v(j), ∃i > 0 v (i) > 0 ∧ ∀j < i v (j) = 0 i > 0, v ≥ v -1 i + (n )1 i-1 v (i) = v(i) -1 and v (i -1) = n v ≤ v -1 i + (n )1 i-1 w ≤ lex v , V ≤ *

E. PDN Simulation of

d - →
The implementation of all the various cases described by the rules of Table I is highly redundant, and relies on the same core ideas that we have illustrated in Section VII. We only present a few salient points that ought to convince the reader that all rules can be implemented in a PDN.

1) Weak Forward Rule 1: Let us recall this rule:

s#t, n d - → t, n + 1 (D1)
This (simple) rule does not require to copy the code in order to be simulated. It is sufficient to select an identity between low and high corresponding to a #, to update the low identity with this identity (implicitly deleting the prefix #) and to increment the counter. This is performed by a single transition depicted in Figure 5.

2) Weak Forward Rule 3: Let us recall this rule:

rvs#s #t, n d - → V# n 0#t , n (D3)
where V ≤ * r is pure, t ≤ * t, and n ≤ n ≤ n. In the perfect case, these orderings are equalities, v is 0, and s, s are ε. a) First Stage: It consists in duplicating the counter, which corresponds to the following transition. The subsequent stages consist of an appropriate copy with update of the code.

b) Second Stage: It consists in extracting a non empty vector sequence and in copying with purification a vector sequence with the last vector (v) which is not copied. This can be performed by a net similar to (and in fact simpler than) the purification net of Figure 4. It corresponds to the following partial transition. The up arrows are "lower bounds" of the identities of from and to. rv ↑ x , n → V ↑ where V ≤ * r, V pure and n ≤ n c) Third Stage: It consists in picking two # in the remaining code (x ) and in copying, with the help of the duplicated counter, at most n # symbols followed by the null vector and a #. This is performed by the net of Figure 6. Transition mult 1 checks that from contains the identity of a # symbol and adds such a symbol to the new code. Transition mult 2 , which can be performed at most n times, also adds a # at the end of the new code. Finally, transition mult 3 adds a null vector to the new code and "moves forward" the identity contained in from. All transitions also move forward the token in to. Creating a null vector is easy since it simply consists in adding a vect identity to the new code. We have not represented the concatenation of the # which simply consists in adding a token in place sharp with identity to and in increasing the identity.

This stage corresponds to the partial transition:

rvs#s # ↑ t, n → V# n 0# ↑
where V ≤ * r, V pure and n ≤ n ≤ n d) Fourth Stage: The last stage consists in copying the remaining code t in a way similar to that of the weak trimming net.

3) Weak Forward Rule 7: Let us recall this rule:

rvs#s #t, n d - → Vv 0 . . . v n #(v n + 1 0 )#t , n (D7)
where V ≤ * r, v 0 + 1 0 ≤ v, V(v 0 + 1 0 ) pure, ∀0 ≤ i ≤ n, v i ≤ v i , t ≤ * t, and n ≤ n ≤ n We have already presented all the gadgets necessary to simulate this rule. First we duplicate the counter which yields a new value n ≤ n. Then we extract and copy a non empty pure vector sequence, the last vector containing at least a token in the 0-component; this sequence is V(v 0 + 1 0 ). We delete this token and extend it to a sequence of n non increasing vectors v 0 . . . v n #v n (inserting a # before and after writing the last vector). This can be done by a modified version of the purification net where the duplicated counter controls the length of the sequence (as for the duplication of # in rule D2). We add a token to the last vector. Finally, we copy the remaining code t at the end of the new code.

4) Weak Forward Rule 11: Let us recall this rule:

rvs#s #t, n d - → Vv #v t , n (D11)
where V ≤ * r, v ≤ v, ∃i > 0 v (i) > 0 ∧ ∀j < i v (j) = 0, Vv pure, v ≤ (v ) n , t ≤ * t and n ≤ n ≤ n We simulate the rule in four stages. First we duplicate the counter. Then we simulate the following partial copy:

rv ↑ x → Vv #v
It consists in extracting and copying a non empty pure vector sequence Vv #v . The copy of the last vector is particular since

• we arbitrarily choose some component index i, such that v (i) > 0; we memorize this choice by marking place deriv i . • we set v (j) = 0 for all j < i; • we duplicate v in the new code and separate them by a #. This can be done by moving forward to three times and keeping in auxiliary places oldto and oldoldto the identities that precede the current one. Then the copy is done simultaneously using to and oldoldto for the two copies of the vector, while a # is inserted with identity oldto.

The third stage consists in deriving it, i.e. in deleting a token in c i and adding at most n tokens in c i-1 . This is done by the net of Figure 7 for some case i. Transition deriv i,1 starts the derivation by subtracting a token in c i . Then there are at most n applications of deriv i,2 adding tokens in c i-1 . Finally, deriv i,3 stops the derivation by adding one more token in c i-1 .

The last stage consists in copying the remaining code #t at the end of the new code.

We end this subsection by presenting the copy of remaining vectors of a sequence during the weak trimming in figure 8.

ADDITIONAL REFERENCES

[24] E. A. Cichoń and E. Tahhan Bittar, "Ordinal recursive bounds for Higman's Theorem," Theor. Comput. Sci., vol. 201, pp. 63-84, 1998. ...

Fig. 1 .

 1 Fig. 1. Schematics for Theorem 4.

  and x is n-trim (and thus pure) and call trimming the transformation from x , n to x, n (nondeterministic but always possible, e.g. by decreasing vector values in excess, or removing vectors). In particular, trim --→⊆≥ * where we let x, n ≤ * x , n def ⇔ x ≤ * x and n ≤ n . Trimness allows us to focus on particular computations of r -→: Lemma 15. If x is n-trim, then there exists a trim computation x, n r -→ * ε, H π(x) (n). As our initial code x 0 defined in Example 10 is k-trim, it suffices in the following to consider trim computations, i.e. forward computations in rt -→ or backward computations in rt -→ -1 , where x, n rt -→ y, m def ⇔ x, n r -→ y, m and x, n and y, m are trim. (In other words, rt -→= r

1 )

 1 so that Theorem 17 is a proof of Lemma 5. We have to explain how to represent pairs x, n in a PDN, how to transform them correctly, and to engineer definitions for d -→ and b -→ that are both simple enough for PDN implementability, but rigorous and complete enough to fulfil the requirements of Definition 18. One can loosely describe on codes, tolerating decreases (wrt ≤ * ) on x and n, all the while trimming x regularly because Definition 18 requires it." The PDNs are highly nondeterministic (unlike r -→) and may deadlock, but this is not a concern.

  be found in the full version of the paper, but all the main implementation ideas are already present with the trimming process.A. Encoding Configurations of r -→ in a PDN The weak implementation of Hardy computations has to maintain a PDN representation of a code/counter pair x, n.

Fig. 2 .

 2 Fig. 2. Duplication of the counter value.

Fig. 3 .

 3 Fig. 3. Copying the first vector (case i).

Fig. 4 .

 4 Fig. 4. Control part of the trimming phase.

  This immediately entails separation results like L(APN) L(LCS) L(PDN)(= L(TPN) = L(DN)) and the noncollapse of hierarchies like {L(k-PDN)} k∈N , {L(k-LCS)} k and {L(k-APN)} k where k-DN, k-APN and k-LCS restrict

  is n-lean by ind. hyp. on β m .Lemma 26. If a successor ordinal α+1 is almost n-lean then α is n-lean.Proof: If α + 1 = ω β1 • c 1 + • • • + ω βm • c mas above, it means β m = 0, thus we are in case (i) of almost n-lean ordinals with c m ≤ n, and α

  and β m is n-lean, and by Lemma 25 (β m ) n is almost nlean and λ n is almost n-lean by condition (ii), or (ii) c m < n and β m is almost n-lean, and by ind. hyp. (β m ) n is almost n-lean, and λ n almost n-lean by condition (ii).

  b) Almost Lean and Trim Computations: Lemma 32 does not provide us with enough information on the values in vectors for our purposes. Recall the definition of almost n-lean ordinals from Appendix A3. Let us call a pure code x almost n-lean if π(x) is almost n-lean. By extension, a configuration x, n of r -→ is almost lean if x is pure and almost n-lean, and a computation x 0 , n 0 r -→ x 1 , n 1 r -→ • • • r -→ x m , n m is almost lean if every configuration x i , n i is almost lean, for every 0 ≤ i ≤ m. By Lemmas 25 to 27, we deduce: Lemma 33. If π(x) is almost n-lean, then there exists an almost lean computation x, n r -→ * ε, H π(x) (n).

  r

Fig. 5 .

 5 Fig. 5. Implementation of (D1).

Fig. 6 .

 6 Fig. 6. Multiplying the tally symbol

Fig. 7 .

 7 Fig. 7. Derivating a vector (case i)

Fig. 8 .

 8 Fig. 8. Weak Trimming: Copying the remaining vectors.

  or[21, §4]) and classic construction yields a PDN N M that simulates M as far as halting is concerned: N M has unbounded places c M 1 , . . . , c M r to simulate the r counters of M . Starting from control place p start and with empty Adding cpt as a budget has two consequences. First, M is now simulated with an upper bound of n for (the sum of) its counters, at any time along its run. Second, when N M reaches p halt , witnessing that M halts, does not require testing

	c M 1 , . . . , c M r , it eventually reaches p halt with c M 1 , . . . , c M r empty iff M halts. We further modify N M so that it uses cpt (where N H [k] stores n ) as a budget, i.e. any incrementing of a c M i is matched by decrementing cpt and vice versa, see [23, §4]. c M 1 , . . . , c M r for emptiness: at this point, the value n f of cpt is necessarily ≤ n , and only equals n if c M 1 , . . . , c M r are empty (NB

  if we have c i < n and if, inductively, β i is also n-lean, this for all i = 1, . . . , m.Let us introduce a slight variant of n-lean ordinals [see 22, Lemma D.2]: let

  generates F ω ω k (n) extra workspace for M and runs it on w; (4) after/if M accepts w, folds back the workspace and reconstructs cpt; (5) outputs # n where n is value now stored in cpt. As in Section V, the nature of weak computations guarantees n ≤ n, and one only has n = n if the simulation of the MM (and storing w) was perfect. Hence the PDN only outputs words w# n s.t. n = |w| and that are accepted by M in space F ω ω k (n) (or s.t. n < |w| and hence that are not in L 0 ).

TABLE I THE

 I EXACT AND WEAK RULES.

This is not bijective, e.g.for v < lex v , α(v v ) = ω β(v) + ω β(v ) =

It would be minimal for arbitrary codes if the second axiom was reading x 1 x 2 ≤ 1 * x 1 0x 2 , but it would not always relate pure codes to pure codes.

ACKNOWLEDGMENT

Work supported by ANR grant 11-BS02-001-01 and by the Leverhulme Trust. The third author is currently visiting the Computer Science Department at Oxford University.

APPENDIX

A. Subrecursive Hierarchies and Monotonicity 1) Properties of the Hardy Hierarchy: Let us remind a few useful facts about the Hardy hierarchy (see [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF] or [22, Appendix C] for details).

The first fact is that each Hardy function is expansive and monotone in its argument n: Fact 21 (Expansiveness and Monotonicity, see e.g. 22, Lemmata C.9 and C.10). For all α, α and n > 0, m,

with n ≤ n ≤ n, V ≤ * r, t ≤ * t with n ≤ n, V ≤ * r and t ≤ * t 1 0 ≤ v, v 0 ≤ (v -1 0 ) and v 0 + 1 0 < lex w v ≤ min(v i ) , w ≤ w and v + 1 0 < lex w Rule 10

Vv#, n r -→ Vv #, n rvs#t, n