Arnaud Carayol

Olivier Serre

Collapsible Pushdown Automata and Labeled Recursion Schemes Equivalence, Safety and Effective Selection

Keywords: Recursion Schemes, Collapsible Pushdown Automata, Safety Constraint, MSO Effective Selection

Higher-order recursion schemes are rewriting systems for simply typed terms and they are known to be equiexpressive with collapsible pushdown automata (CPDA) for generating trees. We argue that CPDA are an essential model when working with recursion schemes. First, we give a new proof of the translation of schemes into CPDA that does not appeal to game semantics. Second, we show that this translation permits to revisit the safety constraint and allows CPDA to be seen as Krivine machines. Finally, we show that CPDA permit one to prove the effective MSO selection property for schemes, subsuming all known decidability results for MSO on schemes.

I. INTRODUCTION

Higher-order recursion schemes are rewriting systems for simply typed terms and in recent years they have received much attention as a method of constructing rich and robust classes of possibly infinite ranked trees. Remarkably these trees have decidable monadic second-order (MSO) theories, subsuming most of the examples of structures for which MSO is decidable. Since the original proof of Ong [START_REF] Ong | On model-checking trees generated by higherorder recursion schemes[END_REF] based on traversals (a tool from game semantics), several alternative proofs (and extensions) were obtained using different techniques: automata [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF], [START_REF] Broadbent | Recursion schemes and logical reflexion[END_REF], intersection types [START_REF] Kobayashi | A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes[END_REF], the Krivine machine [START_REF] Salvati | Krivine machines and higherorder schemes[END_REF].

In this article we focus on the automata approach. In [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF], schemes were shown to be equi-expressive with an extension of the standard model of pushdown automata, called collapsible pushdown automata (CPDA). The translation from schemes into CPDA crucially relied on traversals. The decidability of MSO was obtained by solving parity games played on transition graphs of CPDA. In [START_REF] Broadbent | Recursion schemes and logical reflexion[END_REF] a refinement of this proof was used to show that the family of trees generated by schemes is MSO-reflective, i.e. for any scheme S and any MSO formula ϕpxq with one first-order free variable x, one can build another scheme that produces the same tree as S except that now all nodes satisfying ϕpxq are marked.

In this article, we focus on the merits of CPDA for studying recursion schemes. As CPDA are more naturally associated with a labeled transition system (LTS) than with a tree, we introduce a variant of recursion schemes, labeled recursion schemes, that admit a canonical LTS. In both cases, the tree generated is simply the unfolding of the LTS. Although not technically difficult, we think that this notion and the associated family of LTS can be the subject of further studies.

Our first main result is a simplified and syntactic proof of the translation of a scheme into an equivalent CPDA. This is the first proof of the equi-expressivity result of [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] that does not use game semantics. A comparison of the obtained CPDA can be found at the beginning of Section III.

Furthermore this translation also permits one to view a CPDA as a Krivine machine, hence inheriting the simplified proof of [START_REF] Salvati | Krivine machines and higherorder schemes[END_REF] for decidability of µ-calculus model-checking.

We also show that when translating a safe scheme we obtain a CPDA that does not need to use the links. This result, independently obtained by Blum and Broadbent [START_REF] Broadbent | On Collapsible Pushdown Automata, their Graphs and the Power of Links[END_REF], unifies the work of [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF] on safe schemes and sheds a new light on safety. As a spin-off result, we give a more natural definition of safety based on Damm's original work [START_REF] Damm | The IO-and OI-hierarchies[END_REF].

Finally, the true gain of the apparently more involved CPDA model is demonstrated by showing that the trees defined by recursion schemes enjoy the effective MSO selection property: for any scheme S and any formula DX ϕpXq if the tree t generated by S satisfies DX ϕpXq, one can build another scheme generating the tree t where a set of nodes U satisfying ϕpXq is marked. This new result subsumes all previously known MSO-decidability results on recursion schemes (while keeping the same complexity, in particular the one of [START_REF] Kobayashi | A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes[END_REF]) and relies on a careful analysis of the winning strategies in CPDA parity games.

II. PRELIMINARIES A. Trees and Terms

Let A be a finite alphabet. We denote by A ˚the set of finite words over A. A tree t (with directions in A) is a nonempty prefix-closed subset of A ˚. Elements of t are called nodes and ε is called the root of t. For any node u P t and any direction a P A, we refer to ua, when it belongs to t, as the a-child of u. A node with no child is a leaf.

A ranked alphabet A is an alphabet that comes together with an arity function, ̺ : A Ñ N. The terms built over a ranked alphabet A are those trees with directions Ý Ñ A def " Ť f PA Ý Ñ f where Ý Ñ f " tf 1 , . . . , f ̺pf q u if ̺pf q ą 0 and Ý Ñ f " tf u if ̺pf q " 0. For a tree t with directions in Ý Ñ A to be a term, we require, for all nodes u, that the set A u " td P Ý Ñ A | ud P tu is empty iff u ends with some f P A (hence ̺pf q " 0) and if A u is non-empty then it is equal to some Ý Ñ f P Ý Ñ A . We denote by TermspAq the set of terms over A. For c P A of arity 0, we denote by c the term tε, cu. For f P A of arity n ą 0 and for terms t 1 , . . . , t n , we denote by f pt 1 , . . . , t n q the term tεu Y Ť iPr1,ns tf i u ¨ti . These notions are illustrated in Figure 1.

' ' ' ' ' ' c f 1 f 2 ' ' c f 1 f 2 f f ' c c Figure 1
. Two representations of the infinite term f 2 tf 1 c, f 1 , εu " f pc, f pc, f p¨¨¨qqq over the ranked alphabet tf, cu assuming that ̺pf q " 2 and ̺pcq " 0.

B. Labeled Transition Systems

A rooted labeled transition system (LTS for short) is an edge-labeled directed graph with a distinguished vertex, called the root. When considering LTS associated with computational models, it is usual to allow silent transitions. The symbol for silent transitions is usually ε but here, to avoid confusion with the empty word, we will instead use e.

We forbid a vertex to be the source of both a silent transition and of a non-silent transition. When Σ is an alphabet we let Σ e " Σzteu.

Formally, a rooted labeled transition system with silent transitions L is a tuple x D, r, Σ, p a ÝÑq aPΣ y where D is a finite or countable set called the domain, r P D is a distinguished element called the root, Σ is a finite set of labels that contains a distinguished symbol denoted e and for all a P Σ, a ÝÑ Ď D ˆD is a binary relation on D.

For any a P Σ and any ps, tq P D 2 we write s a ÝÑ t to indicate that ps, tq P a ÝÑ, and we refer to it as an atransition with source s and target t. Moreover, we require that for all s P D, if s is the source of a e-transition, then s is not the source of any a-transition with a ‰ e. For a word w " a 1 ¨¨¨a n P Σ ˚, we define a binary relation w ÝÑ on D by letting s w ÝÑ t (meaning that ps, tq P w ÝÑ) if there exists a sequence s 0 , . . . , s n of elements in D such that s 0 " s, s n " t, and for all i P r1, ns, s i´1 ai ÝÑ s i . These definitions are extended to languages over Σ by taking, for all L Ď Σ ˚, the relation L ÝÑ to be the union of all w ÝÑ for w P L.

For all words w " a 1 ¨¨¨a n P Σ e , we denote by An LTS is said to be deterministic if for all s, t 1 and t 2 in D and all a in Σ, if s a ÝÑ t 1 and s a ÝÑ t 2 then t 1 " t 2 .

Caveat 1. From now on, we always assume that the LTS we consider are deterministic.

We associate a tree to every LTS L, denoted TreepLq, with directions in Σ e , reflecting the possible behaviours of L starting from the root. For this we let TreepLq def " tw P Σ e | Ds P D, r w ùñ su. As L is deterministic, TreepLq is obtained by unfolding the underlying graph of L from its root and contracting all e-transitions. Figure 2 presents an LTS with silent transitions together with its associated tree TreepLq.

As illustrated in Figure 2, the tree TreepLq does not reflect the diverging behaviours of L (i.e. the ability to perform an infinite sequence of silent transitions). For instance in the LTS of Figure 2, the vertex s diverges whereas the vertex t does not. A more informative tree can be defined in which diverging behaviours are indicated by a K-child for some fresh symbol K. This tree, denoted Tree K pLq, is defined by letting Tree K pLq def " TreepLq Y twK P Σ e K | @n ě 0, r we n ùñ s n for some s n u.

C. Types, Applicative Terms

Types are generated by the grammar τ ::" o | τ Ñ τ . Every type τ " o can be uniquely written as τ 1 Ñ pτ 2 Ñ ¨¨¨pτ n Ñ oq . . .q where n ě 0 and τ 1 , . . . , τ n are types. The number n is the arity of the type and is denoted by ̺pτ q. To simplify the notation, we take the convention that the arrow is associative to the right and we write τ 1 Ñ ¨¨¨Ñ τ n Ñ o (or pτ 1 , . . . , τ n , oq to save space).

The order measures the nesting of a type: ordpoq " 0 and ordpτ 1 Ñ τ 2 q " maxpordpτ 1 q `1, ordpτ 2 qq.

Let X be a set of typed symbols. Every symbol f P X has associated a type τ ; we write f : τ to mean that f has type τ . The set of applicative terms of type τ generated from X, denoted Terms τ pXq, is defined by induction over the following rules. If f : τ is an element of X then f P Terms τ pXq; if s P Terms τ1Ñτ2 pXq and t P Terms τ1 pXq then the applicative term obtained by applying s to t, denoted s t, belongs to Terms τ2 pXq. For every applicative term t, and every type τ , we write t : τ to mean that t is an applicative term of type τ . By convention, the application is considered to be left-associative, thus we write t 1 t 2 t 3 instead of pt 1 t 2 qt 3 . The set of subterms of t, denoted Subsptq, is inductively defined by Subspf q " tf u for f P X and Subspt 1 t 2 q " Subspt 1 q Y Subspt 2 q Y tt 1 t 2 u. The subterms of the term f pf gq c : o in Example 1 are f pf gq c , f , f g , f pf gq , c and g. A less permissive notion is that of argument subterms of t, denoted ASubsptq, which only keep those subterms that appear as an argument. The set ASubsptq is inductively defined by letting ASubspt 1 t 2 q " ASubspt 1 qYASubspt 2 qY tt 2 u and ASubspf q " ∅ for f P X. In particular if t " F t 1 ¨¨¨t n , ASubsptq " Y n i"1 pASubspt i q Y tt i uq. The argument subterms of f pf gq c : o are f g , c and g. In particular, for all terms t, one has |ASubsptq| ă |t| (the size |t| of a term is the length of the word representation of t).

Remark 1. A ranked alphabet A can be seen as a typed alphabet by assigning to every symbol f of A the type o Ñ ¨¨¨Ñ o Ñ loooooooomoooooooon ̺pf q o. In particular, every symbol in A has order 0 or 1. The finite terms over A (seen as a ranked alphabet) are in bijection with the applicative ground terms over A (seen as a typed alphabet).

D. Labeled Recursion Schemes

Recursion schemes are grammars for simply typed terms, and they are often used to generate a possibly infinite term. Traditionally, recursion schemes are not associated with an LTS. Here we provide an alternative definition based on LTS.

For each type τ , we assume an infinite set V τ of variables of type τ , such that V τ1 and V τ2 are disjoint whenever τ 1 " τ 2 , and we write V for the union of those sets V τ as τ ranges over types. We use letters x, y, ϕ, ψ, . . . to range over variables.

A deterministic labeled recursion scheme is a 5-tuple S " x Σ, N, R, Z, K y where ' Σ is a finite set of labels and K is a distinguished symbol in Σ,

' N is a finite set of typed non-terminals; we use uppercase letters F, G, H, . . . to range over non-terminals, ' Z : o P N is a distinguished initial symbol which does not appear in any right-hand side, ' R is a finite set of production rules of the form

F x 1 ¨¨¨x n a ÝÑ e
where a P ΣztKu, F : pτ 1 , ¨¨¨, τ n , oq P N , the x i s are distinct variables, each x i is of type τ i , and e is a ground term over pN ztZuq Y t x 1 , . . . , x n u.

In addition, we require that there is at most one production rule starting with a given non-terminal and labeled by a given symbol. The LTS associated with S has the set of ground terms over N as domain, the initial symbol Z as root, and, for all a P Σ, the relation a ÝÑ is defined by: F t 1 . . . t ̺pF q a ÝÑ ert 1 {x 1 , . . . , t ̺pF q {x ̺pF q s if F x 1 ¨¨¨x n a ÝÑ e is a production rule. The tree generated by a labeled recursion scheme S, denoted Tree K pSq, is the tree Tree K of its associated LTS. To use labeled recursion schemes to generate terms over ranked alphabet A, it is enough to enforce that for every non-terminal F P N :

' either there is a unique production starting with F which is labeled by e, ' or there is a unique production starting with F which is labeled by some symbol c of arity 0 and whose righthand side starts with a non-terminal that comes with no production rule in the scheme,

' or there exists a symbol f P A with ̺pf q ą 0 such that the set of labels of production rules starting with F is exactly Ý Ñ f . Example 2. Consider the order-1 scheme S " x Σ, N, R, Z, K y where Σ " ta, f 1 , f 2 , Ku, N consists of Z, X, a : o, H : po, oq, f : po, o, oq and F : ppo, o, oq, oq, and R is given below The LTS and the tree associated with S are depicted in Figure 3.

Remark 2. A more standard definition of recursion schemes [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] comes with a ranked alphabet A of terminal symbols that can be used in the right hand side of the rewriting rules; moreover the rules are no longer labeled. Applying rewriting rules from the initial symbol one derives finite terms over the set of terminal and non-terminal symbols. Replacing in such a term t any non-terminal, together with its argument, by a fresh symbol K : o leads a term t K over A Y tKu.

As the rewriting is confluent, there exists a supremum of all terms t K where t ranges over terms that can be rewritten from the initial symbol, and this (possibly infinite) term is defined as the value term of the scheme.

It is easily seen that labeled recursion schemes and (usual) recursions schemes generate the same terms; the translations are linear and preserve both order and arity.

E. Examples of Trees Defined by Labeled Recursion Schemes

We provide some examples of trees defined by labeled recursion schemes. Given a language L over Σ, we denote by PrefpLq the tree containing all prefixes of words in L.

Example 3. Using order-2 schemes, it is possible to go beyond deterministic context-free languages and to define for instance the tree T 1 " Prefpta n b n c n | n ě 0uq. Consider for instance the order-2 scheme S 1 given by:

Z a ÝÑ F I pK C Iq B x b ÝÑ x F ϕ ψ a ÝÑ F pK B ϕq pK C ψq C x c ÝÑ x F ϕ ψ b ÝÑ ϕpψ Xq I x e ÝÑ x K ϕ ψ x e ÝÑ ϕpψpxqq
with Z, X : o, B, C, I : o Ñ o, F : ppo Ñ oq, po Ñ oq, oq and K : ppo Ñ oq, po Ñ oq, o, oq.

Intuitively, the non-terminal K plays the role of the composition of functions of type o Ñ o (i.e. for any terms

F 1 , F 2 : o Ñ o and t : o, K F 1 F 2 t e ÝÑ F 1 pF 2 tq).
For any term G : o Ñ o, we define G n for all n ě 0 by taking G 0 " I and G n`1 " K G G n . For any ground term t, G n t behaves as G p. . . pG looomooon n pItqq . . .q and in particular B n X b n ùñ X. For all n ě 0, we have:

Z a n ÝÑ F B n´1 C n b ÝÑ B n´1 pC n Xq b n´1 c n ùñ X.
Example 4. We present a tree T U proposed by Urzyczyn which exemplify the full expressivity of order-2 schemes (see Section IV). The tree T U has directions in t p, q, ‹ u. A word over t p, q u is well bracketed if it has as many opening brackets as closing brackets and if for every prefix the number of opening brackets is not smaller than the number of closing brackets. The language U is defined as the set of words of the form w‹ n where w is a prefix of a well-bracketed word and n is equal to |w| ´|u| `1 where u is the longest suffix of w which is well-bracketed. In other words, n equals 1 if w is well-bracketed, and otherwise it is equal to the index of the last unmatched opening bracket plus one.

For instance, the words pqpppqq ‹ ‹ ‹ ‹ and pqpqpq‹ belong to U . The tree T U is simply PrefpU q. The following scheme

S U generates T U . Z e ÝÑ G pH Xq F ϕ x y p ÝÑ F pF ϕxq y pHyq G z p ÝÑ F G z pHzq F ϕ x y q ÝÑ ϕ pH yq G z ‹ ÝÑ X F ϕ x y ‹ ÝÑ x H u ‹ ÝÑ u with Z, X : o, G, H : o Ñ o and F : po Ñ o, o, oq.
To better explain the inner workings of this scheme, let us introduce some syntactic sugar. With every integer, we associate a ground term by letting 0 " X and, for all n ě 0, n `1 " H n. With every sequence rn 1 . . . n ℓ s of integers, we associate a term of type o Ñ o by letting r s " G and rn 1 . . . n ℓ n ℓ`1 s " F rn 1 . . . n ℓ s n ℓ`1 . Finally we write prn 1 . . . n ℓ s, nq to denote the ground term rn 1 . . . n ℓ s n.

The scheme can be revisited as follows (note that the two rules labelled by p are now merged):

Z e ÝÑ
‹ ÝÑ n ℓ ‹ n ℓ
ÝÑ 0. Hence, as expected, the number of ‹ symbols is equal to 1 if w is well-bracketed (i.e. ℓ " 0), and otherwise it is equal to the index of the last unmatched opening bracket plus one.

F. Collapsible Pushdown Automata

Fix a finite stack alphabet Γ and a distinguished bottomof-stack symbol K R Γ. An order-1 stack is a sequence K, a 1 , . . . , a ℓ P KΓ ˚which is denoted [Ka 1 . . . a ℓ ] 1 . An order-k stack (or a k-stack), for k ą 1, is a non-empty sequence s 1 , . . . , s ℓ of order-pk ´1q stacks which is written [s 1 . . . s ℓ ] k . For convenience, we may sometimes see an element a P Γ as an order-0 stack, denoted [a] 0 . We denote by Stacks k the set of all order-k stacks and Stacks " Ť kě1 Stacks k the set of all higher-order stacks. The height of the stack s denoted | s | is simply the length of the sequence. We denote by ordpsq the order of the stack s.

A substack of an order-1 stack

[Ka 1 . . . a h ] 1 is a stack of the form [Ka 1 . . . a h 1 ] 1 for some 0 ď h 1 ď h. A substack of an order-k stack [s 1 . . . s h ] k , for k ą 1 is either a stack of the form [s 1 . . . s h 1 ] k with 0ăh 1 ď h or a stack of the form [s 1 . . . s h 1 s 1 ] k with 0 ď h 1 ď h ´1 and s 1 a substack of s h 1 `1. We denote by s Ď s 1 the fact that s is a substack of s 1 .
In addition to the operations push a 1 and pop 1 that respectively pushes and pops a symbol in the topmost order-1 stack, one needs extra operations to deal with the higherorder stacks: the pop k operation removes the topmost orderk stack, while the push k duplicates it.

For an order-n stack s " [s 1 . . . s ℓ ] n and an order-k stack t with 0 ď k ă n, we define s `t as the order-n stack obtained by pushing t on top of s:

s `t " " [s 1 . . . s ℓ t] n if k " n ´1, [s 1 . . . ps ℓ `tq] n otherwise.
We first define the (partial) operations pop i and t op i with i ě 1: t op i psq returns the top pi ´1q-stack of s, and pop i psq returns s with its top pi ´1q-stack removed. Formally, for an order-n stack [s 1 ¨¨¨s ℓ`1 ] n with ℓ ě 0

t op i psq " " s ℓ`1 if i " n t op i ps ℓ`1 q if i ă n pop i psq " " [s 1 ¨¨¨s ℓ ] n if i " n and ℓ ě 1 [s 1 ¨¨¨s ℓ pop i ps ℓ`1 q] if i ă n
By abuse of notation, we let t op ordpsq`1 psq " s. Note that pop i psq is defined if and only if the height of t op i`1 psq is strictly greater than 1. For example

pop 2 p[[K a b] 1 ] 2 q is undefined.
We now introduce the operations push i with i ě 2 that duplicates the top pi ´1q-stack of a given stack. More precisely, for an order-n stack s and for 2 ď i ď n, we let push i psq " s `t op i psq.

The last operation, push a 1 pushes the symbol a P Γ on top of the top 1-stack. More precisely, for an order-n stack s and for a symbol a P Γ, we let push a 1 psq " s `[a] 0 . Example 5. Let s be the order-3 stack of height 2 given by s

" [[[Kbaac] 1 [Kbb] 1 [Kbcc] 1 [Kcba] 1 ] 2 [[Kbaa] 1 [Kbc] 1 [Kbab] 1 ] 2 ] 3 . Then t op 3 psq is the 2-stack [[Kbaa] 1 [Kbc] 1 [Kbab] 1 ] 2 and pop 3 psq is the stack s 1 " [[[Kbaac] 1 [Kbb] 1 [Kbcc] 1 [Kcba] 1 ] 2 ] 3 . Note that pop 3 ppop 3 psqq is undefined. Then push 2 ps 1 q is the stack [[[Kbaac] 1 [Kbb] 1 [Kbcc] 1 [Kcba] 1 [Kcba] 1 ] 2 ] 3 and push c 1 ps 1 q " [[[Kbaac] 1 [Kbb] 1 [Kbcc] 1 [Kcbac] 1 ] 2 ] 3 .
We now define a richer structure of higher-order stacks where we allow links. Intuitively, a stack with links is a higher-order stack in which any symbol may have a link that points to an internal stack below it. This link may be used later to collapse part of the stack.

Order-n stacks with links are order-n stacks with a richer stack alphabet. Indeed, each symbol in the stack can be either an element a P Γ (i.e. not being the source of a link) or an element pa, ℓ, hq P Γ ˆt2, ¨¨¨, nu ˆN (i.e. being the source of an ℓ-link pointing to the h-th pℓ ´1q-stack inside the topmost ℓ-stack). Formally, order-n stacks with links over alphabet Γ are defined as order-n stacks 1 over alphabet Γ Y Γ ˆt2, ¨¨¨, nu ˆN. Example 6. The stack s below is an order-3 stack with links

[[[Kbaac] 1 [Kbb] 1 [Kbcpc, 2, 2q] 1 ] 2 [[Kbaa] 1 [Kbc] 1 [Kbpa, 2, 1qpb, 3, 1q] 1 ] 2 ] 3 .
To improve readability when displaying n-stacks in examples, we shall explicitly draw the links rather than using stacks symbols in Γ ˆt2, ¨¨¨, nu ˆN. For instance, we shall rather represent s as follows:

[[[Kbaac] 1 [Kbb] 1 [Kbcc] 1 ] 2 [[Kbaa] 1 [Kbc] 1 [Kbab] 1 ] 2 ] 3
In addition to the previous operations pop i , push i and push a

1 , we introduce two extra operations: one to create links, and the other to collapse the stack by following a link. Link creation is made when pushing a new stack symbol, and the target of an ℓ-link is always the pℓ ´1q-stack below the topmost one. Formally, we define push a,ℓ 1 psq " push pa,ℓ,hq 1

where we let h " |t op ℓ psq| ´1 and require that h ą 1.

The collapse operation is defined only when the topmost symbol is the source of an ℓ-link, and results in truncating the topmost ℓ-stack to only keep the component below the target of the link. Formally, if t op 1 psq " pa, ℓ, hq and s " s 1 `rt 1 ¨¨¨t k s ℓ with k ą h we let collapsepsq " s 1 `rt 1 ¨¨¨t h s ℓ .

For any n, we let Op n pΓq denote the set of all operations over order-n stacks with links.

Example 7. Let s " [[[ K a] 1 ] 2 [[ K] 1 [ K a] 1 ] 2 ] 3 . We have push b,2 1 psq " [[[ K a] 1 ] 2 [[ K] 1 [ K a b] 1 ] 2 ] 3 collapse ppush b,2 1 psqq " [[[ K a] 1 ] 2 [[ K] 1 ] 2 ] 3 push c,3 1 ppush b,2 1 psqq loooooooooooomoooooooooooon θ " [[[ K a] 1 ] 2 [[ K] 1 [ K a b c] 1 ] 2 ] 3 .
Then push 2 pθq and push 3 pθq are respectively

[[[ K a] 1 ] 2 [[ K] 1 [ K a b c] 1 [ K a b c] 1 ] 2 ] 3 and [[[ K a] 1 ] 2 [[ K] 1 [ K a b c] 1 ] 2 [[ K] 1 [ K a b c] 1 ] 2 ] 3 .
We have collapse ppush 2 pθqq " collapse ppush 3 pθqq "

collapsepθq " [[[ K a] 1 ] 2 ] 3 .
An order-n (deterministic) collapsible pushdown automaton (n-CPDA) is a 5-tuple A " x Σ, Γ, Q, δ, q 0 y where Σ is an input alphabet containing a distinguished symbol denoted e, Γ is a stack alphabet, Q is a finite set of control states, q 0 P Q is the initial state, and δ : Q ˆpΓ Y tKuq ˆΣ Ñ Q ˆOp n pΓq is a (partial) transition function such that, for all q P Q and γ P Γ, if δpq, γ, eq is defined then for all a ‰ e, δpq, γ, aq is undefined, i.e. if some e-transition can be taken, then no other transition is possible. We require δ to respect the convention that K cannot be pushed onto or popped from the stack.

Let A " x Σ, Γ, Q, δ, q 0 y be an n-CPDA. A configuration of an n-CPDA is a pair of the form pq, sq where q P Q and s is an n-stack with link over Γ; we call pq 0 , rr¨¨¨rKs 1 ¨¨¨s n´1 s n q the initial configuration. It is then natural to associate with A a deterministic LTS denoted L A " x D, r, Σ, p a ÝÑq aPΣ y and defined as follows. We let D be the set of all configurations of A and r be the initial one. Then for all a P Σ and all pq, sq, pq 1 , s 1 q P D we have pq, sq a ÝÑ pq 1 , s 1 q if and only if δpq, t op 1 psq, aq " pq 1 , opq and s 1 " oppsq.

The tree generated by an n-CPDA A, denoted Tree K pAq, is simply the tree Tree K pL A q of its LTS.

III. FROM RECURSION SCHEMES TO COLLAPSIBLE PUSHDOWN AUTOMATA

In this section, we present a translation of schemes into CPDA. This translation generalizes at all orders the order-2 translation of [A4]. The translation from [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] assumes a normal form for the schemes but up to these normalisations, the CPDA obtained is the same as the one in [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. Our contributions are to work direclty on schemes without normalisation and more importantly to prove the correctness of the translations without using game semantics as an intermediary tool as in [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. Note that the converse translation from [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] (from CPDA into scheme) does not use game semantics and is therefore not presented here.

We construct, for any labeled recursion scheme S, a collapsible pushdown automaton A of the same order defining the same tree as S -i.e. Tree K pSq " Tree K pAq. To simplify the presentation, we assume that S does not contain any silent productions rule (i.e. production rule labeled by e). If S were to contain silent transitions, we would treat the symbol e as any other symbol 2 in Σ. For the rest of this section, we fix a labeled recursion scheme x Σ, N, R, Z, K y of order n ě 1 without silent transitions.

The automaton A has a distinguished state, denoted q ‹ , and with the configurations of the form pq ‹ , sq we will associate a ground term over N denoted by rr s ss. Other configurations correspond to internal steps of the simulation and are only the source of silent transitions. To show that the two LTS define the same trees, we will establish that, for any reachable configuration of the form pq ‹ , sq and for any a P Σ, the following holds:

' if pq ‹ , sq ae Ý Ñ A pq ‹ , s

Ñ

A pq ‹ , s 1 q and rr s 1 ss " t. Hence, the main ingredient of the construction is the partial mapping rr ¨ss associating with any order-n stack a ground term over N . The main difficulty is to guarantee that any rewriting rule of S applicable to the encoded term rr s ss can be simulated by applying a sequence of stack operations to s. In Section III-A, we present the mapping rr ¨ss together with its basic properties; in Section III-B, we give the definition of A and prove the desired properties.

To simplify the presentation we assume, without loss of generality, that all productions starting with a non-terminal A have the same left-hand side (i.e. they use the same variables in the same order) and that two productions starting with different non-terminals do not share any variables. 2 Formally, one labels all silent production rules of S by a fresh symbol e to obtain a labeled scheme S 1 without silent transitions. The construction presented in this section produces an automaton A 1 such that Tree K pS 1 q " Tree K pA 1 q. The automaton A obtained by replacing all e-labeled rules of A by e is such that Tree K pSq " Tree K pAq.

Hence a variable x P V appears in a unique left-hand side A x 1 . . . , x ̺pAq and we denote by rkpxq the index of x in the sequence x 1 ¨¨¨x ̺pAq (i.e. x " x rkpxq ).

Throughout the whole section, we will illustrate definitions and constructions using as a running example the order-2 scheme S U generating the tree T U of Example 4.

A. Stacks Representing Terms.

The stack alphabet Γ consists of the initial symbol and of the right-hand sides of the rules in R and their argument subterms, i.e.

Γ def " t Z u Y Ť F x1¨¨¨x ̺pxq a
ÝÑ e t e u Y ASubspeq. For the scheme S U , one gets Γ " tx, y, z, u, ϕu Y t Z , G pH Xq , H X , X , F pF ϕ xq y pHyq , F ϕ x , Hy , F G z pHzq , G , Hz , ϕ pHyqu. Notation 1. For ϕ P V Y N , a ϕ-stack designates a stack whose top symbol starts with ϕ. By extension a stack s is said to be an N -stack (resp. a V -stack) if it is a ϕ-stack for some ϕ P N (resp. ϕ P V ).

In order to represent a term in TermspN q, a stack over Γ must be well-formed, i.e. it must satisfy some syntactic conditions.

Definition 1 (Well-formed stack). A non-empty stack of order-n over Γ is well-formed if every non-empty substack r of s satisfies the following two conditions:

' if t op 1 prq is not equal to Z nor to K then pop 1 prq is
an A-stack for some A P N and t op 1 prq belongs to an A-production rule, ' if t op 1 prq is of type τ of order k ą 0 then t op 1 prq is the source of an pn ´k `1q-link and collapseprq is a ϕ-stack for some variable ϕ P V of type τ . We denote by WStacks the set of all well-formed stacks.

Example 8. For the scheme S U , the following order-2 stacks are well-formed. Notation 2. We write s :: t for s P WStacks and t P Γ to mean that if t belongs to the r.h.s. of a production starting with A P N then s is an A-stack. In particular, if s P WStacks then pop 1 psq :: t op 1 psq. We denote by CStacks the set of such s :: t, and define the size of an element s :: t as the pair p|s|, |t|q where |s| denotes the number of stack symbols in s and |t| the length of the term t. When comparing sizes, we use the standard lexicographic (total) order over N ˆN.

In Definition 4, we will associate, with any well-formed stack s, a ground term over N that we refer to as the value of s. To define this value, we first associate, with any element s :: t in CStacks, a value denoted rr s :: t ss. This value is a term over N of the same type as t. Intuitively, it is obtained by replacing the variables appearing in the term t by values encoded in the stack s, and one should therefore understand rr s :: t ss as the value of the term t in the context (or environment) of s. See Remark 3 below for natural connections with Krivine machine. Definition 2. For all ϕ P V Y N , all k P r1, ̺pϕqs and all ϕ-stack s P WStacks, we define an element of CStacks, denoted Arg k psq, representing the k-th argument of the term represented by s. More precisely if the top symbol of s is ϕ t 1 ¨¨¨t ℓ , we take:

" Arg k psq " pop 1 psq :: Let us provide some intuitions regarding the definition of rr s :: t ss. Unsurprisingly rr s :: t ss is defined by structural induction on t, and the cases for the application and the non-terminal symbols are straightforward. It remains to consider the case where t is a variable x appearing in rkpxq-th position in the left-hand side A x 1 ¨¨¨x ̺pAq . As s :: t P CStacks, t op 1 psq is of the form At 1 . . . t ℓ for some ℓ ď ̺pAq. Note that ℓ is not necessarily equal to ̺pAq meaning that some arguments of A might be missing. There are now two cases -that correspond to the two cases in the definition of Arg k psq -depending on whether x references to one of the t i 's (i.e. rkpxq ď ℓ) or one of the missing arguments (i.e. rkpxq ą ℓ):

t k if k ď ℓ,
' If rkpxq ď ℓ then the term associated with x in s is equal to the term associated with t rkpxq in pop 1 psq, i.e. rr s :: x ss " rr pop 1 psq :: t rkpxq ss. ' If rkpxq ą ℓ then the term rr s :: x ss is obtained by following the link attached to t op 1 psq. Recall that, as s is a well-formed stack and t op 1 psq is not of ground type (as ℓ ă ̺pAq), there exists a link attached to t op 1 psq. Moreover, collapsepsq, the stack obtained by following the link, has a top-symbol of the form ϕ t 1 1 . . . t 1 m for some ϕ P V and m ě 0. Intuitively, t 1 i corresponds to the pℓ `iq-th argument of A. If rkpxq belongs to rℓ `1, ℓ `ms then the term rr s :: x ss is defined to be the term rr pop 1 pcollapsepsqq :: t 1 rkpxq´ℓ ss. If rkpxq is greater than ℓ `m then the link attached to the top symbol of collapsepsq is followed and the process is reiterated. As the size of the stack strictly decreases at each step this process terminates. Now, if s is a well-formed ϕ-stack, its value is obtained by applying the value of ϕ in the context of pop 1 psq to the value of all its ̺pϕq arguments. This leads to the following formal definition. rr s 1 ss " rr s 2 ss " F G pH Xq pHpHpHpH Xqqqq rr s 3 ss " HpHpHpHpH Xqqq

The following lemma states the basic properties of the encoding rr ¨ss and Arg k p ¨q.

Lemma 1. We have the following properties:

1) For all ϕ-stacks s P WStacks with ϕ P V Y N of type τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o and for all k P r1, ̺pϕqs, Arg k psq is equal to some r :: t P CStacks with t of type τ k . 2) For all s :: t P CStacks with t : τ P Γ, rr s :: t ss is a term in Terms τ pN q. 3) For all s P WStacks, rr s ss belongs to Terms o pN q.

We conclude with two fundamental properties of Arg k p¨q that will allow us to simulate the rewriting of the scheme using stack operations and finite memory.

The first property is that the arguments represented by a well-formed stack are not modified when performing a push k operation. More precisely, for all ϕ-stacks s P WStacks with ϕ P N Y V , rr Arg ℓ ppush k psqq ss " rr Arg ℓ psq ss for all ℓ P r1, ̺pϕqs and all k P r2, ms. This follows (by letting r " t op k psq) from the following slightly more general result. Lemma 2. Let k P r2, ms and let s " s 1 `t op k psq P WStacks. For all non-empty ϕ-stacks r Ď t op k psq, rr Arg ℓ ps 1 `rq ss " rr Arg ℓ ps `rq ss for all ℓ P r1, ̺pϕqs.

The next property will later be used to prove that any rewriting step can be simulated by a finite number of transitions in the automaton. Lemma 3. Let s be a ϕ-stack in WStacks for some ϕ : τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o in V YN and let ℓ P r1, ̺pϕqs with τ ℓ of order k ą 0. If Arg ℓ psq is equal to r :: t P CStacks with t starting with ψ P N YV then pop n´k`1 psq " pop n´k`1 prq, | t op n´k`1 psq | ą | t op n´k`1 prq |.

B. Simulating the LTS of S on Stacks

As an intermediate step, we define an LTS M over wellformed stacks and we prove that it generates the same tree as S (i.e. Tree K pMq " Tree K pSq). From M, a CPDA generating Tree K pMq is then defined at the end of this section.

We let M " x WStacks, r. The first line of the definition of ÝÑ M corresponds to the case of an N -stack. To simulate the application of a production rule A x 1 ¨¨¨x n a ÝÑ e on the term encoded by an A-stack s, we simply push the right-hand side e of the production on top of s. The correctness of this rule directly follows from the definition of rr ¨ss. Doing so, a term starting with a variable may be pushed on top of the stack, e.g. when applying the production rule F ϕ x y q ÝÑ ϕ pH yq. Indeed, we need to retrieve the value of the head variable in order to simulate the next transition of S: the second and third lines of the definition are normalisation rules that aim at replacing the variable at the head of the top of the stack (for instance, in the 5th stack of Example 10 the variable ϕ) by its definition (hence not changing the value of the associated term). By iterative application, we eventually end up with an N -stack encoding the same term and we can apply again the first rule. From M we now define an n-CPDA A " x Σ, Γ, Q, δ, q 0 y generating the same tree as M. The set of states Q is equal to t q 0 , q 1 , . . . , q ̺pSq , q ˚u where ̺pSq denotes the maximal arity appearing in S. Intuitively the initial state q 0 is only used to go from pq 0 , r. . . r K s 1 . . .s n q to pq ˚, r. . . r KZ s 1 . . .s n q; the state q ˚is used to mark Nstacks; for k P r1, ̺pSqs, the state q k is used to the compute Arg k p¨¨¨q. The transitions are given below.

' δpq 0 , K, eq " pq ˚, push Z 1 q, ' If t starts with F P N and F x 1 ¨¨¨x ̺pF q a ÝÑ e P R:

δpq ˚, t, aq " pq ˚, push e 1 q if e starts with a symbol in N , -δpq ˚, t, aq " pq rkpxq , idq if e is a variable x : o (here id is the identity function), -δpq ˚, t, aq " pq rkpxq , push e 1 ; push n´k`1 ; pop 1 q if e starts with a variable x of order k ą 0.

' If t is a term of the form ϕ t 1 ¨¨¨t ℓ for some ϕ P V YN :

δpq k , t, eq " pq rkpt k q , pop 1 ; push t k 1 q if k ď ℓ and t k : o, -δpq k , t, eq " pq rkpt k q , pop 1 ; push t k ,n´h`1

1 q if k ď ℓ and t k has order h ą 0, -δpq k , t, eq " pq k´ℓ , collapseq if k ą ℓ.
where, for all t P Γ, q rkptq designates the state q rkpxq if t starts with a variable x and q ˚otherwise, and op 1 ; op 2 means applying op 1 followed by op 2 . An equivalent CPDA using only one operation per transition may be obtained by adding intermediary states.

Theorem 1. For every labeled recursion scheme S of ordern, there is an n-CPDA A that generates the same tree. Moreover, the number of states in A is linear in the maximal arity appearing in S, and its alphabet is of size linear in the one of S3 . Remark 3. In [START_REF] Salvati | Krivine machines and higherorder schemes[END_REF], the authors use Krivine machines [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF] as an abstract model to represent the sequence of rewriting of a scheme4 . A Krivine machine computes the weak head normal form of a λY -term, using explicit substitutions (called here environments). Environments are functions assigning closures to variables, and closures themselves are pairs consisting of a term and an environment. This mutually recursive definition is schematically represented by the grammar C :" pt, ρq and ρ :" ∅ | ρrx Ñ Cs where t is an term of the λY -calculus with free-variable and ∅ designates the empty environment. The λY -term t C represented by a closure C " pt, ρq is inductively defined as t in which every occurrence of a free variable x is replaced by the term t ρpxq .

A pair s :: t (cf. Notation 2) can be seen as a closure5 pt, ρq where ρpxq is defined for all variables x occurring in t by ρpxq " Arg rkpxq psq. With this view in mind and up to the translation of schemes into equivalent λY -terms, the LTS M faithfully simulates the Krivine machine presented in [START_REF] Salvati | Krivine machines and higherorder schemes[END_REF]. Note that the correspondence is facilitated by the use of labeled schemes.

This remark also allows us to inherit the simplifications of [START_REF] Salvati | Krivine machines and higherorder schemes[END_REF] for the decidability of CPDA parity games.

IV. SAFE HIGHER-ORDER RECURSION SCHEMES

In this section, we consider a syntactic subfamily of recursion schemes called the safe recursion schemes. The safety constraint was introduced in [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF] but was already implicit in the work of Damm [START_REF] Damm | The IO-and OI-hierarchies[END_REF] (see also [7, p. 44] for a detailed presentation). This restriction constrains the way variables are used to form argument subterms of the rules' right-hand sides.

Definition 5 ([10]

). A recursion scheme is safe if no right-hand side contains an argument-subterm of order k containing a variable of order strictly less than k.

For instance, the scheme in Example 3 is safe. On the other hand, the scheme S U of Example 4 is not because the production F ϕ x y p ÝÑ F pF ϕxqypHyq contains in its right-hand side the argument subterm F ϕx : o Ñ o of order-1 which contains the variable x : o of order-0. Urzyczyn conjectured that (a slight variation of) the tree T U generated by S U , though generated by a order-2 scheme, could not be generated by any safe scheme. This conjecture was recently proved by Parys [START_REF] Parys | On the Significance of the Collapse Operation[END_REF].

Remark 4. In [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF], [START_REF] Knapik | Higher-Order Pushdown Trees Are Easy[END_REF], the notion of safety is only defined for homogeneous schemes. A type is said to be homogeneous if it is either ground or equal to τ 1 Ñ ¨¨¨Ñ τ n Ñ o where the τ i 's are homogeneous and ordpτ 1 q ě ¨¨¨ě ordpτ n q. By extension, a scheme is homogeneous if all its non-terminal symbols have homogeneous types. For instance po Ñ oq Ñ o Ñ o is an homogeneous type whereas o Ñ po Ñ oq Ñ o is not. We will see in Proposition 2 that dropping the homogeneity constraint in the definition of safety does not change the family of generated trees.

A. Safety and the Translation from Schemes to CPDA In [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF], [START_REF] Knapik | Higher-Order Pushdown Trees Are Easy[END_REF], the motivation for considering the safety constraint was that safe schemes can be translated into a subfamily of the collapsible automata, namely higher-order pushdown automata. An order-k pushdown automaton is an order-k CPDA that does not use the collapse operation (hence, links are useless).

Theorem 2 below shows that the translation of recursion schemes into collapsible automata presented in Section III, when applied to a safe scheme, yields an automaton in which links are not really needed. Obviously the automaton performs the collapse operations but whenever it is applied to an order-k link its target is the pk ´1q-stack below the top pk ´1q-stack. Hence any collapse operation can safely be replaced by a pop k operation. In doing so, we re-obtain the translation of safe (homogeneous) schemes into higher-order pushdown automata presented in [START_REF] Knapik | Higher-Order Pushdown Trees Are Easy[END_REF]. Definition 6. A CPDA is link-free if for every configuration pp, sq reachable from the initial configuration and for every transition δpp, t op 1 psq, aq " pq, collapseq, we have collapsepsq " pop ℓ psq where ℓ is the order of the link attached to t op 1 psq.

Theorem 2. The translation of Section III applied to a safe recursion scheme yields a link-free collapsible automaton. Sketch: We present the ingredients of the proof only at order-2. For the general case, the ideas are similar but lead to more technicalities.

Let us first introduce some notations. Let pq, s " rs 1 . . . s m s 2 q be a configuration of A reachable from the initial configuration. For i P r1, ms and j P r1, |s i |s, we denote by rpi, jq, tpi, jq and opi, jq respectively the j-th symbol of stack s i , the target (if defined) in r1, i ´1s of its link and the order (if defined) of this link. By definition of A, tpi, jq and opi, jq are defined iff rpi, jq is a term of order k ą 0 and in this case opi, jq is equal to 2 ´k `1 Moreover for i P r2, ms, we let ℓ i be the smallest index at which s i´1 and s i have a different symbol (or

|s i | `1 if no such index exists).
The stack s satisfies the following properties: 1) for all i P r1, |s 1 |s, tp1, iq is undefined;

2) for all i P r2, ms, ℓ i ď |s i´1 | and for all i P r2, m´1s, ℓ i ď |s i |; 3) for all i P r2, ms and 1 ď j ă ℓ i , tpi, jq " tpi ´1, jq; 4) for all i P r2, ms with ℓ i ď |s i |, rpi, ℓ i q does not contain a variable of order 0 and is an argument subterm of rpi ´1, ℓ i q and if rpi, ℓ i q is of order 1 then tpi, ℓ i q " i ´1; 5) for all i P r2, ms with j

P rℓ i `1, |s i |s, tpi, jq is undefined; 6) if m ě 2 then ℓ m " |s m | `1 iff t op 1 psq " ϕt 1 . . . t h ,
q " q k for some k P r1, hs such that ordpt k q " 1. These properties are proved by induction on the length of the shortest path in the LTS from the initial configuration to pq, sq and by inspection of the transitions of A.

Inspecting the transitions of A, a collapse operation can only be performed if q " q k and t op 1 psq " ϕ t 1 . . . We get the following corollary extending (by dropping the homogeneity assumption) a previous result from [START_REF] Knapik | Higher-Order Pushdown Trees Are Easy[END_REF].

Corollary 1. Order-k safe schemes and order-k pushdown automata generate the same trees.

B. Damm's View of Safety

The safety constraint may seem unnatural and purely adhoc. Inspired by the constraint of derived types of Damm, we introduce a more natural constraint, Damm-safety, which leads the same family of trees [START_REF] Damm | The IO-and OI-hierarchies[END_REF].

Damm-safety syntactically restricts the use of partial application: in any argument subterm of a right-hand side if one argument of some order-k is provided then all arguments of order-k must also be provided. For instance if ϕ : po Ñ oq Ñ po Ñ oq Ñ o Ñ o Ñ o, f : o Ñ o and c : o, the terms ϕ, ϕ f f and ϕ f f c c can appear as argument subterms in a Damm-safe scheme but ϕ f and ϕ f f c are forbidden.

Definition 7 ([6]

). A recursion scheme is Damm-safe if it is homogeneous and all argument-subterms appearing in a right hand-side are of the form ϕ t 1 ¨¨¨t k with ϕ :

τ 1 Ñ ¨¨¨Ñ τ n Ñ o and either k " 0, k " n or ordpτ k q ą ordpτ k`1 q.
As in Damm-safe scheme all argument subterms of an argument subterm of order-k appearing in a right-hand side have at least order-k, it is easy to see that Damm-safety implies the safety constraint. However, the safety constraint, even when restricted to homogeneous schemes, is less restrictive than Damm-safety. Consider for instance a variable x : o and non-terminals G : o Ñ o Ñ o and C : o, then G x cannot appear as an argument-subterm in a safe scheme but G C can. As G C does not satisfy Damm-safety constraint, safety is syntactically more permissive than Damm-safety.

However unsurprisingly, any safe scheme can be transformed into an equivalent Damm-safe scheme of the same order. The transformation consists in converting the safe scheme into a higher-order pushdown automaton (Corollary 1) and then converting this automaton back to a scheme using the translation of [START_REF] Knapik | Higher-Order Pushdown Trees Are Easy[END_REF]. In fact, this translation of higher-order pushdown automata into safe schemes produces Damm-safe schemes.

Proposition 2. Damm-safe schemes are safe and for every safe scheme, there exists a Damm-safe scheme of the same order generating the same tree.

V. EFFECTIVE SELECTION

Let ϕpX 1 , ¨¨¨, X ℓ q be a monadic second order (MSO) formula with ℓ second-order free variables, and let t be a term over a ranked alphabet Σ. The MSO selection problem is to decide whether the formula DX 1 . . . DX ℓ ϕpX 1 , ¨¨¨, X ℓ q holds in t, and in this case to give a term t ϕ over the ranked alphabet Ξ " Σ ˆt0, 1u ℓ (we take ̺pa, pb 1 , . . . , b ℓ qq " ̺paqq such that the following holds:

1) t " πpt ϕ q where π is the alphabetical morphism from Ý Ñ Ξ to Ý Ñ Σ defined by πppa, bqq " a for a P Σ with ̺paq " 0 and πppa, bq i q " a i for a P Σ with ̺paq ą 0 and i P r1, ̺paqs. Intuitively, t ϕ is obtained by marking every node in t by a vector of ℓ booleans. Indeed for all non-leaf node u, there exists a unique element pc, bq P Ξ such that for all x P ÝÝÑ pc, bq, ux is in t ϕ . The tuple b P t0, 1u ℓ is the label of the node u of t. The label of a non-leaf node u of t is denoted b u 2) The formula ϕpX 1 Ð U 1 , . . . , X ℓ Ð U ℓ q holds in t where @1 ď i ď ℓ, U i " tu P t | b u piq " 1u. Intuitively, the second point states that this marking exhibits a valuation of the X i for which ϕ holds in t. We refer to t ϕ as a selector for ϕ in t.

Let R be a class of generators of terms. We say that R has the effective MSO selection property if there is an algorithm that transforms any pair pR, ϕpX 1 , . . . , X ℓ qq with R P R into some R ϕ P R (if exists) such that the term generated by R ϕ is a selector for ϕ in the term generated by R.

Theorem 3. Labeled recursion schemes as well as CPDA have the effective MSO selection property.

The proof of Theorem 3 is highly non-trivial and requires a precise analysis of winning strategies in parity games played over terms generated by CPDA (the key argument is that winning strategies can be embedded into the CPDA generating the term). We do not believe that a proof of the statement for labeled recursion schemes can be obtained without using an automaton model, and we think that it shows the usefulness of CPDA in the study of logical properties of schemes. Remark 5. A similar statement for safe schemes can be deduced from [START_REF] Fratani | Automates à piles de piles[END_REF], [START_REF] Carayol | Automates infinis, logiques et langages[END_REF], [START_REF] Carayol | Positional strategies for higherorder pushdown parity games[END_REF]. However the machinery for general schemes is much more involved.

In [START_REF] Broadbent | Recursion schemes and logical reflexion[END_REF] a much weaker notion, MSO-reflectivity, was considered. A class of generators of terms is MSO-reflective if it has the effective MSO selection property for those formula ϕpXq of the form ϕpXq " x P X ô ψpxq where ψpxq is an MSO formula with a single first-order free variable (note that in this case, there is a unique valuation of X that makes ϕpXq holds). The main result of [START_REF] Broadbent | Recursion schemes and logical reflexion[END_REF] follows from Theorem 3.

Corollary 2. Labeled recursion schemes as well as CPDA have the effective MSO-reflectivity property. Remark 6. A variant of selection [START_REF] Rabinovich | Selection and uniformization problems in the monadic theory of ordinals: A survey[END_REF] ask for existence of a formula ψpX 1 , . . . X ℓ q that is a selector for ϕpX 1 , . . . X ℓ q in t in the following sense. Either neither of the formulas DX 1 . . . DX ℓ ϕpX 1 , ¨¨¨, X ℓ q and DX 1 . . . DX ℓ ψpX 1 , ¨¨¨, X ℓ q holds in t or ψ defines a unique tuple pU 1 , ¨¨¨, U ℓ q and this tuple also satisfies ϕ. In [START_REF] Carayol | Choice functions and well-orderings over the infinite binary tree[END_REF] it is shown that a selector does not always exist in general, and the counter-example is for a tree generated by a (safe) recursion scheme.

A degenerated version of selection is model-checking.

Theorem 1 together with a careful analysis of the complexity of parity games on CPDA lead the same complexity as in [START_REF] Kobayashi | A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes[END_REF].

Corollary 3. The µ-calculus model-checking of trees generated by recursion schemes is polynomial under the assumption that the arity of types and the formula are bounded above by a constant.

APPENDIX

A. Proofs Omitted in Section II 1) Labeled Recursion Schemes vs (Classical) Recursion Schemes: . We recall the notion of recursion schemes as it is usually considered in the literature (see e.g. [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]).

For each type τ , we assume an infinite set V τ of variables of type τ , such that V τ1 and V τ2 are disjoint whenever τ 1 " τ 2 , and we write V for the union of those sets V τ as τ ranges over types. We use letters x, y, ϕ, ψ, χ, ξ, . . . to range over variables.

A (deterministic) recursion scheme is a 5-tuple S " x A, N, R, Z, K y where ' A is a ranked alphabet of terminals and K is a distinguished terminal symbol of arity 0 (and hence of ground type) that does not appear in any production rule,

' N is a finite set of typed non-terminals; we use upper-case letters F, G, H, . . . to range over non-terminals, ' Z P N is a distinguished initial symbol of type o which does not appear in any right-hand side of a production rule, ' R is a finite set of production rules, one for each non-terminal F : pτ 1 , ¨¨¨, τ n , oq, of the form

F x 1 ¨¨¨x n Ñ e
where the x i are distinct variables with x i : τ i for i P r1, ns and e is a ground term in TermsppAztKuq Y pN ztZuq Y t x 1 , . . . , x n uq. Note that the expressions on either side of the arrow are terms of ground type.

As for labelled schemes, the order of a recursion scheme is defined to be the highest order of (the types of) its nonterminals.

A recursion scheme S induces a rewriting relation, denoted Ñ S , over TermspAYN q. Informally, Ñ S replaces any ground subterm F t 1 . . . t ̺pF q starting with a non-terminal F by the right-hand side of the production rule F x 1 ¨¨¨x n Ñ e in which the occurrences of the "formal parameter" x i are replaced by the actual parameter t i for i P r1, ̺pF qs.

The term M rt{xs obtained by replacing a variable x : τ by a term t : 6 by induction on M by taking ϕrt{xs " ϕ for ϕ ‰ x P A Y N Y V , xrt{xs " t and pt 1 t 2 qrt{xs " t 1 rt{xs t 2 rt{xs.

τ over A Y N in a term M over A Y N Y V is defined
The rewriting system Ñ S is defined by induction using the following rules:

' (Substitution) F t 1 ¨¨¨t n Ñ S ert 1 {x 1 , ¨¨¨, t n {x n s where F x 1 ¨¨¨x n Ñ e is a production rule of S. ' (Context) If t Ñ S t 1 then pstq Ñ S pst 1 q and ptsq Ñ S pt 1 sq.
Example 11. Let S be the order-2 recursion scheme with non-terminals tZ : o, H : po, oq, F : ppo, o, oq, oqu, variables tz : o, ϕ : po, o, oqu, terminals A " tf, au of arity 2 and 0 respectively, and the following rewrite rules:

Z Ñ f pH aqpF f q H z Ñ H pH zq F ϕ Ñ ϕ a pF ϕq
The figure below depicts the first rewriting steps of Ñ S starting from the initial symbol Z.

Z f F f H a f f F f a H a f F f H H a f f f F f a a H a f f F f a H H a f F f H H H a
As illustrated above, the relation Ñ S is confluent, i.e. for all ground terms t,t 1 and t 2 , if t Ñ S t 1 and t Ñ S t 2 (here Ñ S denotes the transitive closure of Ñ S ), then there exists t 1 such that t 1 Ñ S t 1 and t 2 Ñ S t 1 . The proof of this statement is similar to proof of the confluence of the lambda-calculus.

Informally the value tree of (or the tree generated by) a recursion scheme S, denoted rr S ss, is a (possibly infinite) term, constructed from the terminals in A, that is obtained as the "limit" of the set of all terms that can obtained by iterative rewriting from the initial symbol Z.

The terminal symbol K : o is used to formally restrict terms over A Y N to their terminal symbols. We define a map p¨q K : TermspA Y N q ÝÑ TermspAq that takes an applicative term and replaces each non-terminal, together with its arguments, by K : o. We define p¨q K inductively as follows, where a ranges over A-symbols, and F over non-terminals in N :

a K " a F K " K pstq K " # K if s K " K ps K t K q otherwise.
Clearly if t P TermspA Y N q is of ground type then t K P TermspAq is of ground type as well.

Terms built over A can be partially ordered by the approximation ordering ď defined for all terms t and t 1 over A by

t ď t 1 if t X p Ý Ñ A ztKuq ˚Ď t 1 .
In other terms, t 1 is obtained from t by substituting some occurrences of K by arbitrary terms over A.

The set of terms over A together with ď form a directed complete partial order. Meaning that any directed subset D of TermspAq (i.e. D is not empty and for all x, y P D, there exists z P D such that x ď z and y ď z) admits a supremum, denoted sup D.

Clearly if s Ñ S t then s K ď t K . The confluence of Ñ S implies that the set t t K | Z Ñ S t u is directed. Hence the value tree of (or the tree generated by) S can be defined as its supremum.

rr S ss " supt t K | Z Ñ S t u.
Example 12. The value tree of the recursion scheme S of Example 11 is:

f f f f f ' a a a a K " sup t K , f K K , f f K a K , . . . u
The following theorem relates both notions of schemes.

Theorem 4. The recursion schemes and the labeled recursion schemes generate the same terms. Moreover the translations are linear and preserves order and arity.

Proof: Let S " x A, N, R, Z, K y be a recursion scheme. We define a labeled recursion scheme S 1 " x Ý Ñ A , N 1 , R 1 , Z, K y generating the term rr S ss. For each terminal symbol f P A, we introduce a non-terminal symbol, denoted f :

o Ñ ¨¨¨Ñ o Ñ loooooooomoooooooon ̺pf q o. The set N 1 of non-terminal symbols of S 1 is N Y tf | f P Au Y tXu
where X is assumed to be a fresh non-terminal. With a term t over A Y N , we associate the term t over N 1 obtained by replacing every occurrence of a terminal symbol f by its nonterminal counterpart f . The production rules R 1 of S 1 are:

tF x 1 ¨¨¨x n e ÝÑ e | F x 1 ¨¨¨x n ÝÑ e P Ru Y tf x 1 ¨¨¨x ̺pf q fi ÝÑ x i | f P A with ̺pf q ą 0 and i P r1, ̺pf qsu Y tc c ÝÑ X | c P A with ̺pcq " 0u
Conversely, let A be ranked alphabet and let S " x Ý Ñ A , N, R, Z, K y be a labeled recursion scheme generating a ranked tree. We define a recursion scheme S 1 " x A, N, R 1 , Z, K y generating the same term as S. The set of production rules of S 1 are defined as follows:

' If F x 1 ¨¨¨x n
e ÝÑ e belongs to R (in this case it is the only rule starting with F ) then F x 1 ¨¨¨x n Ñ e belongs to R 1 .

' If, for some c of arity 0, F x 1 ¨¨¨x n c ÝÑ e belongs to R (in this case it is the only rule starting with F and e starts with a non-terminal that has no rule in R) then F x 1 ¨¨¨x n Ñ c belongs to R 1 .

' If, for some f P A of arity ̺pf q ą 0, F x 1 ¨¨¨x n fi ÝÑ e i belongs to R for all 1 ď i ď ̺pf q, then F x 1 ¨¨¨x n Ñ f e 1 ¨¨¨e ̺pf q belongs to R 1 .

2) Extra Examples of Labeled Recursion Schemes: . Due to space limitation we could only give two examples of labelled recursion schemes in the main body of the paper. We present here some extra example to illustrate the mechanism of labelled recursion schemes as well as their expressive power.

Example 13. Let T 0 be the tree corresponding to the deterministic context-free language Prefpta n b n | n ě 0uq. As it is the case for all prefix-closed deterministic context-free languages (see [A2], [A3] or Theorem 1 at order 1) , T 0 is generated by an order-1 scheme S 0 .

Z a ÝÑ H X H x a ÝÑ H pB zq B x b ÝÑ x H x b ÝÑ x with Z, X : o and H, B : o Ñ o.
The tree generated by S 0 is given below: For all n ě 0, we have:

Z a n ùñ F D n B c ÝÑ D n B X b 2 n ùñ X.
Example 15. At order k `1 ě 1, we can define the tree T exp k " Prefpta n c b exp k pnq | n ě 0uq where we let exp 0 pnq " n and exp k`1 pnq " 2 exp k pnq for k ě 0. We illustrate the idea by giving an order-3 scheme generating We have @n ě 0: Z 2) Proof of Lemma 1: . Lemma 1. We have the following properties:

T exp 2 " Prefpta n c b 2 2 n | n ě 0uq. Z e ÝÑ F D 1 F ψ a ÝÑ F pD 2 ψq D 2 ψ ϕ x e ÝÑ pψpψ ϕqqx B x b ÝÑ x F ϕ c ÝÑ ϕ B X D 1 ψ x e ÝÑ ψ
a n ùñ F D n 2 D 1 c ÝÑ D n 2 D 1 B X b 2 2 n ùñ X. B.
1) For all ϕ-stacks s P WStacks with ϕ P V Y N of type τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o and for all k P r1, ̺pϕqs, Arg k psq is equal to some r :: t P CStacks with t of type τ k . 2) For all s :: t P CStacks with t : τ P Γ, rr s :: t ss is a term in Terms τ pN q.

3) For all s P WStacks, rr s ss belongs to TermspN q.

Proof: We start proving the first point and then use it to obtain the second one. Combining them, we finally prove the last point.

(1) We proceed by induction on the size of s P WStacks. The base case considers the stack r¨¨¨rKZs 1 ¨¨¨s n . As ̺pZq " 0, there is nothing to prove. Fix some stack s and assume that the property holds for all stacks smaller than s P WStacks. Let ϕ t 1 ¨¨¨t ℓ : τ be the top symbol of s with ϕ P N Y V , ℓ P r1, ̺pϕqs and t i P Γ for all i P r1, ℓs. If ϕ is of type τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o then for all i P r1, ℓs, t i is of type τ i and τ is the type

τ ℓ`1 Ñ . . . Ñ τ ̺pϕq Ñ o.
If k ď ℓ, Arg k psq def " pop 1 psq :: t k and there is nothing to prove. If ̺pϕq ě k ą ℓ, Arg k psq def " Arg k´ℓ pcollapsepsqq. To conclude by induction, the only thing we have to prove that Arg k´ℓ pcollapsepsqq is well defined. As ordpτ q ą 0, we have by definition of WStacks that collapsepsq is well-defined and that its top symbol starts with a symbol ψ of type τ . As |collapsepsq| ă |s| and as ̺pψq " ̺pϕq ´ℓ ě k ´ℓ ě 1, we have by induction hypothesis that Arg k´ℓ pcollapsepsqq is well-defined and is equal to some r :: t P CStacks with t P Γ of type τ k´ℓ`ℓ " τ k .

(2) We proceed by induction on the size of s :: t. The base case deals with r ¨¨¨r K s 1 ¨¨¨s n :: Z. As rr r s n :: Z ss def " Z, the property holds.

Assume that the property holds for all elements of CStacks smaller than some s :: t P CStacks with t : τ . Let us show that rr s :: t ss is of type τ . The case where t P N is trivial. The one where t " t 1 t 2 is immediate by induction as both rr s :: t 2 ss and rr s :: t 1 ss have a size smaller than rr s :: t ss. The last case is when t is a variable x P V . Assume that the variable x appears in an A-production for some A : τ " τ 1 Ñ . . . Ñ τ ̺pAq Ñ o in N . In particular the variable x is of type τ rkpxq . We have rr s :: x ss def " rr Arg rkpxq psq ss. By definition of CStacks, s is an A-stack and using point p1q, Arg rkpxq psq is equal to r :: t 1 with r P Stacks and t 1 : τ rkpxq P Γ. Thus rr s :: x ss " rr r :: t 1 ss for some r smaller than s and using the induction hypothesis, one concludes that rr s :: x ss is a term in Terms τ rkpxq pN q.

(3) Let s P WStacks whose top-symbol starts with ϕ : τ " τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o. Clearly pop 1 psq :: ϕ belongs to CStacks and by point p2q, rr pop 1 psq :: ϕ ss is of type τ . Points p1q and p2q implies that, for all k P r1, ̺pϕqs, rr Arg k psq ss is of type τ k . Hence, from Definition 4 it directly follows that rr s ss is of type o.

3) Proof of Lemma 2: . Lemma 2. Let k P r2, ms and let s " s 1 `t op k psq P WStacks. For all non-empty ϕ-stacks r Ď t op k psq, rr Arg ℓ ps 1 `rq ss " rr Arg ℓ ps `rq ss for all ℓ P r1, ̺pϕqs.

Proof: We show, by induction on the size of r, that s `r and s 1 `r are well-formed and rr Arg ℓ ps 1 `rq ss " rr Arg ℓ ps `rq ss for all ℓ P r1, ̺pϕqs where ϕ P N Y V denotes the head symbol of t op 1 prq.

The base case (which considers r¨¨¨rKZs 1 ¨¨¨s k ) is immediate. Assume that the property holds for all substack of t op k psq smaller than some ϕ-stack r Ď t op k psq. We will show that it holds for r.

The key observation is that: t op 2 ps `rq " t op 2 ps 1 `rq and either collapseps `rq " collapseps `rq if the link attached to topmost symbol of r is order greater than k or collapseps `rq " s `collapseprq and collapseps 1 `rq " s 1 `collapseprq otherwise.

As s 1 `r is a substack of s (which is well-formed), s 1 `r is well-formed as well. To prove that s `r is well-formed, we need to show that any non-empty substack of s `r satisfies the two properties expressed in Definition 1. The case of a proper substack immediately follows the induction hypothesis. We can deduce that s `r satisfies these two properties from the above observations. Indeed the first property only depends on the top most order-1 stack (and t op 2 ps `rq " t op 2 ps 1 `rq) and the second property follows from the fact that t op 1 ps `rq " t op 1 ps 1 `rq and t op 1 pcollapseps `rqq " t op 1 pcollapseps 1 `rqq.

Assume that the top symbol of r is equal to ϕ t 1 ¨¨¨t n . Let ℓ P r1, ̺pϕqs and let us show that rr Arg ℓ ps `rq ss " rr Arg ℓ ps 1 `rq ss. ‹ If ℓ ď n then rr Arg ℓ ps `rq ss " rr s `pop 1 prq :: t ℓ ss and rr Arg ℓ ps `rq ss " rr s 1 `pop 1 prq :: t ℓ ss. By induction hypothesis, we have that rr s `r1 :: t ss " rr s 1 `r1 :: t ss for any proper substack r 1 of r, in particular for r 1 " pop 1 prq. ‹ If ℓ ą n then rr Arg ℓ ps `rq ss " rr Arg ℓ´n pcollapseps `rqq ss and rr Arg ℓ ps `rq ss " rr Arg ℓ´n pcollapseps `rqq ss. From the above observation, we either have collapseps `rq " collapseps 1 `rq and the equality trivially holds or collapseps `rq " s `collapseprq and collapseps 1 `rq " s 1 `collapseprq in which case the equality follows by induction hypothesis as

| collapseprq | ă | r |.
4) Proof of Lemma 3: . Lemma 3. Let s be a ϕ-stack in WStacks for some ϕ :

τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o in V Y N and let ℓ P r1, ̺pϕqs with τ ℓ of order k ą 0. If Arg ℓ psq is equal to r :: t P CStacks with t starting with ψ P N Y V then pop n´k`1 psq " pop n´k`1 prq, | t op n´k`1 psq | ą | t op n´k`1 prq |.
Proof: We proceed by induction of the size of s. The base case which considers the stack r ¨¨¨r KZ s 1 ¨¨¨s n is immediate as ̺pZq " 0.

Assume that the property holds for all stacks in WStacks smaller than some stack s P WStacks. Let ϕ t 1 . . . t m be the top symbol of s with ϕ : τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o in V Y N and m P r0, ̺pϕqs. Let ℓ P r1, ̺pϕqs and let k be the order of τ ℓ . Assume that Arg ℓ psq " r :: t.

If ℓ ď m, Arg ℓ psq " pop 1 s :: t ℓ . In particular r is equal to pop 1 psq and the property holds because pop n´k`1 prq " pop n´k`1 ppop 1 psqq " pop n´k`1 psq as n ´k `1 ě 2 (indeed k ă n by definition of n).

If ℓ ą m, Arg ℓ psq " Arg ℓ´m pcollapsepsqq. By induction hypothesis, pop n´k`1 pcollapsepsqq " pop n´k`1 prq. To conclude it is enough to show that pop n´k`1 pcollapsepsqq " pop n´k`1 psq. Let k 1 be the order of t op 1 psq. As t op 1 psq " ϕ t 1 ¨¨¨t m is of type τ m `1 Ñ . . . Ñ τ ̺pϕq Ñ o, we have k 1 ą k. By definition of well-formed stacks, the order of the link attached to top symbol is equal to n ´k1 `1. In particular, pop n´k`1 pcollapsepsqq " pop n´k`1 psq. The second lemma states the soundness of the second and third lines of the definition of M. Moreover, it permits to conclude that there are no infinite path labeled by e in M.

Lemma 5. We have the following properties:

1) Let s P WStacks be a ϕ-stack for ϕ P V and let s 1 P WStacks be a ψ-stack for ψ P V Y N . If s e ÝÑ M s 1 then rr s ss " rr s 1 ss, ordpϕq ď ordpψq and | t op n´ordpϕq`1 psq | ą | t op n´ordpϕq`1 ps 1 q |.

2) For all s P WStacks there exists a unique N -stack s 1 P WStacks such that s e

Ý Ñ M s 1 .
Proof: (1) Let ϕ be a variable in V and let s be a ϕ-stack in WStacks.We distinguish two cases depending on the order of the ϕ. ‹ Assume that ϕ is of ground type and that Arg rkpϕq ppop 1 psqq is some r :: t P CStacks.

We have by definition of M that s e ÝÑ M s 1 " push t 1 prq. To show that rr s ss is equal to rr s 1 ss, we simply unfold the definitions.

rr s ss " rr push t 1 prq ss def " rr s 1 ss Assume that s 1 " push t 1 prq is a ψ-stack for some ψ P N YV . We have ordpψq ě ordpϕq " 0.

As | Arg k ppop 1 psqq | ď | s |´2, we have that | t op n`1 psq " s | ą | t op n`1 ps 1 q " s 1 |. ‹ Assume that ϕ is of type τ " τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o of order k ą 0.
Assume that Arg rkpϕq ppop 1 ppush n´k`1 psqqq is equal to r :: t P CStacks. First recall that, from Lemma 1, we have that t : τ . We have by definition that s ÝÑ M s 1 " push t,n´k`1 1 prq. Let us show that rr s ss " rr s 1 ss. Using Fact 1, we have that: rr s 1 ss " rr pop 1 ps 1 q :: t op 1 ps 1 q ss looooooooooooomooooooooooooon " rr pop 1 psq::ϕ ss p1q

rr Arg 1 pcollapseps 1 qq ss loooooooooooomoooooooooooon " rr Arg 1 psq ss p2q

. . . rr Arg ̺pϕq pcollapseps 1 qq ss loooooooooooooomoooooooooooooon " rr Arg ̺pϕq psq ss p2q

" rr pop 1 psq :: ϕ ssrr Arg 1 psq ss ¨¨¨rr Arg ̺pϕq psq ss " rr s ss.

The equalities denoted p1q and p2q are proven below:

rr pop 1 ps 1 q :: t op 1 ps 1 q ss def " rr r :: t ss " rr Arg rkpϕq ppop 1 ppush n´k`1 psqqq ss

As both ϕ and t have type τ , and as t is of the form ψ t 1 ¨¨¨t ℓ for some ℓ ě 0, it directly follows that ordpϕq ď ordpψq.

The fact that | t op n´ordpϕq`1 psq | ą | t op n´ordpϕq`1 ps 1 q | directly follows from Lemma 3. (2) Assume by contradiction that there exists an infinite sequence ps i q iě0 of stacks in WStacks such that for all i ě 0, s i e ÝÑ M s i`1 . For all i ě 0, we denote by t i the top-symbol of s i and ϕ i the head symbol of t i . According to (1), the order of the ϕ i increases and hence is ultimately constant. Let j and k be such that, for all i ě j, ordpϕ i q is equal to k. Using (1), the size of the t op n´k`1 ps i q is strictly decreasing starting from j which leads the contradiction.

By definition of M, only well-formed N -stacks can be the source of non-silent transitions. Let s be a well-formed Nstack. If rr s ss 6) Proof of Theorem 1: . Theorem 1. For every labeled recursion scheme S of order-n, there is an n-CPDA A that generates the same tree. Moreover, the number of states in A is linear in the maximal arity appearing in S, and its alphabet is of size linear in the one of S.

Proof (sktech): Let s be a well-formed stack. We denote by xx s yy the configuration of A defined by xx s yy " pq ˚, sq if s is an N -stack and xx s yy " pq rkpxq , sq if s is a V -stack whose topmost symbol starts with a variable x.

Clearly for any well-formed N -stack s, s C. Proofs Omitted in Section IV 1) Proof of Remark ??: . Remark ??. The second constraint in the definition of Damm-safety can be reformulated as : all argument subterms of an argument subterm of order-k appearing in a right-hand side, have at least order-k.

Proof: Let us first show that the condition of Definition 7 implies the condition stated in Remark ??. Let t : ϕ t 1 ¨¨¨t ℓ be an argument subterm of a right hand side of a Damm-safe scheme with ϕ : τ 1 Ñ ¨¨¨Ñ τ n Ñ o. It is enough to show that the t i 's have at least of order ordptq. If ℓ " 0 or ℓ " n (i.e. ordptq " 0q, the condition trivially holds. Assume that 0 ă ℓ ă n. As the scheme is homogeneous, the order of t is max iPrℓ`1,ns ordpτ i q `1 " ordpτ ℓ`1 q `1. Due to the Damm-safety condition, ordpτ ℓ q ě ordpτ ℓ`1 q `1 " t. Using homogeneity, it implies that ordpt i q " ordpτ i q ě ordpτ ℓ q ě ordptq.

Let us now show that the condition stated in Remark ?? implies the condition of Definition 7.

Let t : ϕ t 1 ¨¨¨t k be an argument subterm of a right hand side of a Damm-safe scheme with ϕ : τ 1 Ñ ¨¨¨Ñ τ n Ñ o and 0 ă k ă n. Using homogeneity, we have ordptq " ordpτ k`1 q`1. Toward a contradiction, assume that ordpτ k q " ordpτ k`1 q. This would imply that the argument subterm t of order ordpτ k`1 q `1 " ordpτ k q `1 contains the argument subterm t k of strictly smaller order ordpτ k q.

2) Proof of Proposition 2: . Proposition 2. Damm-safe schemes are safe and for every safe labeled scheme, there exists a Damm-safe labeled scheme of the same order generating the same tree.

Proof: Let S be a Damm-safe scheme, let us show that S is safe. Assume by contradiction that it is not and let t be an argument subterm of minimal size appearing in a right-hand side and violating the safety condition (i.e. t contains a variable of order less than ordptq). The term t can be written ϕ t 1 ¨¨¨t ℓ with ϕ : τ 1 Ñ ¨¨¨Ñ τ n Ñ o and 0 ă ℓ ă n. As S is Damm-safe, all the t i 's have at least order ordptq (cf. Remark ??) and one of them t i0 contains a variable of order strictly smaller than ordptq. This contradicts the minimality of t.

Let S be a safe scheme. By Corollary 1, we can construct a higher-order pushdown automaton A of the same order generating the same tree. It is easy to very that the translation of [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF] of higher-order pushdown automata into safe schemes in fact produces Damm-safe schemes. Therefore applying it to the automaton A yields a Damm-safe scheme generating the same tree as S and of the same order.

3) Proof of Theorem 2: . The following proof substantiate the proof sketch given in Section IV only at order 2. We start with the proof at order-2 to get intuition of the objects. Then we sketch the key invariants for the proof in the general case.

Theorem 2 (order-2). The translation of Section III when applied to a safe order-2 recursion scheme yields a link-free CPDA Proof: Let S be an order-2 safe scheme and let A be the CPDA constructed from S in Section III-B. To show that A is link-free, we first show that, in any reachable configuration 7 pq, s " rs 1 . . . s m s 2 q, we can define the target of the links of s using only the symbols appearing in the stack. Then, this stronger result allows us to conclude.

For this, we need to introduce some notations. For i P r1, ms and j P r1, |s i |s, we denote by rpi, jq, tpi, jq and opi, jq respectively the j-th symbol of stack s i , the target (if defined) in r1, i ´1s of its link and the order (if defined) of this link. By definition of A, tpi, jq and opi, jq are defined iff rpi, jq is a term of order k ą 0 and in this case opi, jq is equal to 2 ´k `1 Moreover for i P r2, ms, we let ℓ i be the smallest index at which s i´1 and s i have a different symbol (or

|s i | `1 if no such index exists).
The stack s satisfies the following properties: 1) for all i P r1, |s 1 |s, tp1, iq is undefined;

2) for all i P r2, ms, ℓ i ď |s i´1 | and for all i P r2, m ´1s, ℓ i ď |s i |;

3) for all i P r2, ms and 1 ď j ă ℓ i , tpi, jq " tpi ´1, jq; 4) for all i P r2, ms with ℓ i ď |s i |, rpi, ℓ i q does not contain a variable of order 0 and is an argument subterm of rpi´1, ℓ i q and if rpi, ℓ i q is of order 1 then tpi, ℓ i q " i ´1;

5) for all i P r2, ms with j P rℓ i `1, |s i |s, tpi, jq is undefined; 6) if m ě 2 then ℓ m " |s m | `1 iff t op 1 psq " ϕt 1 . . . t h , q " q k for some k P r1, hs such that ordpt k q " 1. These properties are proved by induction on the length of the shortest path in the LTS from the initial configuration to pq, sq and by inspection of the transitions of A. These properties trivial hold for the initial configuration. Assume that they are verified by a configuration pq, sq, let us show that they hold for any configuration pp, rq such that pq, sq a ÝÑ P pp, rq. We distinguish several cases depending on the transition of A applied to go from pq, sq to pp, s 1 q. Let t be t op 1 psq and let ℓ 1 i , t 1 pi, jq, o 1 pi, jq, r 1 pi, jq be the notions corresponding to s 1 . ‹ If t starts with F P N and if F x 1 ¨¨¨x ̺pF q a ÝÑ e P R.

' The transition is δpq ˚, t, aq " pq ˚, push e 1 q. Then e starts with a non-terminal and p " q " q ˚and s 1 " push e 1 psq. If m " 1, there is nothing to prove. Otherwise, as q " q ˚, by Property 6, ℓ m ď |s m | hence, ℓ m " ℓ 1 m . Therefore, all properties for s 1 are inherited from s. In particular Property 5 is still satisfied as we did not attached a link to the order-0 term we just pushed on top of s.

' The transition is δpq ˚, t, aq " pq rkpxq , idq. Then s 1 " s and all properties are inherited from s. ' The transition is δpq ˚, t, aq " pq rkpxq , push e 1 ; push 2 ; pop 1 q. Then e starts with a variable x of order 1, p " q ˚, q " q rkpxq and s 1 " pop 1 ppush 2 ppush e 1 psqqq. The most interesting case is that of Property 6. As ℓ 1 m`1 " |s m`1 | `1, we need to show that t op 1 ps 1 q " ϕt 1 . . . t h , q " q k for some k P r1, hs such that ordpt k q " 1. The only non-immediate part is that k ď h. It holds as otherwise it would imply that t op 1 ps 1 q is an argument subterm of order-2 (as it misses at least one argument of order-1) which leads a contradiction as the scheme we consider has order-2 (hence all its argument subterms have order ď 1).

‹ If t is a term of the form ϕ t 1 ¨¨¨t h for some ϕ P V Y N .
' The transition is δpq k , t, eq " pq rkptkq , pop 1 ; push tk 1 q. Then k ď h, t k : o, p " q k , q " q rkpt k q and s 1 " m " |s 1 m |: indeed, Property 4 guaranties that rpm, ℓ m q is an argument subterm of rpm ´1, ℓ m q, hence t k is as well an argument subterm of rpm ´1, ℓ m q (as it is an argument subterm of rpm, ℓ m q) hence differs from rpm ´1, ℓ m q. It remains to show that Property 4 holds (the others are inherited). As r 1 pm, ℓ 1 m q " t k has order 0, the only thing to prove is that t k does not contains a variable of order-0. But, as t k is an argument subterm of t and because t does not contain any variable of order 0 (by induction hypothesis) the same holds for t k .

push t k 1 ppop 1 psqq. If m " 1,
' The transition is δpq k , t, eq " pq rkptkq , pop 1 ; push tk,2 1 q. Then k ď h and t k has order 1, p " q k , q " q rkpt k q and s 1 " push t k ,n´h`1 1 ppop 1 psqq. First remark that the previous transition was necessarily pq k , push t 1 ; push 2 ; pop 1 q (coming from state q ˚) or pq k , collapseq (coming from some state q h with h ą k). In the first subcase, s m was a prefix of s m´1 hence s 1 m and s 1 m´1 differs in their last symbol, meaning that ℓ 1 m " |s 1 m |; the only thing to prove is Property 4 holds (the others are inherited) and in particular that t k does not contain a variable of order 0: but this is a consequence of the safety constraint because t k is an argument subterm of a right-hand-side and as it has order-1 the safety constraint imposes that it does not contain a variable of order 0. For the second subcase (the previous transition was a collapse), we remark that ℓ m ď |s m | (see next case below). Hence we can conclude as in case above when t k : o.

' The transition is δpq k , t, eq " pq k´h , collapseq. Then k ą h, p " q k , q " q k´h and s 1 " collapsepsq. All properties except Property 6 are inherited. For Property 6, we use the the second part of Property 2 to crucially guaranty that the stack s 1 is such that ℓ 1 n 1 ď |s 1 n 1 | (here n 1 refers to the stack height in s 1 ). We are now ready to conclude that A is link-free. Inspecting the transitions of A, a collapse operation can only be performed if q " q k and t op 1 psq " ϕ t 1 . . . To extend the previous proof at any order n, we first need to introduce notations to designate positions in an order-n stack.

Let s " rs 1 , . . . s m s n be an order-n stack. For h P r0, ns, we inductively define an h-position in s as the index of an order-h stack inside s. An h-position in s is a tuple i P N n´h such that:

The set of h-positions in s is denoted Pos h psq. For two positions i and j, we write i ď j if i is smaller than j for the lexicographic order. We denote by max h psq the maximum element of Pos h psq.

For any h P r0, n ´1s and any i P Pos h psq, we inductively define the order-h stack occurring at postion i, denoted spiq, by: ' if h " n there is only one h-position : the empty tuple ε and we let spεq " s; ' if h " n ´1 then spiq " s i ; ' if h ă n ´1 then as i " ij with i P r1, ms and j is an h-position in s i , we take spiq " s i pjq.

Notation 3. For a symbol appearing in the stack x, Rpxq, T pxq and Opxq respectively designate the symbol (in Γ), the target of the link (if defined) and the order of the link (if defined) appearing in x.

By construction of A, T pspiqq and Opspiqq are defined iff Rpspiqq is a term of order k ą 0 and in this case OpSpiqq is equal to n ´k `1.

For all h P r0, n ´1s and all i " pi 1 , . . . , i |i| q P Pos h psq, we define predpiq P Pos h psq and suppiq P Pos h`1 psq if h ă n by predpiq " pi 1 , . . . , i |i| ´1q if i |i| ą 1 and predpiq is undefined otherwise and suppiq " pi 1 , . . . , i |i|´1 q.

For all h P r0, n ´1s, the position i " pi 1 , . . . , i |i| q P Pos h psq is initial if i |i| " 1. In other terms, i is initial if and only if predpiq is undefined.

For all h P r1, n ´1s, we define a partial mapping ℓ h s with domain in Pos h psq associating to an h-position i a 0-position in spi). The value of ℓ h s piq (when it is defined) is the smallest 0-position j in spiq such that rpiq differs from Rpă piqq. Remark that ℓ h s piq is undefined for a non-initial i if and only if spiq is a substack of sppredpiqq.

Theorem 2 (arbitrary order). The translation of Section III when applied to a safe order-n recursion scheme yields a link-free CPDA Proof: We define by induction on the order h the notion of safe stack. All order-1 stacks are safe stacks. An oder-ph`1q stack s " rs 1 . . . s m s h`1 is safe if:

1) for all i P r1, ms, s i is a safe order-h stack.

2) for all i P r2, ms, ℓ h s piq is defined and is such that ℓ h s piq belongs to Pos 0 ps i´1 q and Rps i pℓ h s piqqq is an argument subterm of Rps i´1 pℓ h s piqqq which does not contain any variable of order ă n ´h `1. If Rps i pℓ h s piqqq is of order ą 0 then T ps i pℓ h s piqqq " i ´1. For all j ě ℓ h s piq in Pos 0 ps i q, Rps i pjqq is not of order n ´h `1. We slightly relax the notion of safe stack by defining w-safe stack for w P r2, h `1s. An oder-ph `1q stack s " rs 1 . . . s m s h`1 is w-safe if:

1) for all i P r1, m ´1s, s i is a safe order-h stack, s m is safe if w " h `1 and s m is w-safe otherwise;

2) for all i P r2, m 1 s where m 1 " m if w ă h `1 and m 1 " m ´1 otherwise, ℓ h s piq is defined and is such that ℓ h s piq belongs to Pos 0 ps i´1 q and Rps i pℓ h s piqq is an argument subterm of Rps i´1 pℓ h s piqqq which does not contain any variable of order ă n ´h `1. If Rps i pℓ h s piqqq is of order ą 0 then T ps i pℓ h s piqqq " i ´1. For all j ě ℓ h s piq in Pos 0 ps i q, Rps i pjqq is not of order n ´h `1. By an induction similar to the order-2 case, we can prove that for all reachable configuration pq, sq, s is w-safe iff t op 1 psq starts with ϕ : pτ 1 , . . . , τ ̺pϕq , oq, q " q i with ordpτ i q " n ´w `1; otherwise s is safe.

We are now ready to conclude that A is link-free. Inspecting the transitions of A, a collapse operation can only be performed if q " q k and t op 1 psq " ϕ t 1 . . . t h with k ą h and ϕ : pτ 1 , . . . , τ m , oq. Let us write w " n ´ordpτ k q `1. By the above property s is w-safe. Let w 1 " n ´ordpt op 1 psqq `1. We have w 1 ă w and the link is of order w 1 . Let s 1 be the topmost order-w 1 stack of s. By definition of w-safety it is safe. The last part of Property 2 implies that ℓ w 1 s 1 is max w 1 ps 1 q hence Property 2 implies that the link of the top-most symbol of s 1 point to the previous order-pw 1 ´1q stack. Hence collapsepsq " pop w 1 psq.

D. Collapsible Pushdown Games: Complexity and Winning Strategies

This section is devoted to the study of parity games played on LTS of CPDA. For simplicity of presentation we omit the input alphabet and introduce the concept of Collapsible pushdown processes (CPDP). The main focus is on complexity of deciding the winner and in establishing the existence of strategies realised by CPDA transducer synchronised with the one defining the game. This latter result is the key ingredient to prove the effective selection property.

Comparison with previous proofs from [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] and [START_REF] Broadbent | Recursion schemes and logical reflexion[END_REF].

The lines behind the proof of the main result of this section (Theorem 5) slightly differ from the one of a similar statement (where complexity was not studied precisely, neither strategies) from [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. Indeed, in [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] the induction step removes the outmost links at the same time as in reduces the order. As a consequence, the definition of collapse rank was different, and the transformation from a usual CPDA to a rank-aware one is different. Separating both steps (removing the link and decreasing the order) seemed necessary with respect to designing strategies realised by CPDA, which is crucially used later for effective selection. Note that a similar proof technique (but without any consideration on strategies and precise complexity) was considered in [START_REF] Broadbent | Recursion schemes and logical reflexion[END_REF]. Hence the main added value here are: precise (and improved) analysis of the complexity (which requires several optimisations) and existence of winning strategies realised by CPDA synchronised with the one defining the game.

1) Collapsible Pushdown Processes: . First we introduce, for any stack symbol γ an operation on stacks that does top 1 rewriting: this operation, denoted r ew γ 1 , takes the top 1 element and replace it by γ without modifying the link. Formally:

r ew γ 1 [s 1 ¨¨¨s l`1 ] loooooomoooooon s " # [s 1 ¨¨¨s l r ew γ 1 s l`1 ] if ords ą 1 [s 1 ¨¨¨s l γ pj,kq ] if ords " 1 and s l`1 " α pj,kq
We also let id for the identity operation (i.e. idpsq " s for all stack s).

We now introduce the notion of collapsible pushdown processes which differs from CPDA from the fact that they have no input alphabet (and can be non-deterministic).

An order-n collapsible pushdown process (n-CPDP) is a 4-tuple A " x Γ, Q, ∆, q 0 y where Γ is the stack alphabet, Q is the finite set of control states, q 0 P Q is the initial state, and ∆ : Q ˆΓ Ñ 2 QˆOpnpΓqˆOpnpΓq is the transition function and satisfies the following constraint. For any q, γ P Q ˆΓ, for any pq 1 , op 1 , op 2 q P ∆pq, γq one has that op 1 P tr ew α 1 | α P Γu Y tidu and op 2 R tr ew α 1 | α P Γu: hence a transition will always act on the stack by doing (possibly) rewriting the top symbol and then (possibly) doing another kind of operation on the stack. In the following we will use notation pq 1 , op 1 ; op 2 q instead of pq 1 , op 1 , op 2 q (to stress that one performs op 1 followed by op 2 ).

Configurations of an n-CPDP are pairs of the form pq, sq where q P Q and s is an n-stack over Γ; we call pq 0 , K n q the initial configuration, where K n " r. . . r K s 1 . . .s n .

An n-CPDP A " x Γ, Q, ∆, q 0 y naturally defines a transition graph GraphpAq :" pV, E Ď V ˆV q whose vertices V are the configurations of A and whose edge relation E is given by: ppq, sq, pq 1 , s 1 qq P E iff Dpq 1 , op 1 ; op 2 q P ∆pq, t op 1 psqq such that s 1 " op 2 pop 1 psqq. Such a graph is called an n-CPDP graph.

2) n-CPDP Parity Games: . Let G " pV, E Ď V ˆV q be a graph. Let V E Z V A be a partition of V between two players, Éloïse and Abelard. A arena is such a tuple G " pG, V E , V A q. A colouring function Ω is a mapping Ω : V ÝÑ C Ă N where C is a finite set of colours. An infinite two-player parity game on an arena G is a pair G " pG, Ωq.

Éloïse and Abelard play in G by moving a pebble between vertices. A play from some initial vertex v 0 proceeds as follows: the player owning v 0 moves the pebble to a vertex v 1 such that pv 0 , v 1 q P E. Then the player owning v 1 chooses a successor v 2 and so on. If at some point one of the players cannot move, she/he loses the play. Otherwise, the play is an infinite word v 0 v 1 v 2 ¨¨¨P V ω and is won by Éloïse just in case lim infpΩpv i qq iě0 is even. A partial play is just a prefix of a play.

A strategy for Éloïse is a function assigning, to every partial play ending in some vertex v P V E , a vertex v 1 such that pv, v 1 q P E. Éloïse respects a strategy Φ during a play Λ " v 0 v 1 v 2 ¨¨¨if v i`1 " Φpv 0 ¨¨¨v i q, for all i ě 0 such that v i P V E .

A strategy Φ for Éloïse is winning from a position v P V if she wins every play that starts from v and respects Φ. Finally, a vertex v P V is winning for Éloïse if she has a winning strategy from v. Symmetrically, one defines the corresponding notions for Abelard. It follows from Martin's determinacy Theorem [A5] that, from every position, either Éloïse or Abelard has a winning strategy. Now let A " x Γ, Q, ∆, q 0 y be an order-n CPDP and let GraphpAq " pV, Eq be its transition graph. Let Q E Z Q A be a partition of Q and let Ω : Q ÝÑ C Ă N be a colouring function (over states). Altogether they define a partition V E Z V A of V whereby a vertex belongs to V E iff its control state belongs to Q E , and a colouring function Ω : V ÝÑ C where a vertex is assigned the colour of its control state. The structure G " pGraphpAq, V E , V A q defines an arena and the pair G " pG, Ωq defines a parity game (that we call a n-CPDP parity game).

Given an n-CPDP parity game, we will consider the following two algorithmic questions: 1) Decide whether pq 0 , K n q is winning for Éloïse.

2) If pq 0 , K n q is winning for Éloïse, provide a description of a winning strategy for Éloïse from pq 0 , K n q.

To answer the second question we will consider strategies realised by n-CPDA transducers.

3) CPDA strategies: . Let A " x Γ, Q, ∆, q 0 y be an order-n CPDP, let GraphpAq " pV, Eq be its transition graph, let G " pGraphpAq, V E , V A q be an arena associated with A and let G " pG, Ωq be a corresponding n-CPDP parity game.

We aim at defining a notion of n-CPDA transducers that provide a description for strategies in G, that is describe a function from partial plays in G into V .

Consider a partial play Λ " v 0 v 1 ¨¨¨v ℓ in G where v 0 " pq 0 , K n q. An alternative description of Λ is by the sequence pq 1 , rew 1 ; op 1 q ¨¨¨pq ℓ , rew ℓ ; op ℓ q P pQ ˆOp n pΓq ˆOp n pΓqq ˚such that v i " pq i , s i q for all 1 ď i ď ℓ and s i " op i prew i ps i´1 qq (with the convention that s 0 " K n ). We may in the following use implicitly this representation of Λ when needed. Similarly, one can represent a strategy as a (partial) function Φ : pQˆOp n pΓqˆOp n pΓqq ˚Ñ QˆOp n pΓqˆOp n pΓq, the meaning being that in a partial play Λ ending in some vertex pq, sq if ΦpΛq " pq 1 , rew; opq then the player moves to pq 1 , opprewpsqqq.

An n-CPDA transducer realising a strategy in G is a tuple S " x Σ, S, δ, τ, s 0 y where Σ is a stack alphabet, S is a finite set of states, s 0 P S is the initial state, δ : S ˆΣ ˆpQ ˆOp n pΓq ˆOp n pΓqq Ñ S ˆOp n pΣq ˆOp n pΣq is a deterministic transition function and τ : S ˆΣ Ñ Q ˆOp n pΓq ˆOp n pΓq is a deterministic choice function (note that we do not require τ to be total). For both δ and τ we do the same requirement as for the transition function for CPDP, namely that the first stack operation should be a top-rewriting (or the identity) and that the second one should not be a top-rewriting.

A configuration of T is a pair ps, σq where s is a state and σ is an n-stack over Σ; the initial configuration of T is ps 0 , K n q. With a configuration ps, σq is associated, when defined, a (unique) move in G given by τ ps, t op 1 pσqq A partial play Λ " pq 1 , rew 1 , op 1 q ¨¨¨pq ℓ , rew ℓ , op ℓ q in G induces a (unique, when defined) run of T which is the sequence such that ps 0 , σ 0 qps 1 , σ 1 q ¨¨¨ps ℓ , σ ℓ q where ps 0 , σ 0 q " ps 0 , K n q is the initial configuration of T and for all 0 ď i ď ℓ ´1 one has δps i , t op 1 pσ i q, pq i`1 , rew i`1 ; op i`1 qq " ps i`1 , rew 1 i`1 ; op 1 i`1 q with σ i`1 " op 1 i`1 prew 1 i`1 pσ i qq. In other words, the control state and the stack of T are updated accordingly to δ.

We say that T is synchronised with A iff for all ps, a, pq, rew; opqq P S ˆΣ ˆpQ ˆOp n pΓq ˆOp n pΓqq such that δps, a, pq, rew; opqq " ps 1 , rew 1 ; op 1 q is defined one has that op and op 1 are of the same kind, i.e. either they are both a pop k (for some k) or both a push k (for some k) or both a push _,e 1 (the symbol pushed being possibly different but the order of the link being the same) or both collapse or both id . In particular, if one defines the shape of a stack s as the stack obtained by replacing all symbols appearing in s by a fresh symbol 7 (but keeping the links) one has the following. Proposition 3. Assume that T is synchronised with A. Then, for any partial play Λ in G ending in a configuration with stack s, the run of T on Λ, when exists, ends in a configuration with stack σ such that s and σ have the same shape.

The strategy realised by T is the (partial) function ϕ S defined by letting ϕ S pΛq " τ pps, t op 1 pσqqq where ps, σq is the last configuration of the run of T on Λ.

We say that Éloïse respects ϕ S during a partial play Λ " pq 1 , rew 1 ; op 1 q ¨¨¨pq ℓ , rew ℓ ; op ℓ q in G iff for all 0 ď i ď ℓ ´1 if the last configuration in pq 1 , rew 1 ; op 1 q ¨¨¨pq i , rew i ; op i q belongs to V E then pq i`1 , rew i`1 ; op i`1 q " ϕ S ppq 1 , rew 1 ; op 1 q ¨¨¨pq i , rew i ; op i qq We say that ϕ S is well-defined iff for any partial play Λ " pq 1 , rew 1 ; op 1 q ¨¨¨pq ℓ , rew ℓ ; op ℓ q where Éloïse respects ϕ S if the last vertex pq ℓ , s ℓ q in Λ belongs to V E then ϕ S pΛq P ∆pq, t op 1 ps ℓ qq, i.e. the move given by ϕ S is a valid one. 4) Main Result: . Theorem 5. Let A " x Γ, Q, δ, q 0 y be an n-CPDA and let G be an n-CPDA parity game defined from A. Then one has the following results.

1) Deciding whether pq 0 , K n q is winning for Éloïse is an n-EXPTIME complete problem.

2) If pq 0 , K n q is winning for Éloïse then one can effectively construct an n-CPDA transducer T synchronised with A realising a well-defined winning strategy for Éloïse in G from pq 0 , K n q.

The proof is by induction on the order and each induction step is itself divided into two steps: the first one removes the outermost links while the second one lowers the order.

Before going to the proof, we give in Section D5 a normalisation result (Theorem 6). Then Section D6 explains how to removes the outermost links and Section D7 shows how to reduce the order. Finally Section D8 combines the previous constructions and provides the proof of Theorem 5 together with a precise complexity analysis. 5) Rank-aware CPDP: . Fix, for the whole subsection, an n-CPDP A " xΓ, Q, ∆, q 0 y, a partition

Q E Z Q A of Q and a colouring function Ω : Q Ñ C Ă N.
Denote by G its transition graph, by G the arena induced by G and the partition Q E Z Q A and by G the parity game pG, Ωq.

Let s be an order-n stack. We first associate with s " s 1 , ¨¨¨, s ℓ a well-bracketed word of depth n, r s P pΣ Y t[, ]uq

˚: r s :" # [ r s 1 ¨¨¨r s ℓ ] if n ě 1 s if n " 0 (i.e. s P Σ)
In order to reflect the link structure, we define a partial function targetpsq : t1, ¨¨¨, |r s|u Ñ t1, ¨¨¨, |r s|u that assigns to every position in t1, ¨¨¨, |r s|u the index of the end of the stack targeted by the corresponding link (if exists; indeed this is undefined for K, [ and ]). Thus with s is associated the pair x r s, targetpsq y; and with a set S of stacks is associated the set r S " tx r s, targetpsq y | s P Su.

Example 16. Consider the stack s " [[[K α]] [[K][K a β γ]]]. Then r s " [[[ K α]] [[K][ K α β γ]]
] and targetp5q " 4, targetp14q " 13, targetp15q " 11 and targetp16q " 7.

A finite path in G is a non-empty sequence of configurations v 0 v 1 ¨¨¨v m such that for all 0 ď i ď m ´1, there is an edge in G from v i to v i`1 . An infinite path is an infinite sequence of configurations v 0 v 1 ¨¨¨such that for all i ě 0, there is an edge in G from v i to v i`1 . Note that we do not require v 0 to be the initial configuration.

We now define a generalisation of n-stacks called indexed n-stacks. Recall that a stack s is equivalently described as a pair x r s, targetpsq y (recall that r s is a well-bracketed word description of s and that targetpsq gives the link structure). An indexed n-stack is described by a triple x r s, targetpsq, indpsq y where r s " r s 1 ¨¨¨r s |r s| and targetpsq are as previously and where indpsq : t1, . . . , |r s|u Ñ N is a partial function that is defined in any position j ă |r s| ´n such that r s j R t[, ]u. The previous conditions on the domain of indpsq ensure that any symbol in s which is not the topmost one has a value by indpsq that we refer to as its index. An indexed configuration is a pair formed by a control state and an indexed stack.

The erasure of an indexed n-stack x r s, targetpsq, indpsq y is the n-stack x r s, targetpsq y. We extend the notion of erasure to indexed configuration in the obvious way.

With any path Λ " v 0 v 1 ¨¨¨, with v i " pp i , s i q for all i ě 0, we inductively associate a sequence of indexed configurations Λ 1 " v 1 0 v 1 1 ¨¨¨such that the following holds. ' The erasure of Λ 1 equals Λ (the erasure of a sequence of indexed configurations being defined as the sequence of the respective erasures).

' For any indexed configuration v 1 m " pq m , s 1 m q the following holds. Denote by s 1 m " x Ă s 1 m , targetps 1 m q, indps 1 m q y, let Ă s 1 m " x 1 ¨¨¨x h , and let j be in the domain of indps 1 m q such that x j`1 " ]. Then let j 1 ą j be the largest integer such

s 1 0 "[[[K 0 α 0 ]][[K]]] colour : 3 push β,1 1 ÝÑ s 1 1 "[[[K 0 α 0 ]][[K 1 β]]] colour : 0 r ew α 1 ;push 2 ÝÑ s 1 2 "[[[K 0 α 0 ]][[K 1 α 2 ][K 1 α]]] colour : 1 pop 1 ÝÑ s 1 3 "[[[K 0 α 0 ]][[K 1 α 2 ][K]]] colour : 5 push α,1 1 ÝÑ s 1 4 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α]]] colour : 3 push β,2 1 ÝÑ s 1 5 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α 5 β]]] colour : 2 push 3 ÝÑ s 1 6 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α 5 β 6 ]][[K 1 α 2 ][K 4 α 5 β]]] colour : 4 push γ,3 1 ÝÑ s 1 7 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α 5 β 6 ]][[K 1 α 2 ][K 4 α 5 β 7 γ]]] colour : 6 push 2 ÝÑ s 1 8 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α 5 β 6 ]][[K 1 α 2 ][K 4 α 5 β 7 γ 8 ][K 4 α 5 β 7 γ]]] colour : 5 pop 1 ÝÑ s 1 9 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α 5 β 6 ]][[K 1 α 2 ][K 4 α 5 β 7 γ 8 ][K 4 α 5 β]]] colour : 6 collapse ÝÑ s 1 10 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α 5 β 6 ]][[K 1 α]]] colour : 4 pop 3 ÝÑ s 1 11 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α 5 β]]] colour : 3 push γ,1 1 ÝÑ s 1 12 "[[[K 0 α 0 ]][[K 1 α 2 ][K 4 α 5 β 12 γ]]] colour : 2 Figure 4.
Example of a sequence of indexed stacks that x k " ] for all j `1 ď k ď j 1 and let i be the unique integer such that x i ¨¨¨x j 1 is well-bracketed. Then, for any i ă k ă j 1 , if indps 1 m qpkq is defined, one has indps 1 m qpkq ď indps 1 m qpjq, and this inequality is strict if indps 1 m qpjq ‰ 0. Intuitively, position j is the topmost symbol of some pj 1 ´jq-stack, and any symbol in this stack has an index smaller than the topmost symbol. The intended meaning of the index of some symbol in the stack is the following. The index is equal to the largest integer i such that since v i {v 1 i the symbol no longer appears as a t op 1 -element. If one uses the stack to store (and maintain) some information, the index is the moment from which this information was no longer updated. Hence when some symbol appears again as the t op 1 -element, one has to update the information by taking into account all that happened since v i {v 1 i (included). The intuitive idea behind the forthcoming definition of Λ 1 is rather simple. The indices are always preserved, so one only cares on new positions in the stack. On doing a push k the indices of the copied stack are inherited from the original copy. Then when new indices are needed (because a position is no longer the t op 1 one, it get index m `1 if the current configuration is v m`1 ).

Before going to the formal definition, we start with an example.

Example 17. In figure 4, we give an example (at order 3) that illustrates the previous intuitive idea as well as the formal description below (ignore the information on colours for this example). We only describe the indexed stacked (omitting the control states), and indicate the stack operation (but omit the id operation). Indices are written as superscripts.

Now, we formally give the construction (the previously mentioned properties easily follow from the definition). The initial configuration v 1 0 " pp 0 , s 1 0 q, is obtained by letting indps 1 0 q be the constant (partial) function equal to 0. Assume now that v 1 1 ¨¨¨v 1 m has been constructed, let v 1 m " pp m , s 1 m q with s 1 m " x r s m , targetps m q, indps 1 m q y and let v m`1 " pp m`1 , s m`1 q with s m`1 " x r s m`1 , targetps m`1 q y. We let v 1 m`1 " pp m`1 , s 1 m`1 q with s 1 m`1 " x r s m`1 , targetps m`1 q, indps 1 m`1 q y where indps 1 m`1 q is defined thanks to a case distinction. ' A top-rewriting operation followed by a push γ,k 1 operation is applied in configuration v m . Then all previous indices are inherited and the former t op 1 -element gets index m `1. Formally, indps 1 m`1 qpjq " indps 1 m qpjq whenever j ă |r s m | ´n and indps 1 m`1 qp|r s m | ´nq " m `1.

' A top-rewriting operation followed by a push k operation is applied: s m`1 " push k ps m q. First, all existing indices are preserved, i.e. indps 1 m`1 qpjq " indps 1 m qpjq whenever j belongs to the domain of indps 1 m q. Then one writes r s m as [ ¨¨¨[t]] n´k`1 with t being well-bracketed; hence, r

s m`1 " [ ¨¨¨[t][t]] n´k`1 . Then we let indps 1 m`1 qp| Ă s 1 m | ṕn ´k `1q `jq " indps 1 m qp| Ă s 1
m | ´pn ´k `1q ´p|t| `2q `jq for all j ě 1 such that the second member of the equality is defined: the indices are simply copied from the former top pk ´1q-stack. Finally, the former t op 1 -element gets index m `1: indps 1 m`1 qp|r s m | ´n `k ´3q " m `1. ' A top-rewriting operation followed by a either a pop k operation or a collapse or id is applied in configuration v m in Λ. Then all indices are inherited from the previous indexed stack. Formally, indps 1 m`1 qpjq " indps 1 m qpjq whenever j belongs to the domain of indps 1 m`1 q. The following proposition is crucial for the rest of the proof. In particular, it means that if we stored some information on the stack, the index gives the "expiry date" of the stored information, that is the step in the computation starting from which the information has no longer been updated. Proposition 4. Let Λ " v 0 v 1 ¨¨¨be a path and Λ 1 " v 1 0 v 1 1 ¨¨¨be as above. Let m ě 0, let s 1 m " x r s m , targetps m q, indps 1 m q y be the indexed stack in v 1 m . Let j be such that i " indps 1 m qpjq is defined. If i ą 0, then pi ´1q is the largest integer such that the j-th letter of r s m is a copy of t op 1 ps i´1 q. If i " 0, there is not i 1 such that the j-th letter of r s m is a copy of t op 1 ps i 1 q.

Proof: Immediate by induction on m and from the definition of Λ 1 from Λ. Our main goal is to enrich the stack alphabet in order to compute the link-rank. Assume that in configuration v m the t op 1 -element has a link (that is possibly a copy of a link) that was created in configuration v j : then the link-rank in v m is defined as the smallest colour since the creation of the link, i.e. mintΩpv j q, ¨¨¨Ωpv m qu. In order to maintain this information, we need to define two other concepts: the collapse-rank (for updating after performing a collapse) and the pop-rank for k (for updating after performing a pop k ).

We first introduce the notion of ancestor. Fix a finite path Λ " v 0 v 1 ¨¨¨v m , let v m " pq, sq be some configuration in Λ and let x be a symbol in s. Then the ancestor of x is the configuration v i where i is the index of x in v 1 m (the indexed version of v m ).

We now introduce the notion of collapse-rank. Fix a finite path Λ " v 0 v 1 ¨¨¨v m and assume that the t op 1 -element of v m has a pk `1q-link for some k. Then the collapse-ancestor in v m is the ancestor of the t op 1 -element of the pointed k-stack and the collapse-rank in v m is the smallest colour visited since the collapse-ancestor (included).

Example 18. Consider the sequence of indexed stacks given in Figure 4 (the colours of the corresponding configurations are indicated on the right part of the figure).

In v 1 8 the collapse-ancestor is 6 and the collapse-rank is therefore 4. In v 1 9 the collapse-ancestor is 2 and the collapse-rank is therefore 1.

Next, we give a notion of pop-rank. Fix a partial play Λ " v 0 v 1 ¨¨¨v m and a configuration v m " pq, sq in Λ. Then, for any 1 ď k ď n, the pop-ancestor for k, when defined, is the ancestor of the t op 1 -element of pop k psq and the pop-rank for k, when defined, is the smallest colour visited since the pop-ancestor for k (included). In particular, the pop-rank for n is the smallest colour visited since the stack has height at least the height of s.

Example 19. Again, consider the sequence of indexed stacks given in Figure 4.

In configuration v 1 9 the pop-ancestor (resp. pop-rank) for 3 is 6 (resp. 4), the pop-ancestor (resp. pop-rank) for 2 is 8 (resp. 5) and the pop-ancestor (resp. pop-rank) for 1 is 5 (resp. 2).

In configuration v 1 12 the pop-ancestor (resp. pop-rank) for 3 is 0 (resp. 0), the pop-ancestor (resp. pop-rank) for 2 is 2 (resp. 1) and the pop-ancestor (resp. pop-rank) for 1 is 12 (resp. 2). Consider a finite path Λ " v 0 v 1 ¨¨¨v m in G ending in a configuration v m " pq, sq such that t op 1 psq has an n-link (if the link is a k-link for some k ă n the following concepts are not relevant). The link-ancestor of v m is the configuration v j where the original copy of the n-link in t op 1 psq was created 8 , or v 0 if the link was present in the stack of the configuration v 0 . The link-rank of v m is the minimum colour of a state occurring in Λ since its link-ancestor v j (inclusive) i.e. it is mintΩpv j q, ¨¨¨Ωpv m qu.

Example 20. Consider the sequence of indexed stacks given in Figure 4. The link-ancestor of configuration v 1 8 is configuration v 1 7 and its link-rank is 5. The link-ancestor of configuration v 1 11 is configuration v 1 5 and its link-rank is 2.

Definition 8. An n-CPDP A " x Γ, Q, ∆, q 0 y equipped with a colouring function is rank-aware from a configuration v 0 if there exist a function LinkRk : Q ˆΓ Ñ N such that for any finite path Λ " v 0 v 1 ¨¨¨v ℓ , the link-rank (if defined) of the configuration v ℓ " pq, sq is equal to LinkRkpq, t op 1 psqq. In other words, the link rank can be retrieved from the control state together with the t op 1 -element of the stack.

Remark 7. In the current setting, if the ancestor of the pointed stack (resp the ancestor of the the t op 1 -element of pop k psq / the link-ancestor) is v 0 , then the collapse-rank (resp the pop-rank / the link-rank) is simply the smallest colour seen since the beginning of the play. Hence, it does not make much sense but it permits the construction to remain uniform.

The next theorem shows that we can restrict our attention to CPDP games where the underlying CPDP is rank-aware.

Theorem 6. For any n-CPDP A " xΓ, Q, ∆, q 0 y and any associated parity game G, one can construct an n-CPDP A rk and an associated parity game G rk such that the following holds.

' There exists a mapping ν from the configurations of A to that of A rk such that:

for any configuration v 0 of A, A rk is rank-aware from νpv 0 q; -Éloïse has a winning strategy in G from some configuration v 0 iff she has a winning strategy in G rk from νpv 0 q;

' If there is an n-CPDA transducer S rk synchronised with A rk realising a well-defined winning strategy for Éloïse in G rk from νpq 0 , K n q, then one can effectively construct an n-CPDA transducer S synchronised with A realising a well-defined winning for Éloïse in G from the initial configuration pq 0 , K n q.

The proof of Theorem 6 is a non-trivial generalisation of [A4, Lemma 6.3] (which concerns 2-CPDP) to the general setting of n-CPDP and starting from an arbitrary configuration. The rest if the subsection is devoted to this proof.

Fix an n-CPDP A " x Γ, Q, ∆, q 0 y, a partition

Q E Z Q A of Q and a colouring function Ω : Q Ñ C Ă N.
Denote by G the induced parity game. We define a rank-aware (to be proven) n-CPDP A rk " x Γ rk , Q rk , ∆ rk , q 0,rk y such that Q rk " Q ˆC and Γ rk " Γ ˆpC Y töuq ˆpC Y tö, :uq ˆpC t1,...,nu Y töuq

We define a map ν that associates with any configuration of A a configuration of A rk . Let pq, sq be a configuration in A. Then νpq, sq " ppq, Ωpqqq, s 1 q where s 1 is obtained by: ' Replacing every internal symbol γ (i.e. that is not the t op 1 -element) by pγ, ö, ö, öq if it has an n-link and by pγ, ö, :, öq otherwise.

' Replacing the t op 1 -element γ by pγ, Ωpqq, Ωpqq, Ωpqqq if it has an n-link and otherwise by pγ, Ωpqq, :, Ωpqqq.

We equip A rk with a colouring function Ω rk by letting Ω rk pq, θq " Ωpqq. Our construction will satisfy the following invariant. Let Λ be a finite path (in GraphpA rk q) starting in some configuration νpq, sq ending in some configuration ppq, θq, sq then the following holds. First, θ is the minimal colour visited from the beginning of the path. Second, if t op 1 psq " pα, m c , m l , τ q then ' m c is the collapse-rank; ' m l is the link-rank if it makes sense (i.e. there is an n-link in the current t op 1 -symbol) or is : otherwise; ' τ is the pop-rank: τ piq is the pop-rank for i for every 1 ď i ď n. Let us now explain how ν is defined. Let pq, sq be some configuration in A. Then νpq, sq " ppq, Ωpqq, s 1 q where s 1 is obtained by: ' Replacing every internal symbol γ (i.e. that is not the t op 1 -element) by pγ, ö, ö, öq if it has an n-link and by pγ, ö, :, öq otherwise.

' Replacing the t op 1 -element γ by pγ, Ωpqq, Ωpqq, Ωpqqq if it has an n-link and otherwise by pγ, Ωpqq, :, Ωpqqq.

Trivially, at the beginning of the path the invariant holds. The transition function of A rk mimics that of A and updates the ranks as explained below. First, let us explain the meaning of symbols ö. Such symbols will never been created using a push _,k 1 or a r ew ö 1 action: hence they can only be duplicated (using push k ) from symbols originally in the stack. The meaning of a symbol ö is that the corresponding object (collapse-rank, link-rank or pop-rank) has not yet been settled. However, when a ö symbol appears in the t op 1 -element the various ranks can be easily retireved as they necessarily equal the smallest colour visited so far (as noted in Remark 7): this is why we made the computation of the minimal colour visited so far in the control state of A rk .

In order to make the construction more readable, we do not formally describe ∆ rk but rather explain how A rk behaves. It should be clear that ∆ rk can be formally described to fit this informal description (and that some extra control states are actually needed as we allow to do several stack operation per transition); technical issues about this construction are discussed in Remark 8. Note that the description below also contains the inductive proof of its validity, namely that m c , m l and τ are as stated above. To avoid case distinction on whether the link-rank is defined or not, we take the following convention that minp:, iq " : for every i P N.

The intuitive idea is the following. One stores in the stack information on the various ranks, and after performing a pop k or a collapse, one needs to update the information stored in the new t op 1 -element. Indeed this information has no longer been updated since the ancestor configuration (this was the last time it was on top of the stack). To update it, one uses either the collapse-rank / pop-rank in the previous configuration, which is exactly what is needed for this update.

Assume A rk is in configuration v ℓ " ppq, θq, sq with t op 1 psq " pα, m c , m l , τ q and let v 0 v 1 ¨¨¨v ℓ be the beginning of the path of GraphpA rk q where we denote v i " ppq i , θ i q, s i q (hence q ℓ " q and s ℓ " s). For any pq 1 , r ew γ 1 ; opq P ∆pq, αq (note that the case where no r ew 1 is performed corresponds to the case where γ " α) the following behaviours are those allowed in ppq, θq, sq.

1) Assume op " pop k for some 1 ď k ď n, let pop k psq " s 1 and let t op 1 ps 1 q " pα 1 , m 1 c , m 1 l , τ 1 q. Then A rk can go to the configuration ppq 1 , θ 1 q, s 2 q where θ 1 " minpθ, Ωpq 1 qq and s 2 is obtained from s 1 by replacing t op 1 ps 1 q by a)

pα 1 , θ 1 , θ 1 , pθ 1 , . . . , θ 1 qq if m 1 c "ö, m 1 l "ö and τ 1 " pö, . . . , öq. b) pα 1 , θ 1 , :, pθ 1 , . . . , θ 1 qq if m 1 c "ö, m 1 l " : and τ 1 " pö, . . . , öq. c) pα 1 , minpm 1 c , τ pkq, Ωpq 1 qq, minpm 1 l , τ pkq, Ωpq 1 qq, τ 2 q, with τ 2 piq " # minpτ 1 piq, τ pkq, Ωpq 1 qq if i ď k minpτ piq, Ωpq 1 qq if i ą k
Cases paq and pbq correspond to the case where one reach (possibly a copy) of a symbol that was in the stack from the very beginning and that never appeared as a t op 1 -element: then the value of the collapse-rank, link-rank (if defined this is case paq otherwise it is case pbq) and pop-ranks are all equal to θ 1 . We now explain case pcq. Let v x be the ancestor of t op 1 ppop k psqq. Then x ą 0 as otherwise we would be in case paq or pbq. By Proposition 4, it follows that t op 1 ppop k psqq " t op 1 ps x´1 q, and by induction hypothesis, at step px ´1q, m 1 c , m 1 l and τ 1 had the expected meaning. Let y be the index of the t op 1 -element of the pointed stack in s 1 : y is also the t op 1 -element of the pointed stack in s x´1 , and moreover y ă x. The collapse-rank in v ℓ`1 is mintΩpq y q, . . . , Ωpq x´1 q, Ωpq x q, . . . , Ωpq n q, Ωpq 1 qu " mintmintΩpq y q, . . . , Ωpq x´1 qu, mintΩpq x q, . . . , Ωpq n qu, Ωpq 1 qu " mintm 1 c , τ pkq, Ωpq 1 qu Similarly, when defined, the link-ancestor of s 1 is the same as the one in s x´1 : hence the pop-rank in v ℓ`1 is mintm 1 l , τ pkq, Ωpq 1 qu. For any i ď k, t op 1 ppop i ps 1 qq " t op 1 ps x´1 q and therefore the pop-rank for i in v ℓ`1 is obtained by updating τ 1 piq to take care of the minimum colour seen since v x -which (as for the collapse-rank) is mintτ pkq, Ωpq 1 qu: therefore the pop-rank for i in v ℓ`1 equals mintτ 1 piq, τ pkq, Ωpq 1 qu. For any i ą k, pop i ps 1 q " pop i psq and thus t op 1 ppop i ps 1 qq " t op 1 ppop i psqq. Therefore the pop-rank for i in v ℓ`1 is obtained by updating the one in v ℓ to take care of the new visited colour Ωpq 1 q: hence the pop-rank for i in v ℓ`1 equals mintτ piq, Ωpq 1 qu.

2) Assume op " collapse, let collapsepsq " s 1 and let t op 1 ps 1 q " pα 1 , m 1 c , m 1 l , τ 1 q. Then A rk can go to the configuration ppq 1 , θ 1 q, s 2 q where θ 1 " minpθ, Ωpq 1 qq and s 2 is obtained from s 1 by replacing t op 1 ps 1 q by a)

pα 1 , θ 1 , θ 1 , pθ 1 , . . . , θ 1 qq if m 1 c "ö, m 1 l "ö and τ 1 " pö, . . . , öq. b) pα 1 , θ 1 , :, pθ 1 , . . . , θ 1 qq if m 1 c "ö, m 1 l " : and τ 1 " pö, . . . , öq. c) pα 1 , minpm 1 c , m c , Ωpq 1 qq, minpm 1 l , m c , Ωpq 1 qq, τ 2 q with τ 2 piq " # minpτ 1 piq, m c , Ωpq 1 qq if i ď k minpτ piq, Ωpq 1 qq if i ą k
The proof follows the same line as for the previous case (pop k ).

Cases paq and pbq correspond to the case where one reach (possibly a copy) of a symbol that was in the stack from the very beginning and that never appeared as a t op 1 -element: then the value of the collapse-rank, link-rank (if defined this is case paq otherwise it is case pbq) and pop-ranks are all equal to θ 1 . We now explain case pcq. Let v x be the collapse-ancestor of v ℓ . Then x ą 0 as otherwise we would be in case paq or pbq. By induction hypothesis, m 1 c and τ 1 give the collapse-rank / link-rank / pop-ranks in v x´1 . Moreover the ancestor of the t op 1 -element of the target of the top link in s 1 is the same as the one in v x´1 . Therefore the collapse-rank is obtained by taking the minimum of the collapse-rank in v x´1 with mintΩpq x q, . . . Ωpq n q, Ωpq 1 qu " mintm c , Ωpq 1 qu.

Similarly (if defined) the link-ancestor in s 1 being the same as the one in v x´1 , the link-rank is obtained by taking the minimum of the one in v x´1 with mintΩpq x q, . . . Ωpq n q, Ωpq 1 qu " mintm c , Ωpq 1 qu.

Let i ď k. The ancestor of t op 1 ppop i ps 1 qq is the same as the ancestor of t op 1 ppop i ps x´1 qq. Therefore the pop-rank for i in v ℓ`1 is obtained by taking the minimum of the one in v x´1 with mintΩpq x q, . . . Ωpq n q, Ωpq 1 qu " mintm c , Ωpq 1 qu. Let i ą k. Then the ancestor of t op 1 ppop i ps 1 qq is the same as the ancestor of t op 1 ppop i ps n qq: indeed the collapse only modified the t op k stack. Therefore the pop-rank for i in v ℓ`1 is obtained by taking the minimum of the one in v ℓ with the new visited colour Ωpq 1 q. 3) Assume op " push j for some 2 ď j ď n, let push j pr ew pγ,mc,m l ,τ q 1 psqq " s 1 and let t op 1 ps 1 q " pγ, m c , m l , τ q (note that ö does not appear in t op 1 ps 1 q). Then, A rk can go to the configuration ppq 1 , θ 1 q, s 2 q where θ 1 " minpθ, Ωpq 1 qq and s 2 is obtained from s 1 when replacing t op 1 ps 1 q by pγ, minpm c , Ωpq 1 qq, minpm l , Ωpq 1 qq, τ 1 q with τ 1 piq "

# minpτ piq, Ωpq 1 qq if i ‰ j Ωpq 1 q if i " j
Indeed, the collapse-ancestor in the new configuration is the same as the one in s. As by induction hypothesis m c is the collapse-rank in v ℓ , the collapse-rank in v ℓ`1 is obtained by updating m c to take care of the new visited colour, namely by taking mintm c , Ωpq 1 qu. Similarly, if defined, the link-ancestors in v ℓ and v ℓ`1 are identical and then the link-rank in v ℓ`1 is mintm c , Ωpq 1 qu.

For any i ‰ j, the ancestor of t op 1 ppop i psq 1 q and the ancestor of t op 1 ppop i ps 1 qq are the same. Again using the induction hypothesis one directly gets that the pop-rank for i in v ℓ`1 equals mintτ piq, Ωpq 1 qu.

The index of the ancestor of top 1 ppop j ps 1 qq is by definition ℓ `1. Hence as the only colour visited since v ℓ`1 is Ωpq 1 q it equals the pop-rank for j. 4) Assume op " push β,k 1 with 1 ď k ď n, and β P pΓztKuq. Then A rk can go to pq 1 , θ 1 q, where θ 1 " minpθ, Ω 1 pq 1 qq, and apply successively r ew pγ,mc,m l ,τ q 1 and push

pβ,m 1 c ,m 1 l ,τ 1 q,k 1
where m 1 c " minpτ pkq, Ωpq 1 qq, m 1 l " Ωpq 1 q if k " n and m 1 l " : otherwise, and τ 1 piq " minpτ piq, Ωpq 1 qq for every i ě 2 and τ p1q " Ωpq 1 q. Indeed, the pointed stack in s 1 is t op k ppop k psqq and therefore the collapse-rank in v ℓ`1 is the minimum of the pop-rank for k in s and of the new visited colour Ωpq 1 q, that is mintτ pkq, Ωpq 1 qu. If k " n, the link-ancestor of v ℓ`1 is v ℓ`1 itself and hence the link-rank is the colour of the current configuration, namely Ωpq 1 q. For any i ě 2, as pop i psq " pop i ps 1 q one also has t op 1 ppop i ps 1 qq " t op 1 ppop i psqq and therefore the pop-rank for i in v ℓ`1 equals the minimum of the one in v ℓ with the new visited colour Ωpq 1 q, that is mintτ piq, Ωpq 1 qu. Finally as the ancestor of pop 1 ps 1 q is v ℓ`1 then the pop-rank for 1 is the current colour, namely Ωpq 1 q.

From the previous description (and the included inductive proof) we conclude that, for any configuration v 0 of A, A rk is rank-aware from νpv 0 q. Remark 8. One must object that A rk does not fit the definition of n-CPDP. Indeed, in a single transition it can do a top-rewriting followed by another stack operation and followed again by a top-rewriting (which itself depends on the new t op 1 -element). One could add intermediate states and simply decompose such a transition into two transitions, but this would be problematic later when defining an n-CPDA transducer realising a winning strategy.

Hopefully, one can define a variant A 1 rk of A rk that has the same properties as A rk and additionally fits the definition of n-CPDP. The idea is simply to postpone the final top-rewriting to the next transition. Indeed, it suffices to add a new component on the control state where one encodes the top-rewriting that should be performed next: this top-rewriting is then performed in the next transition (note that this fits the definition as performing two top-rewriting is the same as only doing the last one). However, there is still an issue as the top-rewriting was actually depending on the t op 1 -symbol (one updates the various ranks) hence, one cannot save the next top-rewriting in the control state without first observing the symbol to be rewritten. But this is not a problem, as it suffices to remember which kind of update should be done (one concerning a pop k or one concerning a collapse) and to store in the control state the various objects needed for this update (for this one can simply store the former t op 1 -element).

One also need to slightly modify the LinkRk function so that it return the link-rank of the t op 1 -symbol after it is rewritten. This can easily be done as the domain of LinkRk is Q rk ˆΓrk .

Note that A 1 rk and A rk use the same stack alphabet, but that the state space of A rk uses an extra component of size linear in the one of the stack alphabet.

In conclusion building a rank-aware (valid) n-CPDP from a non-aware one increases (by a multiplicative factor) the stack alphabet by C n`3 and the state set by OpC n`3 q.

For now on, we uses A rk to mean A 1 rk . We are now ready to conclude the proof of Theorem 6. First recall that we defined Ω rk by letting Ω rk pq, θq " Ωpqq. Then, we define a partition Q rk,E Z Q rk,A of Q rk by letting the states in Q rk,E to be those states with their first component in Q E , and those states in Q rk,A to be those states with their first component in Q A . Let G rk be the corresponding arena and let G rk be the corresponding n-CPDP parity game.

Consider the projection ζ defined from configurations of A rk into configurations of A by only keeping the first component of the control state, and by only keeping the Γ part of symbols appearing in the stack. Note that, on the domain of ν ´1, ζ and ν ´1 coincide. Also note that ζ preserve the shape of stacks 9 , i.e. for any configuration v rk , the stack in v rk has the same shape as the stack in νpv rk q.

We extend ζ as a function from (possibly partial) plays in G rk into (possibly partial) plays in G by letting ζpv 1 0 v 1 1 ¨¨¨q " ζpv 1 0 qζpv 1 1 q ¨¨¨. It is obvious that for any play Λ 1 in G rk starting from νpv 0 q, its image ζpΛ 1 q is a play in G starting from v 0 ; moreover these two plays induces the same sequence of colours and at any round the player that controls the current configuration is the same in both plays. Conversely, from the definition of A rk it is also clear that there is, for any play Λ in G starting from v 0 , a unique play Λ 1 in G rk starting from νpv 0 q such that ζpΛ 1 q " Λ.

In particular, ζ can be used to construct a strategy in G from a strategy in G rk . Indeed, let Φ rk be a strategy for Éloïse from νpv 0 q in G rk . We define a strategy Φ in G from νpv 0 q. This strategy maintains as a memory a partial play Λ rk in G rk such that, if Éloïse respects Φ, in G starting from v 0 after having played Λ one has ζpΛ rk q " Λ and moreover Λ rk is a play in G rk starting from νpv 0 q where Éloïse respects Φ rk . Initially, we let Λ rk " νpv 0 q. Assume that we have been playing Λ and that Éloïse has to play next. Then she considers v rk " Φ rk pΛ rk q and she plays to v where v is the unique configuration such that ζpΛ rk ¨vrk q " Λ ¨v. Finally one updates Λ rk to be Λ rk ¨vrk . If it is Abelard that has to play next and if he moves to some v, then Éloïse updates Λ rk to be Λ rk ¨vrk where v rk is the unique configuration such that Λ rk ¨vrk is a valid play and such that ζpv rk q " v. A symmetrical construction can be done to build a strategy of Abelard in G from one in G rk . Now, assume that νpv 0 q is winning for Éloïse (resp. Abelard) and call Φ rk an associated winning strategy. Let Φ be the strategy in G obtained as explained above. Then Φ is winning for Éloïse (resp. Abelard) in G from v 0 (this follows directly from the fact that Φ rk is winning and that we have the property that ζpΛ rk q " Λ for any partial play Λ in G consistent with Φ). Hence this proves that Éloïse has a winning strategy in G from v 0 iff she has a winning strategy in G rk from νpv 0 q.

Finally, from the previous construction of a strategy Φ from a strategy Φ rk we prove that if there is an n-CPDA transducer S rk synchronised with A rk realising a well-defined winning strategy Φ rk for Éloïse in G rk from νpq 0 , K n q, then one can effectively construct an n-CPDA transducer S synchronised with A realising a well-defined winning strategy Φ for Éloïse in G from the initial configuration pq 0 , K n q. Indeed, in our previous construction of Φ, we maintained a partial play Λ rk in G rk and used the value of Φ rk pΛ rk q to define ΦpΛq. But if Φ rk is realised by an n-CPDA transducer S rk , it suffices to remember the configuration of this transducer after playing Λ rk (as this suffices to compute ϕ rk pΛ rk qq. Hence, the only things that need to be modified from S rk to obtain S is that one needs to "embed" the transition function of A rk into it, so that S can read/output elements in Q ˆOp n pΓq ˆOp n pΓq instead of Q rk ˆOp n pΓ rk q ˆOp n pΓ rk q. This can easily (but writing the formal construction would be quite heavy) be achieved by noting that the shape of stacks is preserved by ζ: hence if S rk is synchronised with A rk then S is synchronised with A (as A rk and A are "synchronised", and S rk and S are "synchronised" as well).

If we summarise, the overall blowup in the transformation from G to G rk given by Theorem 6 is as follows.

Proposition 5. Let A and A rk be as in Theorem 6. Let t0, ¨¨¨, du be the set of colours. Then the set of states of A rk has size Op|Q|pd `1q n`3 q and the stack alphabet of A rk has size Op|Γ|pd `1q 2n`5 q.

Moreover the set of colours used in G and G rk are the same.

Proof: By construction together with Remark 8.

6)

Removing the n-links: .

In this subsection, we show how one can remove the outmost links.

Theorem 7. For any rank-aware n-CPDP A rk " xΓ rk , Q rk , ∆ rk , q 0,rk y and any associated parity game G rk , one can construct an n-CPDP A lf and an associated parity game G lf such that the following holds.

' A lf does not create n-links.

' There exists a mapping ν from the configurations of A rk to that of A lf such that:

-Éloïse has a winning strategy in G rk from some configuration v 0 iff she has a winning strategy in G lf from νpv 0 q;

' If there is an n-CPDA transducer S lf synchronised with A lf realising a well-defined winning strategy for Éloïse in G lf from νpq 0,rk , K n q, then one can effectively construct an n-CPDA transducer S rk synchronised with A rk realising a well-defined winning strategy for Éloïse in G rk from the initial configuration pq 0,rk , K n q.

The whole section is devoted to the proof of Theorem 7 and we thus fix from now on, a rank-aware n-CPDP A rk " x Γ rk , Q rk , ∆ rk , q 0,rk y (together with a function LinkRk), a partition Q rk,E Z Q rk,A of Q rk , a colouring function Ω : Q rk Ñ C Ă N and we let C " t0, . . . , du. Denote by G rk the transition graph of A rk , by G rk the arena induced by G rk and the partition Q rk,E Z Q rk,A , and by G rk the parity game pG rk , Ωq.

Consider the following informal description of a new game G lf (here lf intend to mean link-free) defined from G rk . The new game mimics G rk except that whenever a player wants to perform a push γ,n 1 operation, this is replaced by the following "negotiation" between the players: ' First, Éloïse has to provide a vector Ý Ñ R " pR 0 , ¨¨¨R d q P p2 Q rk q d`1 whose intended meaning is the following: she claims that she has a strategy such that if the newly created n-link (or a copy of it) is eventually used by doing a collapse then it leads to a state in R i where i is the smallest colour visited since the original copy of the link was created.

' Then, Abelard has two options. He can agree with Éloïse's claim, pick a state q in some R i and perform a pop n action whilst going to state q (through an intermediate dummy vertex coloured by i): this is the case where Abelard wants to simulate a collapse involving the n-link. Alternatively Abelard can decide to push the symbol pγ, Ý Ñ R q (and a dummy 1-link is attached). Later in some configuration pq, sq with a top 1 -element of the form pγ, Ý Ñ R q if the player controlling q wants to simulate a transition pq 1 , op; collapseq that collapses the stack, then this move is replaced by one that goes to a sink configuration that is winning for Éloïse iff q 1 P R i where i " LinkRkpq, γq is the link rank and hence corresponds to the smallest colour visited since the original copy of symbol pγ, Ý Ñ R q was pushed onto the stack (recall that A rk is rank-aware). The intuitive idea is that, when simulating a collapse (involving an order-n link), Éloïse wins iff her initial claim on the possible states reachable by following the link was correct. Otherwise she loses.

We now define A lf and the associated game G lf . We start with an informal description of A lf and then formally describe its structure.

The n-CPDP A lf simulates A rk as follows. Assume that the play is in some configuration pq, sq and that the player that controls it wants to simulate a transition pq 1 , r ew α 1 ; opq P ∆ rk pq, t op 1 psqq. In case op is neither of the form push β,n 1 nor of the form collapse with t op 1 psq having an n-link then the same transition pq 1 , r ew α 1 ; opq is available in A rk and is performed. The interesting case is when op " push β,n 1 , and it is simulated by A lf as follows. ' The control state of A lf is updated to be q β and one performs r ew α 1 . ' From q β , Éloïse has to move to a new control state q ? and can push any symbol of the form pα, Ý Ñ R q where Ý Ñ R " pR 0 , ¨¨¨R d q P p2 Q q d`1 . A dummy 1-link is attached (and will never be used for a collapse). ' From q ? , Abelard has to play and choose between one of the following two options:

either go to state q and perform no action on the stack, -or pick a state p in some R i , go to an intermediate new state p i (of colour i) without changing the stack and from this new configuration go to state p and perform a pop n action. The intended meaning of such a decomposition of the push β,n 1 operation is the following: when choosing the sets in Ý Ñ R , Éloïse is claiming that she has a strategy such that if the n-link created by pushing β is eventually used for collapsing the stack then the control state after collapsing will belong to R i where i is meant to be the smallest colour from the creation of the link to the collapse of the stack (equivalently it will be the link rank -as computed in A rk -the just before collapsing). Note that the R i are arbitrary sets because Éloïse has not a full control on the play (and in general cannot force R i to be a singleton). Then Abelard is offered to simulate the collapse (here state p i is only used for going through a state of colour i). If he does not want to simulate a collapse then one stores Ý Ñ R for possibly checking its truth later in the play. Assume that later, in configuration pp 1 , s 1 q one of the two players wants to simulate a transition pp 2 , r ew β 1 ; collapseq involving an n-link. By construction, t op 1 ps 1 q is necessarily of the form pγ, Ý Ñ R q. Then the simulation is done by going to a sink configuration that is winning for Éloïse iff p 2 P R LinkRkpp 1 ,γq , i.e. Éloïse wins iff her former claim on Ý Ñ R was correct. Formally we set A lf " x Γ lf , Q lf , ∆ lf , q 0,lf y with

' Γ lf " Γ rk Y Γ rk ˆp2 Q rk q d`1 ' Q lf " Q rk Y tq γ | q P Q rk , γ P Γ rk u Y tq ? | q P Q rk u Y tq i | q P Q rk , 0 ď i ď du Y ttt, ff u ' If op " push β,n 1
then Éloïse plays plays pq β , r ew α 1 ; idq if t op 1 psq " γ and she plays pq β , r ew pα,

Ý Ñ R q 1 ; idq if t op 1 psq " pγ, Ý Ñ R q.
In this last case, or in the case where p P Q A and Abelard plays some pq β , r ew α 1 ; idq (resp. some pq β , r ew pα, Ý Ñ R q 1

; idq), we also have to explain how Éloïse behaves from pq β , r ew α 1 psqq (resp. pq β , r ew pα,

Ý Ñ R q 1 psqq.
Éloïse has to play pq ? , push pβ, Ý Ñ S q,1 1 q where Ý Ñ S P p2 Q rk q d`1 describes which states can be reached if the n-link created by pushing β (or a copy of it) is used for collapsing the stack, depending on the smallest visited colour in the meantime. In order to define Ý Ñ S , she considers the set of all possible continuations of Λ rk ¨pq, push β,n 1 pσqq (where pp, σq denotes the last vertex of Λ rk ) where she respects her strategy Φ rk . For each such play, she checks whether some configuration of the form pr, pop n pσqq is eventually reached by collapsing (possibly a copy of the) n-link created by push β,n

1 . If such an r exists, she considers the smallest colour i visited from the moment where the link was created to the moment collapse is performed (i.e. the link rank just before collapsing). For every i P t0, . . . du, the set S i is defined to be the set of states r P Q such that the preceding case happens. Formally, S i " tr | D Λ rk ¨v0 ¨¨¨v k ¨vk`1 ¨¨¨play in G rk where Éloïse respects Φ rk and s.t. v 0 " pq, push β,n 1 pσqq, v k`1 " pr, pop n pσqq is obtained by applying collapse from v k , v 0 is the link ancestor of v k and i is the link rank in v k u

Finally, we set Ý Ñ S " pS 0 , . . . , S d q and Éloïse plays pq ? , push pβ,

Ý Ñ S q,1 1
q.

Update of Λ rk . The memory Λ rk is updated after each visit to a configuration with a control state in Q rk Y ttt, ff u. We have several cases depending on the transition.

' If the last transition is of the form pq, r ew α 1 ; opq or pq, r ew pα,

Ý Ñ R q 1
; opq with op being neither of the form push β,n 1 nor collapse, then we extend Λ rk by applying transition pq, r ew α 1 ; opq, i.e. if pp, σq denotes the last configuration in Λ rk , then the updated memory is Λ rk ¨pq, oppr ew α 1 pσqqq. ' If the last transition is of the form ptt, idq or pff, idq, the play is in a sink configuration. Therefore we do not update Λ rk as the play will loop forever.

' If the last transitions form a sequence of the form pq β , r ew α 1 ; idq ¨pq ? , push pβ, Ý Ñ S q,1 1 q ¨pq, idq or of the form

pq β , r ew pα, Ý Ñ R q 1
; idq ¨pq ? , push pβ, Ý Ñ S q,1 1 q ¨pq, idq, then the updated memory is Λ rk ¨pq, push β,n 1 pσqq, where pp, σq denotes the last configuration in Λ rk .

' If the last transitions form a sequence of the form pq β , r ew α 1 ; idq ¨pq ? , push pβ, Ý Ñ S q,1 1 q ¨pr i , idq ¨pr, pop n q or of the form

pq β , r ew pα, Ý Ñ R q 1 ; idq ¨pq ? , push pβ, Ý Ñ S q,1 1
q ¨pr i , idq ¨pr, pop n q, then we extend Λ rk by a sequence of actions (consistent with Φ rk ) that starts by performing transition pq, push β,n 1 q and ends up by collapsing (possibly a copy of) the link created at this first step and goes to state p while visiting i as a minimal colour in the meantime. By definition of Ý Ñ S such a sequence always exists. More formally, if pp, σq denotes the last configuration in Λ rk , then the updated memory is a play in G rk , Λ rk ¨v0 ¨¨¨v k ¨vk`1 , where Éloïse respects Φ rk and such that v 0 " pq, push β,n 1 pσqq, v k`1 " pr, pop n pσqq is obtained by applying collapse from v k , v 0 is the link ancestor of v k and i is the link rank in v k . Therefore, with any partial play Λ lf in G lf in which Éloïse respects her strategy Φ lf , is associated a partial play Λ rk in G rk . An immediate induction shows that Λ rk is a play where Éloïse respects Φ rk . The same arguments works for any infinite play Λ lf that does not contain a state in ttt, ff u, and the corresponding play Λ rk is therefore infinite, starts from νpp 0 , s 0 q and Éloïse respects Φ rk in that play. Therefore it is a winning play.

Moreover, if Λ lf is an infinite play that does not contain a state in ttt, ff u, it easily follows from the definitions of Φ lf and Λ rk that the smallest infinitely visited colour in Λ lf is the same as the one in Λ rk . Hence, any infinite play in G lf starting from νpp 0 , s 0 q where Éloïse respects Φ lf and that does not contain a state in ttt, ff u is won by Éloïse. Now, consider a play that contains a state in ttt, ff u (hence loops on it forever). Reaching a configuration with state in ttt, ff u is necessarily by simulating a collapse from some configuration with a t op 1 -element of the form pα, Ý Ñ R q. We should distinguish between those elements pα, Ý Ñ R q that are "created" before (i.e. by the ν function) or during the play (by Éloïse). For the second ones, one may note that whenever Éloïse wants to simulate a collapse, she can safely goes to state tt (meaning Φ lf is well defined): indeed, if this was not the case, it would contradict the way Ý Ñ S was defined when simulating the original creation of the link. For the same reason, Abelard can never reach state ff provided Éloïse respects her strategy Φ lf . Now consider an element pα, Ý Ñ R q created by ν and assume that one player wants to simulate a collapse from some configuration with such a t op 1 -element. Call Λ lf the partial play just before and call Λ rk the associated play in G rk . Then in Λ rk , Éloïse respects her winning strategy Φ rk . If she has to play next in Λ rk , strategy Φ rk indicates to play collapse; if it is Abelard's turn to move he can play collapse. In both case, the configuration that is reached after collapsing is winning for Éloïse (it is a configuration visited in a winning play). Hence, by definition of ν, its control state belongs to R where Ý Ñ R " pR, ¨¨¨, Rq, and therefore from the current vertex in G lf there are no transition to ff and there is at least one to tt. Therefore plays where Éloïse respects Φ lf and that contain a state in ttt, ff u necessarily contains state tt hence are won by Éloïse.

Altogether, it proves that Φ lf is a winning strategy for Éloïse in G lf from νpv 0 q.

Let us now prove the converse implication Assume that the configuration νpp 0 , s 0 q is winning for Éloïse in G lf , and let Φ lf be a winning strategy for her. Using Φ lf , we define a strategy Φ rk for Éloïse in G rk from pp 0 , s 0 q. First, recall how νpp 0 , s 0 q is defined: every symbol α in s with an n-link is replaced by a pair pα, pR, . . . , Rqq where R is the set of states r such that Éloïse wins from pr, s 1 q where s 1 is the stack obtained by first removing every symbol (and stacks) above α and then performing a collapse. We can therefore assume that we have a collection of winning strategies, one per each such configurations pr, s 1 q -call such a strategy Φ r,s 1 rk . Then, during a play where Éloïse respects Φ rk , if one eventually visits such a configuration pr, s 1 q, the strategy Φ rk will mimic the winning strategy Φ r,s 1 rk from that point and therefore the resulting play will be winning for Éloïse. Then in the rest of this description we mostly focus on the case of plays where this phenomenon is not happening.

The strategy Φ rk maintains as a memory a partial play Λ lf in G lf , that is an element in V l f (where V lf denotes the set of vertices of G lf ). At the beginning Λ lf is initialised to the configuration νpp 0 , s 0 q. After having played Λ rk , the play Λ lf will satisfy the following invariant. Assume that the play Λ lf ends in a configuration pp, sq then the following holds.

' If t op 1 psq " α, the last configuration of Λ rk has control state p and its t op 1 -element is α and it has a k-link for some k ă n. ' If t op 1 psq " pα, Ý Ñ R q, the last configuration of Λ rk has control state p and its t op 1 -element is α and it has an n-link. Moreover, if Éloïse keeps respecting Φ rk in the rest of the play, if (possibly a copy of) this link is eventually used in a collapse, then the state that will be reached just after doing the collapse will belong to R i where i will be the link rank just before collapsing. We first describe Φ rk and we then explain how Λ lf is updated. Recall that we switch to a known winning strategy in case we do a collapse from (possibly a copy of) an n-link that was already in s 0 .

Choice of the move. Assume that the play is in some vertex pp, sq with p P Q rk,E . The move given by Φ rk depends on Φ lf pΛ lf q " pq, rew; opq (we shall later argue that Φ lf is well defined while proving that it is winning).

' If q P Q rk then Éloïse plays pq, r ew α 1 ; opq where α is such that either rew " r ew α 1 or rew " r ew pα, Ý Ñ R q

1

. Note that in this case, op is neither a collapse involving an n-link nor of the form push β,n 1 . ' If q " r β then Éloïse plays to pr, r ew α 1 ; push β,n 1 q where α is such that either rew " r ew α 1 or rew " r ew pα,

Ý Ñ R q 1 .
' If q " tt then Éloïse plays pr, collapseq for some arbitrary r P R i where we let i " LinkRkpp, t op 1 psqq and pα, Ý Ñ R q denotes the t op 1 -element of the last vertex of Λ lf . Note that in this case, the collapse involves an n-link.

Update of Λ lf . The memory Λ lf is updated after each move (played by any of the two players). We have several cases depending on the last transition.

' If the last transition is of the form pq, r ew α 1 ; opq and op is neither a collapse involving an n-link nor of the form push β,n 1 , then Λ lf is extended by mimicking the same transition, i.e. if pp, σq denotes the last configuration in Λ lf , then the updated memory is Λ lf ¨pq, oppr ew α 1 pσqq if t op 1 pσq " γ for some γ P Γ rk , and is Λ lf ¨pq, oppr ew pα, Ý Ñ R q 1 pσqq if t op 1 pσq " pγ, Ý Ñ R q for some pγ, Ý Ñ R q P Γ lf . ' If the last transition is of the form pq, r ew α 1 ; push β,n 1 q then, we let pp, σq denotes the last configuration in Λ lf . If t op 1 pσq " γ for some γ P Γ rk then the updated memory Λ lf ¨pq β , r ew α 1 pσqq ¨pq ? , push pβ,

Ý Ñ R q,1 1 pr ew α 1 pσqqq pq, push pβ, Ý Ñ R q,1 1
pr ew α 1 pσqqq where Φ lf pΛ lf ¨pq β , r ew α 1 pσqqq " pq ? , push pβ,

Ý Ñ R q,1 1
pr ew α 1 pσqqq. If t op 1 pσq " pγ, Ý Ñ S q for some pγ, Ý Ñ S q P Γ lf then the updated memory Λ lf ¨pq β , r ew pα,

Ý Ñ S q 1 pσqq pq ? , push pβ, Ý Ñ R q,1 1 pr ew pα, Ý Ñ S q 1 pσqqq ¨pq, push pβ, Ý Ñ R q,1 1 pr ew pα, Ý Ñ S q 1 pσqqq where Φ lf pΛ lf ¨pq β , r ew pα, Ý Ñ S q 1 pσqqq " pq ? , push pβ, Ý Ñ R q,1 1 pr ew pα, Ý Ñ S q 1
pσqqq.

' If the last transition is of the form pr, collapseq and the collapse follows to an n-link, then we have two cases. Either the collapse was following (possibly a copy of) an n-link that was already in s 0 in case we claim (and prove later) that one ends up in a winning configuration and then switch to a corresponding winning strategy as already explained.

Either one follows an n-link that was created during the play, in which case we let Λ lf " v 0 ¨¨¨v m and denote by v i the link ancestor of v m 10 . Then the updated memory is obtained by backtracking inside Λ lf until reaching the configuration where the (simulation of the) collapsed n-link was created (this configuration is v i , the link ancestor) and then extend it by a choice of Abelard consistent with the collapse. That is the updated memory is v 0 ¨¨¨v i ¨pr ℓ , σq ¨pr, pop n pσqq where v i " pp ? , σq and ℓ denotes the link rank in the configuration Λ rk was just before doing the collapse. Therefore, with any partial play Λ rk in G rk in which Éloïse respects her strategy Φ rk , is associated a partial play Λ lf in G lf . Note that if we end up in a configuration that is known to be winning, Λ lf is no longer extended. This also implies that when collapsing an n-link that was already in s 0 one necessarily ends up in a winning configuration. Indeed assume the contrary and let Λ lf be the constructed play before collapsing: then either Éloïse has to play and therefore moves to tt (and therefore the configuration in Λ rk after collapsing is winning by definition of ν, leading a contradiction) of Abelard could move to ff (leading a contradiction with Φ lf being winning). Therefore from now on we restrict our attention to the case where the n-links (and their copies) in s 0 are never used to do a collapse.

An easy induction shows that Éloïse respects Φ lf in Λ lf . The same arguments works for an infinite play Λ rk , and the corresponding play Λ lf is therefore infinite (one simply considers the limit of the Λ lf in the usual way 11 ), starts from νpp 0 , s 0 q, never visits a state in ttt, ff u and Éloïse respects Φ lf in that play. Therefore it is a winning play. Now, in order to conclude that any play Λ rk in G rk in which Éloïse respects strategy Φ rk is winning for her, one needs to relate the sequence of colours in Λ rk with the one in Λ lf . For this, we introduce a notion of factorisation of a partial play Λ rk " v 0 v 1 ¨¨¨v m in G rk (we should later note that it directly extends to infinite plays). A factor is a nonempty sequence of vertices of the following kind:

(1) it is a sequence v h ¨¨¨v k such that the stack operation from v h´1 to v h is of the form r ew α 1 ; push n,β 1 , the stack operation from v k´1 to v k is a collapse involving an n-link, and v h is the link ancestor of v k .

(2) or it is a single vertex; Then the factorisation of Λ rk denoted F actpΛ rk q is a sequence of factors inductively defined as follows (we underline factors to make them explicit): F actpΛ rk q " v 0 ¨¨¨v k , F actpv n`1 ¨¨¨v n q if there exists some k such that v 0 ¨¨¨v k is as in (1) above, and F actpΛ rk q " v 0 , F actpv 1 ¨¨¨v n q otherwise.

In the following, we refer to the colour of a factor as the minimal colour of its elements. Note that the previous definition is also valid for infinite plays. Now we easily get the following proposition (the result is obtained by reasoning on partial play using a simple induction combined with a case analysis. Then it directly extends to infinite plays). Proposition 6. Let Λ rk be some infinite play in G rk starting from pp 0 , s 0 q where Éloïse respects Φ rk and assume that there is no collapse that follows (possibly a copy of) an n-link already in s 0 . Let Λ lf be the associated infinite play in G lf constructed from Φ rk . Let Λ rk,0 , Λ rk,1 , ¨¨¨be the factorisation of Λ rk and, for every i ě 0, let c i be the colour of Λ rk,i .

Then the sequence pc i q iě0 and the sequence of colours visited in Λ lf have the same lim inf.

The previous proposition directly implies that Φ rk is a winning strategy for Éloïse from pp 0 , s 0 q in G rk .

In order to complete the proof of Theorem 7 it remains to establish the following proposition.

Proposition 7. If there is an n-CPDA transducer S lf synchronised with A lf realising a well-defined winning strategy for Éloïse in G lf from νpq 0,rk , K n q, then one can effectively construct an n-CPDA transducer S rk synchronised with A rk realising a well-defined winning strategy for Éloïse in G rk from the initial configuration pq 0,rk , K n q.

Proof: The result follows from a carefully analysis of how we defined Φ rk from Φ lf in the proof of Theorem 8. As we now only focus on the initial configuration pq 0,rk , K n q we will not have to deal with the special case of doing a collapse following (possibly a copy of) an n-link originally in the initial configuration. Also note that νpq 0,rk , K n q " pq 0,rk , K n q. 10 Here we implicitly extends the notion of link ancestor as follows. In G lf instead of creating n-link one pushes symbol of the form pβ, Ý Ñ R q: hence whenever doing a push pβ,

Ý Ñ R q,1 1
one attaches to the vector Ý Ñ R the index of the current configuration. Then if the top 1 element of vn is some pβ, Ý Ñ R q then the link ancestor of vm is defined to be v i where i is the indexed attached with Ý Ñ R . Note in particular that the control state in the link ancestor is necessarily of the form p ? . 11 Let punq ně0 be a sequence of finite words. For any n ě 0 let un " u 0 n ¨¨¨u kn n . Then the limit of the sequence punq ně0 is the (possibly infinite) word α " α 0 α 1 ¨¨¨such that α is maximal for the prefix ordering and for all 0 ď i ă |α| there is some N i such that u i n " α i for all n ě N i . In our setting, the play Λ lf associated with an infinite play Λ rk is defined as the limit of the sequence of partial plays pΛ n lf q ně0 where Λ n lf is the partial play associated with Λ rk truncated to its n `1 first vertices. From the definitions of the Λ n lf it is easily verified that the limit Λ lf is infinite.

An abstract pushdown automaton is a tuple A " xA, Q, ∆, q 0 y where A is a (possibly infinite) set called an abstract pushdown alphabet and containing a bottom-of-stack symbol denoted K P A, Q is a finite set of states, q 0 P Q is an initial state and ∆ :

Q ˆA Ñ 2 QˆA ď2
is the transition relation (here A ď2 " tεu Y A Y A ¨A are the words over A of length at most 2). We additionally require that for all a ‰ K, ∆pq, aq does not contain any element of the form pq, aKq nor pq, Kaq, and that ∆pq, Kq does not contain any element of the form pq 1 , εq nor pq 1 , aq nor pq, abq with a ‰ K or b " K, i.e. the bottom-of-stack symbol can only occur at the bottom of the stack, and is never popped nor rewritten. An abstract pushdown content is a word in St " KpAztKuq ˚. A configuration of A is a pair pq, uq with q P Q and u P St. Remark 9. In general an abstract pushdown automaton is not finitely describable, as the domain of ∆ is infinite and no further assumption is made on ∆.

Example 22. An order-1 pushdown process is an abstract pushdown automaton whose stack alphabet is finite.

A abstract pushdown automaton A induces a possibly infinite graph, called an abstract pushdown graph, denoted G " pV, Eq, whose vertices are the configurations of A and edges are defined by the transition relation ∆, i.e., from a vertex pq, u ¨aq one has an edge to pq 1 , u ¨u1 q whenever pq 1 , u 1 q P ∆pq, aq.

Example 23. Order-n CPDP that does not create n-links (i.e. never use stack operation of the form push γ,n 1 ) are special cases of abstract pushdown automata. Indeed, let n ą 1 and consider such an order-n CPDP A " xΓ, Q, ∆, q 0 y. Let A be the set of all order-pn ´1q stacks over Γ, and for every p P Q and a P A with γ " top 1 paq, we define ∆ 1 pp, aq by ' pq, εq P ∆ 1 pp, aq iff pq, pop n q P ∆pq, γq; ' pq, a 1 ¨a1 q P ∆ 1 pp, aq with a 1 " r ew α 1 paq iff pq, r ew α 1 ; push n q P ∆pq, γq; ' pq, a 1 q P ∆ 1 pp, aq with a 1 " oppr ew α 1 paqq iff pq, r ew α 1 ; opq P ∆pq, γq and op R tpop n , push n u. It follows that A and the abstract pushdown automaton xA, Q, ∆ 1 , q 0 y have isomorphic transition graphs.

Consider now a partition Q E Y Q A of Q between Éloïse and Abelard. It induces a natural partition V E Y V A of V by setting V E " Q E ˆSt and V A " Q A ˆSt. The resulting game graph G abs " pV E , V A , Eq is called an abstract pushdown game graph. Let Ω be a colouring function from Q to a finite set of colours C Ă N. This function is easily extended to a function from V to C by setting Ωppq, σqq " Ωpqq. Finally, an abstract pushdown parity game is a parity game played on such an abstract pushdown game graph where the colouring function is defined as above.

For every subset R Ď Q we define the conditional game induced by R over G abs , denoted G abs pRq, as the game played over G abs where a play Λ is winning for Éloïse iff one of the following happens:

' In Λ no configuration with an empty stack (i.e. of the form pq, Kq) is visited, and Λ satisfies the parity condition. ' In Λ a configuration with an empty stack is visited and the control state in the first such configuration belongs to R. More formally, the set of winning plays WpRq in G abs pRq is defined as follows (W par stands for the parity condition on G abs ):

WpRq " rW par zV ˚pQ ˆtKuqV ω s Y V ˚pR ˆtKuqV ω

For any state q, any stack letter a ‰ K, and any subset R Ď Q it follows from Martin's Determinacy theorem [A5] that either Éloïse or Abelard has a winning strategy from pq, Kaq in G abs pRq. We denote by Rpq, aq the set of subsets R for which Éloïse wins in G abs pRq from pq, Kaq: Rpq, aq " tR Ď Q | pq, Kaq is winning for Éloïse in G abs pRqu

We now build a new game whose winning region embeds all the information needed to determine the sets Rpq, aq. Moreover in the underlying game graph the vertices no longer encode stacks.

For an infinite play Λ " v 0 v 1 ¨¨¨in G abs , let Steps Λ be the set of indices of positions where no configuration of strictly smaller stack height is visited later in the play. More formally, Steps Λ " ti P N | @j ě i shpv j q ě shpv i qu, where shppq, Ka 1 ¨¨¨a n qq " n `1. Note that Steps Λ is always infinite and hence induces a decomposition of the play Λ into finite pieces.

In the decomposition induced by Steps Λ , a factor v i ¨¨¨v j is called a bump if shpv j q " shpv i q, called a Stair otherwise (that is, if shpv j q " shpv i q `1 and j " i `1).

For any play Λ with Steps Λ " tn 0 ă n 1 ă ¨¨¨u, we can define the sequence pmcol Λ i q iě0 P N N by letting mcol Λ i " mintΩpv k q | n i ď k ď n i`1 u. This sequence fully characterises the parity condition. Proposition 9. For a play Λ, Λ P W par iff lim infppmcol Λ i q iě0 q is even. In the sequel, we build a new parity game r G over a new game graph r G " p r V , r Eq. This new game simulates the abstract pushdown graph, in the sense that the sequence of visited colours during a correct simulation of some play Λ in G abs is exactly the sequence pmcol Λ i q iě0 . Moreover, a play in which a player does not correctly simulate the abstract pushdown game is losing for that player. We will show how the winning region in r G allows us to compute the sets ta P A | R P Rpq, aqu. Before providing a description of the game graph r G, let us consider the following informal description of this simulation game. We aim at simulating a play in the abstract pushdown game from the initial configuration pq 0 , Kq. In r G we keep track of only the control state and the top stack symbol of the simulated configuration.

The interesting case is when the simulated play is in configuration with control state p and top stack symbol a, and the player owning p wants to perform transition pq, a 1 bq, i.e. go to state q, rewrite a into a 1 and push b on top of it. For every strategy of Éloïse, there is a certain set of possible (finite) prolongation of the play (consistent with her strategy) that will end with popping b (or actually a symbol into which b was rewritten in the meantime) from the stack. We require Éloïse to declare a vector Ý Ñ S " pS 0 , . . . , S d q of p`1q subsets of Q, where S i is the set of all states the game can be in after popping (possibly a rewriting of) b along those plays where in addition the smallest visited colour while (possibly a rewriting of) b was on the stack is i.

Abelard has two choices. He can continue the game by pushing b onto the stack and updating the state (we call this a pursue move). Otherwise, he can pick a set S i and a state s P S i , and continue the simulation from that state s (we call this a jump move). If he does a pursue move, then he remembers the vector Ý Ñ S claimed by Éloïse; if later on, a transition of the form ps, εq P Q ˆtεu is simulated, the play goes into a sink state (either tt or ff ) that is winning for Éloïse if and only if the resulting state is in S θ where θ is the smallest colour seen in the current level (this information will be encoded in the control state, reset after each pursue move and updated after each jump move). If Abelard does a jump move to a state s in S i , the currently stored value for θ is updated to minpθ, i, Ωpsqq, which is the smallest colour seen since the current stack level was reached.

There are extra edges to simulate transition of the form pq, a 1 q P Q ˆA where the top stack element and the value of θ are updated.

(q, a ′ , -→ R , min(θ, Ω(q)))

tt ff (p, a, -→ R , θ) (p, a ′ , -→ R , θ, q, b) (p, a ′ , -→ R , θ, q, b, -→ S )
(q, b, -→ S , Ω(q)) (s, a ′ , -→ R , min(θ, i, Ω(s)), i) (s, a ′ , -→ R , min(θ, i, Ω(s)))

If ' The main vertices of r G are those of the form pp, a, Ý Ñ R , θq, where p P Q, a P A, Ý Ñ R " pR 0 , . . . , R d q P p2 Q q d`1 and θ P t0, . . . , du. A vertex pp, a, Ý Ñ R , θq is reached when simulating a partial play Λ in G abs such that:

-The last vertex in Λ is pp, uaq for some u P A ˚.

-Éloïse claims that she has a strategy to continue Λ in such a way that if a (or a rewriting of it) is eventually popped, the control state reached after popping belongs to R i , where i is the smallest colour visited since the stack height was at least |ua|. -The colour θ is the smallest one since the current stack level was reached from a lower stack level. A vertex pp, a, Ý Ñ R , θq is controlled by Éloïse if and only if p P Q E . ' The vertices tt and ff are here to ensure that the vectors Ý Ñ R encoded in the main vertices are correct. Both are sink vertices and are controlled by Abelard. Vertex tt gets colour 0 and vertex ff gets colour 1. As these vertices are sinks, a play reaching tt is won by Éloïse whereas a play reaching ff is won by Abelard. There is a transition from some vertex pp, a, Ý Ñ R , θq to tt, if and only if there exists a transition rule pr, εq P ∆pp, aq, such that r P R θ (this means that Ý Ñ R is correct with respect to this transition rule). Dually, there is a transition from a vertex pp, a, Ý Ñ R , θq to ff if and only if there exists a transition rule pr, εq P ∆pp, aq such that r R R θ (this means that Ý Ñ R is not correct with respect to this transition rule). ' To simulate a transition rule pq, a 1 q P ∆pp, aq, the player that controls pp, a, Ý Ñ R , θq moves to pq, a 1 , Ý Ñ R , minpθ, Ωpqqqq. Note that the last component has to be updated as the smallest colour seen since the current stack level was reached is now minpθ, Ωpqqq.

' The round is of the form pp, a, Ý Ñ R , θqpq, a 1 , Ý Ñ R , θq and corresponds therefore to the simulation of a transition pq, a 1 q. We designate it as a trivial bump.

' The round is of the form pp, a, Ý Ñ R , θqpp, a 1 , Ý Ñ R , θ, q, bqpp, a 1 , Ý Ñ R , θ, q, b, Ý Ñ S q ps, a 1 , Ý Ñ R , minpθ, i, Ωpsqq, iqps, a 1 , Ý Ñ R , minpθ, i, Ωpsqqq and corresponds therefore to the simulation of a transition pq, a 1 bq pushing b followed by a sequence of moves that ends by popping b (or a rewriting of it). Moreover i is the smallest colour encountered while b (or other top stack symbol obtained by successively rewriting it) was on the stack. We designate it as a (non-trivial) bump.

' The round is of the form pp, a, Ý Ñ R , θqpp, a 1 , Ý Ñ R , θ, q, bqpp, a 1 , Ý Ñ R , θ, q, b, Ý Ñ S q pq, b, Ý Ñ S , Ωpqqq and corresponds therefore to the simulation of a transition pq, a 1 bq pushing a symbol b leading to a new stack level which the play will never go below. We designate it as a stair. We define the colour of a round as the smallest colour of the vertices in the round. For any play λ " v 0 v 1 v 2 ¨¨¨in r G, we consider the subset of indices corresponding to vertices of the form pp, a, Ý Ñ R , θq. More precisely:

Rounds λ " tn | v n " pp, a, Ý Ñ R , θq, p P Q, a P A, Ý Ñ R P p2 Q q d`1 , 0 ď θ ď du

The set Rounds λ induces a natural factorisation of λ into rounds. Indeed, let Rounds λ " tn 0 ă n 1 ă n 2 ă ¨¨¨u, then for all 0 ď i ă |Rounds λ | we let λ i " v ni ¨¨¨v ni`1 . We call the sequence pλ i q iě0 the round factorisation of λ. For every i ě 0, λ i is a round and the first vertex in λ i`1 equals the last one in λ i . Moreover, λ " λ 1 d λ 2 d λ 3 d ¨¨¨, where λ i d λ i`1 denotes the concatenation of λ i with λ i`1 without its first vertex.

In order to prove both implications of Theorem 9, we build from a winning strategy for Éloïse in one game a winning strategy for her in the other game. The main argument to prove that the new strategy is winning is to prove a correspondence between the factorisations of plays in both games.

Direct implication.

Assume that the configuration pp in , Kq is winning for Éloïse in G abs , and let Φ be a corresponding winning strategy for her.

Using Φ, we define a strategy ϕ for Éloïse in r G from pp in , K, p∅, . . . , ∅q, Ωpp in qq. The strategy ϕ maintains as a memory a partial play Λ in G abs , that is an element in V åbs (where V abs denotes the set of vertices of G abs ). At the beginning Λ is initialised to the vertex pp in , Kq. We first describe ϕ, and then we explain how Λ is updated. Both the strategy ϕ and the update of Λ, are described for a round. Choice of the move. Assume that the play is in some vertex pp, a, Ý Ñ R , θq for p P Q E . The move given by ϕ depends on ΦpΛq:

' If ΦpΛq " pr, εq, then Éloïse goes to tt (Proposition 10 will prove that this move is always possible). ' If ΦpΛq " pq, a 1 q, then Éloïse goes to pq, a 1 b, Ý Ñ R , minpθ, Ωpqqqq. ' If ΦpΛq " pq, a 1 bq, then Éloïse goes to pp, a 1 , Ý Ñ R , θ, q, bq. In this last case, or in the case where p P Q A and Abelard goes to pp, a 1 , Ý Ñ R , θ, q, bq, we also have to explain how Éloïse behaves from pp, a 1 , Ý Ñ R , θ, q, bq. She has to provide a vector Ý Ñ S P p2 Q q d`1 that describes which states can be reached if b (or its successors by top rewriting) is eventually popped, depending on the smallest visited colour in the meantime. In order to define Ý Ñ S , Éloïse considers the set of all possible continuations of Λ ¨pq, ua 1 bq (where pp, uaq denotes the last vertex of Λ) where she respects her strategy Φ. For each such play, she checks whether some configuration of the form ps, ua 1 q is visited after Λ ¨pq, ua 1 bq, that is if the stack level of b is eventually left. If it is the case, she considers the first configuration ps, ua 1 q appearing after Λ ¨pq, ua 1 bq and the smallest colour i since b and (possibly) its successors by top-rewriting were on the stack. For every i P t0, . . . du, S i , is exactly the set of states s P Q such that the preceding case happens. More formally, S i " ts | D Λ ¨pq, ua 1 bqv 0 ¨¨¨v k ps, ua 1 q ¨¨¨play in G abs where Éloïse respects Φ and s.t. |v j | ą |ua|, @j " 0, . . . , k and minptΩpv j q | j " 0, . . . , ku Y tΩpqquq " iu Finally, we let Ý Ñ S " pS 0 , . . . , S d q and Éloïse moves to pp, a 1 , Ý Ñ R , θ, q, b, Ý Ñ S q. Update of Λ. The memory Λ is updated after each visit to a vertex of the form pp, a, Ý Ñ R , θq. We have three cases depending on the kind of the last round:

  ÝÑ where L w def " e ˚a1 e ˚¨¨¨e ˚an e ˚is the set of words over Σ obtained by inserting arbitrarily many occurrences of e in w.

Figure 2 .

 2 Figure 2. An LTS L with silent transitions of root r (on the left), the tree TreepLq (in the center) and the tree Tree K pLq (on the right).

Example 1 .

 1 Assuming that f : po Ñ oq Ñ o Ñ o, g : o Ñ o and c : o, we have g c : o, f g : o Ñ o, f g c " pf gq c : o and f pf gq c : o.

Figure 3 .

 3 Figure 3. The LTS and the tree associated with the scheme S of Example 2.

Z e ÝÑ f pH aq pF f q a

F

  pF ϕ xq y pH yq y loooooooooooooooooooooooomoooooooooooooooooooooooon s3

  pH zq F pF ϕ xq y pH yq ϕ pH yq Z G pH Xq F G z pH zq F ϕ x F pF ϕ xq y pH yq y looooooooooooooooooooooooooomooooooooooooooooooooooooooon s3

Example 10 .

 10 In the figure below, we illustrate the definition of M on the scheme S U .

  t h with k ą h and ϕ : pτ 1 , . . . , τ m , oq. Thanks to Definition 1, ϕ t 1 . . . t h is of order-1. Property 5 implies that ℓ m is either equal to |s m | or to |s m | `1. Property 6 implies ℓ m ‰ |s m |`1 as otherwise we would have k ď h. Thus, we have ℓ m " |s m | and by Property 4, collapsepsq " pop 2 psq.

Example 14 .

 14 Following the same ideas as for S 1 (see Example 3), the order-2 scheme S exp given below defines the treeT exp " Prefpta n cb 2 n | n ě 0uq.with Z, X : o, B : o Ñ o, D : po Ñ o, o, oq and F : po Ñ o, oq. If we denote by D n B the term of type o Ñ o defined by D 0 B " B and D n`1 B " D pD n Bq for n ě 0, we have Z a n ùñ F D n B. As D intuively doubles its argument, D n B behaves as B 2 n for n ě 0. In particular, D n B X reduces by b 2 n to X.

2 D 1 "

 21 pψ xq with Z, X : o, B : o Ñ o, F : ppo Ñ o, o, oq, oq, D 1 : po Ñ o, o, oq and D 2 : ppo Ñ o, o, oq, o Ñ o, o, oq. If we denote by D n 2 D 1 the term of type po Ñ o, o, oq defined by D 0 2 D 1 " D 1 and D n`1 D 2 D n 2 D 1 for n ě 0, we have Z a n ùñ F D n 2 D 1 . As D 2 intuitively double its argument with each application, D n 2 D 1 behaves as D 2 n 1 and hence D 2 n 1 B behaves as B 2 2 n .

def " rr pop 1

 1 psq :: ϕ ss def " rr Arg rkpϕq ppop 1 psqq ss def " rr r :: t ss Def 4

tMs 1 Ms 1

 11 for a P Σ then the N -stack s 1 such that s ae Ý Ñ is such that rr s 1 ss " t. Conversely if s ae Ý Ñ for some N -stack s 1 then rr s ss a ÝÑ S rr s 1 ss.

s 1 A xx s 1 M s 1 and xx s yy e ÝÑ A xx s 2 yy then xx s 2 yy e Ý Ñ A xx s 1

 111 if and only if xx s yy a ÝÑ A xx s 1 yy. For any V -stack s, if s e ÝÑ M s 1 then xx s yy e Ý Ñ yy as intuitively ÝÑ A combines the definition of both ÝÑ M and Arg k p ¨q.Conversely for all V -stack, if s e ÝÑ yy.

  there is nothing to prove. Otherwise, as t k : o, by Property 6, ℓ m ď |s m |. If ℓ m ă |s m | then all properties are trivially inherited from s. The interesting case is ℓ m " |s m |. In this case, ℓ 1

  t h with k ą h and ϕ : pτ 1 , . . . , τ m , oq. Thanks to Definition 1, ϕ t 1 . . . t h is of order-1. Property 5 implies that ℓ m is either equal to |s m | or to |s m | `1. Property 6 implies ℓ m ‰ |s m | `1 as otherwise we would have k ď h. Thus, we have ℓ m " |s m | and by Property 4, collapsepsq " pop 2 psq.

Figure 5 .

 5 Figure 5. Local structure of r G.

  Let w " w 0 . . . w |w|´1 be a prefix of a well-bracketed word. We have Z w ùñ pr n 1 . . . n ℓ s, |w| `1q where r n 1 . . . n ℓ s is the sequence (in increasing order) of those indices of unmatched opening brackets in w. In turn, pr n 1 . . . n ℓ s, |w| `1q

	pr s, 1q	pr s, nq	‹ ÝÑ 0
	prn 1 . . . n ℓ s, nq	‹ ÝÑ n ℓ	n	`1 ‹ ÝÑ n
	prn 1 . . . n ℓ s, nq

p ÝÑ prn 1 . . . n ℓ ns, n `1q prn 1 . . . n ℓ s, nq q ÝÑ prn 1 . . . n ℓ´1 s, n `1q

  Arg k psq " Arg k´ℓ pcollapsepsqq otherwise.

	Definition 3. For all s :: t P CStacks, we define the value
	of t in the context of s: $ rr s :: t 1 t 2 ss " rr s :: t 1 ssrr s :: t 2 ss & rr s :: A ss " A % rr s :: x ss " rr Arg rkpxq psq ss	if t 1 , t 2 P Γ if A P N if x P V

  Definition 4. The term associated with a well-formed ϕstack s P Stacks with ϕ P N Y V is rr s ss def " rr pop 1 psq :: ϕ ssrr Arg 1 psq ss ¨¨¨rr Arg ̺pϕq psq ss.Equiv., if t op 1 psq : o then: rr s ss " rr pop 1 psq :: t op 1 psq ss. If t op 1 psq : τ 1 Ñ . . . Ñ τ ℓ Ñ o then: rr s ss " rr pop 1 psq :: t op 1 psq ss rr Arg 1 pcollapsepsqq ss ¨¨r r Arg ℓ pcollapsepsqq ss.

	Example 9. Let us consider the well-formed stacks s 2 and
	s 3 presented in Example 8. In the representation below the
	association between variables and their "values" are made
	explicit by the red arrows.

  . . r K Z s . . .s n , Σ, p prq if s is a ϕ-stack with ϕ : τ P V of order k ą 0 and Arg rkpϕq ppop 1 ppush n´k`1 psqqq " r :: t.

	and define the transitions as follows	a ÝÑ q aPΣ y M
	' s A x 1 ¨¨¨x ̺pAq a ÝÑ push t 1 psq if s is an A-stack with A P N and M a ÝÑ t P R,
	' s and Arg rkpϕq ppop 1 psqq " r :: t, e ÝÑ push t 1 prq if s is a ϕ-stack with ϕ : o P V M
	' s	e ÝÑ M	push t,n´k`1 1

  Proposition 1. Tree K pSq " Tree K pMq. Let s be an N -stack in WStacks and a P Σ.For any t P TermspN q, if rr s ss WStacks be a ϕ-stack for ϕ P V and let s 1 P WStacks be a ψ-stack for ψ P V Y N . then rr s ss " rr s 1 ss, ordpϕq ď ordpψq and | t op n´ordpϕq`1 psq | ą | t op n´ordpϕq`1 ps 1 q |. ' For all s P WStacks there exists a unique N -stack s 1 P WStacks such that s e

	Sketch: One easily concludes after establishing the
	following soundness result about the definition of ÝÑ
			a ÝÑ t then Ds 1 P
	WStacks, s If Ds 1 P WStacks, s a ÝÑ s 1 and rr s 1 ss " t. M a ÝÑ M s 1 then rr s ss	a ÝÑ rr s 1 ss.
	If s	e ÝÑ M	s 1

M . ' ' Let s P Ý Ñ M s 1 .

  Proofs Omitted in Section III 1) Justification of Definition 4: . We start with a fact that justifies the second part of Definition-4 Definition 4. The term associated with a well-formed ϕ-stack s P Stacks with ϕ P N Y V is V of type τ 1 Ñ . . . Ñ τ ̺pϕq Ñ o and for all i P r1, ns, t i P Γ of type τ i . Note that ℓ " ̺pϕq ´n. We have:

	rr s ss
	rr s ss

def " rr pop 1 psq :: ϕ ssrr Arg 1 psq ss ¨¨¨rr Arg ̺pϕq psq ss.

Equiv., if t op 1 psq : o then: rr s ss " rr pop 1 psq :: t op 1 psq ss. If t op 1 psq : τ 1 Ñ . . . Ñ τ ℓ Ñ o then: rr s ss " rr pop 1 psq :: t op 1 psq ss rr Arg 1 pcollapsepsqq ss ¨¨r r Arg ℓ pcollapsepsqq ss. Fact 1. Let s be a well-formed ϕ-stack. If t op 1 psq : o then: rr s ss " rr pop 1 psq :: t op 1 psq ss. If t op 1 psq : τ 1 Ñ . . . Ñ τ ℓ Ñ o then: rr s ss " rr pop 1 psq :: t op 1 psq ss rr Arg 1 pcollapsepsqq ss ¨¨¨rr Arg ℓ pcollapsepsqq ss. Proof: The first case (t op 1 psq : o) is immediate. Assume that t op 1 psq is equal to ϕ t 1 ¨¨¨t n with ϕ P N Y def " rr pop 1 psq :: ϕ ssrr Arg 1 psq ss ¨¨¨rr Arg n psq ss loooooooooooooooooooooooooomoooooooooooooooooooooooooon rr pop 1 psq::ϕ t1¨¨¨tn ss rr Arg n`1 psq ss ¨¨¨rr Arg ̺pϕq psq ss " rr pop 1 psq :: t op 1 psq ss rr Arg 1 pcollapsepsqq ss ¨¨¨rr Arg ̺pϕq´n"ℓ pcollapsepsqq ss

5 )

 5 Proof of Proposition 1: . Proposition 1. Tree K pSq " Tree K pMq.Proof: The proof relies on two lemmas. The first lemma states the soundness of the first line of the definition of ÝÑ Let s be an N -stack in WStacks and a P Σ. Let s P WStacks be an A-stack for some A P N and let a P Σ. By definition of rr s ss, rr s ss is equal to A rr Arg 1 psq ss ¨¨¨rr Arg ̺pAq psq ss.Assume that rr s ss there exists a production A x 1 ¨¨¨x ̺pAq a ÝÑ t 1 in R such that t is equal to t 1 rx 1 {rr Arg 1 psq ss, . . . , x ̺pAq {rr Arg ̺pAq psq sss. By definition of push t 1 1 psq hence we only need to note that rr push t 1 1 psq ss is equal to t 1 rx 1 {rr Arg 1 psq ss, . . . , x ̺pAq {rr Arg ̺pAq psq sss. Indeed, as t 1 is of ground type, rr push t 1 1 psq ss is equal to rr s :: t 1 ss which is by definition equal to t 1 rx 1 {rr Arg 1 psq ss, . . . , x ̺pAq {rr Arg ̺pAq psq sss. Now, assume that s R such that s 1 " push t 1 1 psq. As s is an A-stack, we have rr s ss " A rr Arg 1 psq ss . . . rr Arg ̺pAq psq ss. Furthermore rr s 1 ss is equal to t 1 rx 1 {Arg 1 psq, . . . , x ̺pAq {Arg ̺pAq psqs. Hence by definition of

	$ &	Dt P TermspN q, rr s ss
	%	M	s 1	ñ rr s ss

M . Lemma 4. a ÝÑ t ñ Ds 1 P WStacks, s a ÝÑ M s 1 and rr s 1 ss " t Ds 1 P WStacks, s a ÝÑ a ÝÑ rr s 1 ss Proof: a ÝÑ t for some t P TermspN q. By definition of a ÝÑ, a ÝÑ M , we have s a ÝÑ M a ÝÑ M s 1 for some s 1 P WStacks. By definition of a ÝÑ M , there exists a production A x 1 ¨¨¨x ̺pAq a ÝÑ t 1 P a ÝÑ, rr s ss a ÝÑ rr s 1 ss.

  rr Arg i pcollapseps 1 qq ss " rr Arg i pcollapseppush t,n´k`1 Arg i ppop n´k`1 ppop 1 ppush n´k`1 psqqqq ss " rr Arg i psq ss.

		1	prqqq ss
	"	rr Arg i ppop n´k`1 prqq ss
	Lemma 3 "	rr
		Lemma 2

" rr Arg rkpϕq ppop 1 psqq ss " rr pop 1 psq :: ϕ ss

[START_REF] Broadbent | On Collapsible Pushdown Automata, their Graphs and the Power of Links[END_REF]

and for all i P r1, ̺pϕqs,

Note that we therefore slightly generalise our previous definition as we implicitly use an infinite stack alphabet, but this does not introduce any technical change in the definition.

The size of a scheme is defined as the sum of the sizes of the left and right hand sides of the rewriting rules. In particular it is larger than the sum of the sizes of all argument subterms of right hand sides of the rules.

The authors work with the equivalent formalism of the λY -calculus.

to represent applicative terms over N instead of λY -terms.

Note that t does not contain any variables and hence we do not need to worry about capture of variables.

i.e. reachable from the initial configuration

' if h " n there is only one position : the empty tuple ε; ' if h " n ´1 then i P r1, ms; ' if h ă n ´1 then i " ij for some i P r1, ms and j an h-position in s i .

Formally, one could index links as well: whenever performing, in configuration v j , a push γ,e 1 , one attaches to the newly created link the index j `1. Later, if the link is copied (by doing a push k operation) then the index is copied as well.

Recall that the shape of a stack is the stack obtained by replacing all symbols appearing in s by a fresh symbol 7 (but keeping the links).

' The round is a trivial bump and therefore a pq, a 1 q transition was simulated. Let pp, uaq be the last vertex in Λ, then the updated memory is Λ ¨pq, ua 1 q.

Technically speaking, if we impose that a transition of S lf does a r ew 1 (or id) followed by another stack operation, we may not be able to do the update of the stack after doing a pop n . However, we can use the same trick as the one used to define A rk (seeRemark 8).

Acknowledgements: This work was supported by the following projects: AMIS (ANR 2010 JCJC 0203 01 AMIS) and FREC (ANR 2010 BLAN 0202 02 FREC).

' ∆ lf is defined as follows, where q, q 1 range over Q rk , α, β, γ range over Γ rk and Ý Ñ R " pR 0 , . . . , R d q ranges over p2 Q rk q d`1 .

-If pq 1 , r ew α 1 ; opq P ∆ rk pq, γq and if op is neither of the form push β,n 1 nor collapse, then pq 1 , r ew α 1 ; opq P ∆ lf pq, γq and pq 1 , r ew pα, Ý Ñ R q 1 ; opq P ∆ lf pq, pγ, Ý Ñ R qq.

-If pq 1 , r ew α 1 ; push β,n 1 q P ∆ rk pq, γq, then pq β , r ew α 1 ; idq P ∆ lf pq, γq and pq β , r ew pα, Ý Ñ R q

1

; idq P ∆ lf pq, pγ, Ý Ñ R qq.

-For all q β P Q lf , ∆pq β , γq " ∆pq β , pγ, Ý Ñ R qq " tpq ? , push pβ, Ý Ñ S q,1 1 q | Ý Ñ S P p2 Q rk q d`1 qu. -For all q ? P Q lf , ∆pq ? , pγ, Ý Ñ R qq " tpq, idqu Y tpp i , idq | 0 ď i ď d and p P R i u. -For all q i P Q lf , ∆pq i , pγ, Ý Ñ R qq " tpq, pop n qu. -If pq 1 , r ew α 1 ; collapseq P ∆ rk pq, γq, then pq 1 , r ew α 1 ; collapseq P ∆ lf pq, γq. -If pq 1 , r ew α 1 ; collapseq P ∆ rk pq, γq, then ptt, idq P ∆ lf pq, pγ, Ý Ñ R qq if q 1 P R LinkRkpq,γq and pff, idq P ∆ lf pq, pγ, Ý Ñ R qq if q 1 R R LinkRkpq,γq .

-∆ lf ptt, pγ, Ý Ñ R qq " tptt, idqu and ∆ lf pff, pγ, Ý Ñ R qq " tpff, idqu. We let G lf be the transition graph of A lf . Now, in order to define a game graph G lf out of G lf we let Q lf,E " Q rk,E Y tq γ | q P Q rk , γ P Γ rk u. Finally to define a corresponding n-CPDP parity game G lf we extend Ω by letting, @q P Q rk and γ P Γ rk , Ωpq γ q " Ωpq ? q " d (as one cannot loop forever in such states, it means that they have no influence on the parity Ωpq i q " i for every 0 ď i ď d, Ωpttq " 0 and Ωpff q " 1 (hence a play that visits tt is winning for Éloïse and a play that visits ff is winning for Abelard, as these states are sinks).

Note that A lf never create an n-link.

Consider some configuration v 0 " pp 0 , s 0 q in G rk . We explain now how to define an "equivalent" configuration νpv 0 q in G lf (here equivalent is in the sense of Theorem 8). The transformation consists in replacing any occurrence of a stack letter (call it γ) with an n-link in s 0 by another letter of the form pγ, Ý Ñ R q and replace the n-link by a 1-link. The vector Ý Ñ R is defined as follows. Let s 1 be the stack obtained by popping every element and stack above γ, and let R " tq | Éloïse wins in G rk from pq, collapseps 1 qqu. Then one sets Ý Ñ R " pR, ¨¨¨, Rq.

Example 21. Assume we are playing a two-colour parity game and let The rest of this section is devoted to the proof of the following result.

Theorem 8. Éloïse wins in G rk from some configuration v 0 if and only if she wins in G lf from νpv 0 q.

Assume that the configuration v 0 " pp 0 , s 0 q is winning for Éloïse in G rk , and let Φ rk be a winning strategy for her. Using Φ rk , we define a strategy Φ lf for Éloïse in G lf from νpv 0 q. The strategy Φ lf maintains as a memory a partial play Λ rk in G rk , that is an element in V rk (where V rk denotes the set of vertices of G rk ). At the beginning Λ rk is initialised to be pp 0 , s 0 q. The play Λ rk will satisfy the following invariant: assume that the play ends in a configuration pp, sq, then the last configuration in Λ rk has control state p and its t op 1 -element is either t op 1 psq or pt op 1 psq, Ý Ñ R q for some Ý Ñ R (and in this case there is an n-link from the t op 1 -symbol of s).

We first describe Φ lf , and then we explain how Λ rk is updated.

Choice of the move. Assume that the play is in some vertex pp, sq with p P Q lf,E ztq γ | q P Q rk , γ P Γ rk u. The move given by Φ lf depends on Φ rk pΛ rk q " pq, r ew α 1 ; opq (we shall later argue that Φ lf is well defined while proving that it is winning). ' If op is neither of the form push β,n 1 nor collapse then Éloïse plays pq, r ew α 1 ; opq if t op 1 psq " γ and she plays pq, r ew pα,

Ý Ñ R q

1

; opq if t op 1 psq " pγ, Ý Ñ R q. ' If op " collapse and t op 1 psq " γ P Γ rk then Éloïse plays pq, r ew α 1 ; collapseq. ' If op " collapse and t op 1 psq " pγ, Ý Ñ R q then Éloïse plays ptt, idq. We shall later see that this move is always valid.

Recall that Φ rk uses as a memory a partial play Λ lf in G lf and considers the value of Φ lf pΛ lf q to determine the next move to play. Now assume that Φ lf is realised by an n-CPDA transducer S lf synchronised with A lf . Hence, instead of storing Λ lf it suffices to store the configuration S lf is in after reading Λ lf .

One can also notice that the stack s rk in the last configuration of some partial play Λ rk and the stack s lf in the last configuration of the associated Λ lf have the same shapes provided one replaces in s lf every 1-link from a symbol in Γ rk ˆp2 Q rk q d`1 by an n-link. Recall that these 1-links are never used to perform a collapse: hence replacing those 1-links by n-links does not change the issue of the game, and if one does a similar transformation on S lf it still realises a winning strategy, and it is synchronised with the transformed version of Λ lf . Now, it follows from the way one defined Φ rk (both the choice of the move and the memory update) that one can design an n-CPDA transducer S rk synchronised with A rk realising a well-defined winning strategy for Éloïse in G rk from the initial configuration pq 0,rk , K n q. In all cases but one S rk simulates S lf . The only problematic case is when the move to play is some pr, collapseq involving an n-link. Indeed, one needs to backtrack in Λ lf (namely retrieve the configuration of S lf after the link ancestor) and extend it by doing pr ℓ , idq (where ℓ is the link rank) and then pr, pop n q; one needs to retrieve the configuration of S lf right after this. If one performs a collapse in S rk , one directly retrieves the stack content, but the control state of S lf is still missing. However, one can modify S lf so that after the simulation of the creation of an n-link, i.e. after a symbol of the form pγ, Ý Ñ R q in pushed, it stores in its t op 1 -element the control state it will be in after doing the transitions pr ℓ , idqpr, pop n q, for each 0 ď ℓ ď d and each r P R ℓ (this can easily be computed). As this information is then propagated when copying the symbol/link, it is available in the t op 1 -element before doing a collapse involving an n-link, hence S rk can also correctly retrieve the control state of S lf .

From this (somehow informal) description of S rk the reader should be convinced that S rk correctly simulates S lf on Λ lf , hence realises a winning strategy in G rk . The fact that S rk is synchronised with A rk follows from the fact that it is synchronised with the variant of S lf that itself is synchronised with the variant of Λ lf which is synchronised with Λ rk .

Opitmisation. The set Q lf has size Op|Q rk |p|Γ rk | `dqq, which is not very satisfactory for complexity reasons. Actually, one would prefer a variant of the construction where |Γ rk | does not appear in the blowup concerning states. This factor actually comes from states tq γ | q P Q rk , γ P Γ rk u, and one can easily get read of them by doing the following modification of A lf . When simulating a push β,n 1 , instead of going to q β , one stores β (thanks to a r ew 1 operation) in the t op 1 element of the stack (hence the stack alphabet gets augmented by a linear factor in |Γ rk |) and goes to a special state q ! . State q ! is controlled by Éloïse and the transition function is the same as from q β where β is the symbol stored on the t op 1 -element of the stack.

It is straightforward that this modification does not change the validity of the previous statements.

If we summarise, the overall blowup in the transformation from G rk to G lf given by Theorem 7 is as follows.

Proposition 8. Let A rk and A lf be as in Theorem 7. Then the set of states of A lf has size Op|Q rk |dq and the stack alphabet of A lf has size Op|Γ rk | 2 ¨2|Q rk |pd`1q q.

Finally the set of colours used in G rk and G lf are the same.

Proof: By construction together with the optimisation below.

7)

Reducing the Order: .

In the previous section we have constructed from a game played on a rank-aware n-CPDP another game played on an n-CPDP that does not create n-links. The winning regions (resp. winning strategies realised by n-CPDA transducer) in the original game can then be recover from the winning regions (resp. winning strategies realised by n-CPDA transducer) in the latter game.

In this section, we prove a result in a similar flavour. Namely, starting from a game played on an n-CPDP that does not create n-links, we construct a game played on an pn ´1q-CPDP, and we show that the winning regions(resp. winning strategies realised by n-CPDA transducer) in the original game can be recover from the winning regions (resp. winning strategies realised by pn ´1q-CPDA transducer) in the latter game.

We situate the techniques developed here in a general and abstract framework of (order-1) pushdown automata whose stack alphabet is a possibly infinite set: abstract pushdown automata. We start by introducing this concept and show how n-CPDP that does not create n-links fit into it. Then, we introduce the notion of conditional games. Finally, we show how such games can be solved by reduction to a pn ´1q-CPDP parity game, and from the proof we also get the expect result on the existence of strategies realised by CPDA transducers.

We situate the techniques developed here in a general and abstract framework of (order-1) pushdown automata whose stack alphabet is a possibly infinite set.

' To simulate a transition rule pq, a 1 bq P ∆pp, aq, the player that controls pp, a, Ý Ñ R , θq moves to pp, a 1 , Ý Ñ R , θ, q, bq. This vertex is controlled by Éloïse who has to give a vector Ý Ñ S " pS 0 , . . . , S d q P p2 Q q d`1 that describes the control states that can be reached if b (or a symbol that rewrites it later) is eventually popped. To describe this vector, she goes to the corresponding vertex pp,

S q is controlled by Abelard who chooses either to simulate a bump or a stair. In the first case, he additionally has to pick the minimal colour of the bump. To simulate a bump with minimal colour i, he goes to a vertex ps, a 1 , Ý Ñ R , minpθ, i, Ωpsqqq, for some s P S i , through an intermediate vertex ps, a 1 , Ý Ñ R , minpθ, i, Ωpsqq, iq coloured by i. To simulate a stair, Abelard goes to the vertex pq, b, Ý Ñ S , Ωpqqq. The last component of the vertex (that stores the smallest colour seen since the currently simulated stack level was reached) has to be updated in all those cases. After simulating a bump of minimal colour i, the minimal colour is minpθ, i, Ωpsqq. After simulating a stair, this colour has to be initialised (since a new stack level is simulated). Its value, is therefore Ωpqq, which is the unique colour since the (new) stack level was reached.

The vertices of the form pp, a, Ý Ñ R , θq get colours Ωppq. Intermediate vertices of the form pp, a 1 , Ý Ñ R , θ, q, bq or pp, a 1 , Ý Ñ R , θ, q, b, Ý Ñ S q get colours d. The following theorem relates the winning region in r G with G abs and the conditional games induced over G abs .

Theorem 9. The following holds. 1) A configuration pp in , Kq is winning for Éloïse in G abs if and only if pp in , K, p∅, . . . , ∅q, Ωpp in qq is winning for Éloïse in r G. 2) For every q P Q, a P A and R Ď Q, R P Rpq, aq if and only if pq, a, pR, . . . , Rq, Ωpqqq is winning for Éloïse in r G.

The rest of the section is devoted to the proof of Theorem 9. We mainly focus on the proof of the first item, the proof of the second one being a subpart of it. We start by introducing some useful concept and then prove both implications.

To help readability, we will use upper-case letters, e.g. Λ or Φ, to denote objects (plays, strategies. . . ) in G abs , and lower-case letters, e.g. λ or ϕ, to denote objects in r G. Recall that for an infinite play Λ " v 0 v 1 ¨¨¨in G abs Steps Λ denote the set of indices of positions where no configuration of strictly smaller stack height is visited later in the play. More formally, Steps Λ " ti P N | @j ě i shpv j q ě shpv i qu, where shppq, Ka 1 ¨¨¨a n qq " n `1. Note that Steps Λ is always infinite and hence induces a factorisation of the play Λ into finite pieces. Recall that for any play Λ with Steps Λ " tn 0 ă n 1 ă ¨¨¨u, we define the sequence pmcol Λ i q iě0 P N N by letting mcol Λ i " mintΩpv k q | n i ď k ď n i`1 u. Indeed, for any play Λ with Steps Λ " tn 0 ă n 1 ă ¨¨¨u, one can define the sequence pΛ i q iě0 by letting Λ i " v ni ¨¨¨v ni`1 . Note that each of the Λ i is either a bump or a stair. In the later we designate pΛ i q iě0 as the rounds factorisation of Λ.

For any play λ in r G, a round is a factor between two visits through vertices of the form pp, a, Ý Ñ R , θq. We have the following possible forms for a round.

' The round is a bump, and therefore a bump of colour i (where i is the colour of the round) starting with some transition pq, a 1 bq and ending in a state s P S i was simulated. Let pp, uaq be the last vertex in Λ. Then the memory becomes Λ extended by pq, ua 1 bq followed by a sequence of moves, where Éloïse respects Φ, that ends by popping b and reach ps, ua 1 q while having i as smallest colour. By definition of S i such a sequence of moves always exists. ' The round is a stair and therefore we have simulated a pq, a 1 bq transition. If pp, uaq denotes the last vertex in Λ, then the updated memory is Λ ¨pq, ua 1 bq. Therefore, with any partial play λ in r G in which Éloïse respects her strategy ϕ, is associated a partial play Λ in G abs . An immediate induction shows that Éloïse respects Φ in Λ. The same arguments works for an infinite play λ, and the corresponding play Λ is therefore infinite, starts from pp in , Kq and Éloïse respects Φ in that play. Therefore it is a winning play.

The following proposition is a direct consequence of how ϕ was defined.

Proposition 10. Let λ be a partial play in r G that starts from pp in , K, p∅, . . . , ∅q, Ωpp in qq, ends in a vertex of the form pp, a, Ý Ñ R , θq, and where Éloïse respects ϕ. Let Λ be the play associated with λ built by the strategy ϕ. Then the following holds:

1) Λ ends in a vertex of the form pp, uaq for some u P A ˚.

2) θ is the smallest visited colour in Λ since a (or a symbol that was later rewritten as a) has been pushed.

3) Assume that Λ is extended, that Éloïse keeps respecting Φ and that the next move after pp, uaq is to some vertex pr, uq.

Then r P R θ .

Proposition 10 implies that the strategy ϕ is well defined when it provides a move to tt. Moreover, one can deduce that, if Éloïse respects ϕ, ff is never reached.

For plays that never reach the sink state tt, using the definitions of r G and ϕ, we easily deduce the following proposition.

Proposition 11. Let λ be a play in r G that starts from pp in , K, p∅, . . . , ∅q, Ωpp in qq, and where Éloïse respects ϕ. Assume that λ never visit tt, let Λ be the associated play built by the strategy ϕ, and let pΛ i q iě0 be its rounds factorisation. Let pλ i q iě0 be the rounds factorisation of λ. Then, for every i ě 1 the following hold:

1) λ i is a bump if and only if Λ i is a bump 2) λ i has colour mcol Λ i . Now consider a play λ in r G starting from pp in , K, p∅, . . . , ∅q, Ωpp in qq where Éloïse respects ϕ. Either the λ loops in tt (hence is won by Éloïse). Or, thanks to Proposition 11 the sequence of visited colours in λ is pmcol Λ i q iě0 for the corresponding play Λ in G abs . Hence, using Proposition 9 we conclude that λ is winning if and only if Λ is winning; as Λ is winning for Éloïse, it follows that λ is also winning for her.

Converse implication.

First note that in order to prove the converse implication one could follow the direct implication and consider the point of view of Abelard. Nevertheless the proof we give here starts from a winning strategy for Éloïse in r G and deduces a strategy for her in G abs : this induces a more involved proof but has the advantage to lead to an effective construction of a winning strategy for Éloïse in G abs if one has an effective strategy for her in r G. Assume now that Éloïse has a winning strategy ϕ in r G from pp in , K, p∅, . . . , ∅q, Ωpp in qq. Using ϕ, we build a strategy Φ for Éloïse in G abs for plays starting from pp in , Kq.

The strategy Φ maintains as a memory a partial play λ in r G, that is an element in r V ˚. At the beginning λ is initialised to pp in , K, p∅, . . . , ∅q, Ωpp in qq For any play Λ where Éloïse respects Φ the following will hold.

' λ is a play in r G that starts from pp in , K, p∅, . . . , ∅q, Ωpp in qq and where Éloïse respects her winning strategy ϕ. ' The last vertex of λ is some pp, a, Ý Ñ R , θq if and only if the current configuration in Λ is of the form pp, uaq. ' If Éloïse keeps respecting Φ, and if a (or a symbol that rewrite it later) is eventually popped the configuration reached will be of the form pr, uq for some r P R i , where i is the smallest visited colour since a (or some symbol that was later rewritten as a) was on the stack. Note that initially the previous invariants trivially hold. In order to describe Φ, we assume that we are in some configuration pp, uaq and that the last vertex of λ is some pp, a, Ý Ñ R , θq. We first describe how Éloïse plays if p P Q E , and then we explain how Ď is updated. Choice of the move. Assume that p P Q E . Then the move given by Φ depends on ϕpλq.

' If ϕpλq " pq, a 1 , Ý Ñ R , minpθ, Ωpqqqq, Éloïse plays transition pq, a 1 q. ' If ϕpλq " pp, a 1 , Ý Ñ R , θ, q, bq, then Éloïse applies plays transition pq, a 1 bq. ' If ϕpλq " tt, Éloïse plays transition pr, εq for some state r P R θ . Lemma 6 will prove that such an r always exists. Update of λ. The memory λ is updated after each move (played by any of the two players). We have several cases depending on the last transition.

' If the last move was from pp, uaq to pq, ua 1 q then the updated memory is λ ¨pq, a 1 , Ý Ñ R , minpθ, Ωpqqqq. ' If the last move was from pp, uaq to pq, ua 1 bq, let pp, a 1 , Ý Ñ R , θ, q, b, Ý Ñ S q " ϕpλ¨pp, a 1 , Ý Ñ R , θ, q, bqq. Intuitively, Ý Ñ S describes which states Éloïse can force a play to reach if b is eventually popped. Then the updated memory is λ¨pp, a 1 , Ý Ñ R , θ, q, bqp p, a 1 , Ý Ñ R , θ, q, b, Ý Ñ S q ¨pq, b, Ý Ñ S , Ωpqqq. ' If the last move was from pp, uaq to pr, uq the update of λ is as follows. One backtrack in λ until one finds a configuration of the form pp 1 , a 1 , Ý Ñ R 1 , θ 1 , p 2 , a 2 , Ý Ñ R q that is not immediately followed by a vertex of the form ps, a 2 , Ý Ñ R , θ 2 , iq. This configuration is therefore in the stair that simulates the pushing of a 2 onto the stack (here if a 2 ‰ a then a 2 was later rewritten as a). Call λ 1 the prefix of λ ending in this configuration. The updated memory is

Formally, write λ " λ 1 d λ 2 d ¨¨¨d λ k where pλ i q 1ďiďk is the round factorisation of λ. Let h ď k be the largest integer such that λ h is a stair and let

h . The following lemma gives the meaning of the information stored in Ď. Lemma 6. Let Λ be a partial play in G abs , where Éloïse respects Φ, that starts from pp in , Kq and that ends in a configuration pp, uaq. We have the following facts:

1) The last vertex of λ is pp, a, Ý Ñ R , θq with Ý Ñ R P p2 Q q d`1 and 0 ď θ ď d.

2) λ is a partial play in r

G that starts from pp in , K, p∅, . . . , ∅q, Ωpp in qq, that ends with pp, a, Ý Ñ R , θq and where Éloïse respects ϕ.

3) θ is the smallest colour visited since a (or some symbol that was later rewritten as a) was pushed. 4) If Λ is extended by some move that pops a, the configuration pr, uq that is reached is such that r P R θ .

Proof: The proof goes by induction on Λ. We first show that the last point is a consequence of the second and third points. Assume that the next move after pp, uaq is to play a transition pr, εq P ∆pp, aq. The second point implies that pp, a, Ý Ñ R , θq is winning for Éloïse in r G. If p P Q E , by definition of Φ, there is some edge from that vertex to tt, which means that r P R θ and allows us to conclude. If p P Q A , note that there is no edge from pp, a, Ý Ñ R , θq (winning position for Éloïse) to the losing vertex ff . Hence we conclude the same way.

Let us now prove the other points. For this, assume that the result is proved for some play Λ, and let Λ 1 be an extension of Λ. We have two cases, depending on how Λ 1 extends Λ: ' Λ 1 is obtained by applying a transition of the form pq, a 1 q or pq, a 1 bq. The result is trivial in that case. ' Λ 1 is obtained by applying a transition of the form pr, εq. Let pp, uaq be the last configuration in Λ, and let Ý Ñ R be the last vector component in the last vertex of λ when in configuration pp, uaq. By the induction hypothesis, it follows that Λ 1 " Λ ¨pr, uq with r P R θ . Considering how λ is updated, and using the fourth point, we easily deduce that the new memory λ is as desired.

Actually, we easily deduce a more precise result. Lemma 7. Let Λ be a partial play in G abs starting from pp in , Kq and where Éloïse respects Φ and let pΛ i q iě0 be its rounds factorisation. Let pλ i q i"0,...,k be the rounds factorisation of λ. Then the following holds:

Both lemmas 6 and 7 are for partial plays. A version for infinite plays would allow us to conclude. Let Λ be an infinite play in G abs . We define an infinite version of λ by considering the limit of the pλ i qq iě0 where λ i is the memory after the i first moves in Λ. See Footnote 11 on page 36 for a similar construction. It is easily seen that such a limit always exists, is infinite and corresponds to a play won by Éloïse in r G. Moreover the results of Lemma 7 apply. Let Λ be a play in G abs with initial vertex pp in , Kq, and where Éloïse respects Φ, and let λ be the associated infinite play in r G. Therefore λ is won by Éloïse. Using Lemma 7 and Proposition 9, we conclude, as in the direct implication that Λ is winning.

Main Result.

Theorem 10. For any n-CPDP A lf " xΓ lf , Q lf , ∆ lf , q 0,lf y that does not create n-links and any associated parity game G lf , one can construct an pn ´1q-CPDP r A " x r Γ, r Q, r ∆, r q 0 y and an associated parity game r G such that the following holds.

' pq 0,lf , K n q is winning for Éloïse in G lf if and only if p r q 0 , K n´1 q is winning for Éloïse in r G . ' If there is an pn ´1q-CPDA transducer r S synchronised with r A realising a well-defined winning strategy for Éloïse in r G from p r q 0 , K n´1 q, then one can effectively construct an n-CPDA transducer S lf synchronised with A lf realising a well-defined winning strategy for Éloïse in G lf from the initial configuration pq 0,lf , K n q.

Proof: Following Example 23, A lf can be seen as an abstract pushdown automaton. In particular, we can apply the construction of Section D7. We claim that the resulting game r G is associated with an pn ´1q-CPDP. Indeed, one simply needs to consider how the graph r G is defined and make the following observations concerning the local structure given in Figure 5 when G is played on the transition graph of an n-CPDP that does not create links.

1) For every vertex of the form pp, a, Ý Ñ R , θq, pp, a, Ý Ñ R , θ, q, bq, pp, a, Ý Ñ R , θ, q, b, Ý Ñ S q or ps, a, R, θ 1 , iq, a and b are pn ´1qstack.

2) For every vertex of the form pp, a, Ý Ñ R , θ, q, bq or pp, a, Ý Ñ R , θ, q, b, Ý Ñ S q, one has a " b. This implies that any vertex in r G can be seen as a pair formed by a state in a finite set and an pn ´1q-stack. Then one concludes the proof by checking that the edge relation is the one of an pn ´1q-CPDP (for the transition to vertices tt and ff one introduces vertices ptt, aq and pff, aq for any pn ´1q-stack a).

Therefore, the first point follows by Theorem 9.

We now turn to the last point and therefore assume that there is an pn ´1q-CPDA transducer r S synchronised with r A realising a well-defined winning strategy ϕ for Éloïse in r G from p r q 0 , K n´1 q. We argue that the strategy Φ constructed in the proof of Theorem 9 can be realised, when G abs is obtained from an n-CPDP A lf that does not create n-links, by an n-CPDA transducer S lf synchronised with A lf .

For this, let us first have a closer look at Φ. The key ingredient in Φ is the play λ in r G, and the value of Φ uniquely depends on ϕpλq. In particular, if ϕ is realised by an pn ´1q-CPDA transducer r S, it suffices to know the configuration of r S after reading λ in order to define Φ. We claim that it can be computed by an n-CPDA transducer S lf (synchronised with A lf ); the hard part being to establish that such a device can update correctly its memory.

Let λ " v 0 v 1 ¨¨¨v ℓ and let r λ " pp 0 , s 0 qpp 1 , s 1 q ¨¨¨pp ℓ , s ℓ q be the run of S associated with λ, i.e. after having played v 0 ¨¨¨v k , S is in configuration pp k , s k q. Denote by Lastpr λ q the last configuration of r λ , i.e. pp ℓ , s ℓ q. To define Φ, Lastpr λ q suffices but of course, in order to update Lastpr λ q, we need to recall some more configurations from r λ . In the case where the last transition applies an order-k stack operation with k ă n (i.e. it is neither pop n nor push n ), then the update is simple, as it consists in simulating one step of S. If the last stack operation is push n then the update of λ consists in adding three vertices and the corresponding update of r λ is simple (as the only operation on the pn ´1q-stack is to rewrite the t op 1 -element). If the last stack operation is pop n one needs to backtrack in λ (hence in r λ ): the backtrack is to some

Once v k has been found, the update is fairly simple for both λ and r λ (one simply extends the remaining prefix of λ by two extra vertices whose stack content is unchanged compared with the one in v k ).

Define the following set of indices where λ

Note that after a partial play Λ the cardinality of Extpλq is equal to the height of the stack in the last configuration of Λ.

For any partial play Λ in G lf define the following n-stack (note that it does not contain any n-link)

M empΛq " [s 1 k1 s 1 k2 ¨¨¨s 1 k h ] where we let ' Extpλq " tk 1 ă ¨¨¨k h u, λ being the memory associated with Λ as in the proof of Theorem 9 ' s 1 j is the pn ´1q-stack obtained from s j (recall that pp j , s j q denotes the j-th configuration of r λ ) by appending p j to its t op 1 -symbol (i.e. we work on an enriched stack alphabet). Note that Lastpr λ q is essentially t op 1 pM empΛqq as the only difference is that now the control state is stored in the stack. Moreover M empΛq can easily be updated by an n-CPDA transducer: for the case of a transition involving an order-k stack operation with k ă n one simulates S on t op 1 pM empΛqq; for the case of a transition involving a push n one first simulates S on t op 1 pM empΛqq (as one may do a r ew 1 before push n ) and then makes a push n to duplicate the topmost pn ´1q-stack in M empΛq; finally, for the case of a pop n , one simply needs to do a pop n in M empΛq to backtrack and then update the control state. This is how we define S lf 12 . The fact that S lf is synchronised with A lf comes from the definition of how S lf behaves when the transition in A lf involves a pop n or a push n , and for the other cases it follows from the initial assumption of S being synchronised with r A.

If we summarise, the overall blowup in the transformation from G lf to r G given by Theorem 10 is as follows.

Proposition 12. Let A lf and r A be as in Theorem 10. Then the set of states of r A has size Op2 2pd`1q|Q lf | q and the stack alphabet of r A has size Op|Γ lf |q. Finally the set of colours used in G lf and r G are the same.

Proof: By construction.

8) Proof of Theorem 5: . The proof of Theorem 5 consists in combining theorems 6, 7 and 10. Indeed, starting from an n-CPDP, by pn ´1q successive applications of this three results, we obtain a 1-CPDP parity game. If we apply to this latter (pushdown) game the construction of Section D7 we end up with a game on a finite graph. Solving this game and following the chain of equivalences provided by theorems 6, 7 and 10 concludes the proof.

Concerning complexity, one step of successive application of the construction in theorems 6, 7 and 10 results in an pn ´1q-CPDP with stack alphabet of size Op|Γ| 2 ¨2|Q|pd`1q n`5 q and state set of size Op2 |Q|pd`1q n`5 q (complexity follows from propositions 5, 8 and 12.

If one let exp k be the function defined by exp 0 pxq " x for all x and exp k`1 pxq " 2 exp k pxq , we conclude that the 1-CPDP obtained after pn ´1q successive applications of the three reductions has a stack alphabet of size Op|Γ| 2pn´1q ëxp n´1 p|Q|pd `1q n`5 qq and state set of size Opexp n´1 p|Q|pd `1q n`5 qq. Finally the finite game we obtain is a parity game with pd `1q colours on a graph with Op|Γ| 4pn´1q exp n p|Q|pd `1q n`6 qq vertices. This latter game can be solve in Opr|Γ| 4pn´1q exp n p|Q|pd `1q n`6 qs d q

In particular the overall complexity of deciding the winner in an n-CPDP parity game is:

' n-times exponential in the number of states of the CPDP; ' pn `1q-times exponential in the number of colours; ' polynomial in the stack alphabet of the CPDP.

Hardness already holds when one considers reachability condition (i.e. does the play visit a configuration with a final control state?) for games generated by higher-order pushdown automata (i.e. CPDP that never use collapse). A self content proof of this result was established by Thierry Cachat and Igor Walukiewicz, but was unfortunately not published [A1].

E. Proofs Omitted in Section V 1) Proof of Theorem 3: . Theorem 3. Labeled recursion schemes as well as CPDA have the effective MSO selection property.

Proof: Let ϕpX 1 , ¨¨¨, X ℓ q be a monadic second order formula with ℓ second-order free variables, and let S " x Σ, N, R, Z, K y be a labelled recursion scheme.

Relying on Theorem 1, we consider a CPDA A such that Tree K pSq " Tree K pAq. Let t ϕ be a term over the ranked alphabet Σ ˆt0, 1u ℓ . We say that t ϕ is a marking of a term t over the ranked alphabet Σ iff t is obtained from t ϕ by forgetting the t0, 1u ℓ component. Formally, if we let π denotes the natural projection from Σ ˆt0, 1u ℓ into Σ, we require that t " tπpu ϕ q | u ϕ P t ϕ u and that for all u ϕ , v ϕ P t ϕ , πpu ϕ q " πpv ϕ q ñ u ϕ " v ϕ (i.e. π is injective on t ϕ ).

Let t ϕ be a marking of a tree t. Then we define for any 1 ď i ď ℓ the set U i " tπpu ϕ q | u ϕ ends by some pa u , b u,1 , . . . , b u,ℓ q with b u,i " 1u of nodes in t which are the image by π of a node whose i-th component is 1.

Thanks to the well-known equivalence between logic and tree automata, there is a nondeterministic parity tree automaton B ϕ working on Σ ˆt0, 1u ℓ trees such that a tree t ϕ is accepted by B ϕ iff t ϕ is the marking of a tree t such that ϕpX 1 Ð U 1 , . . . X ℓ Ð U ℓ q holds in t.

Recall that acceptance of a tree by a nondeterministic parity tree automaton can be seen as existence of a winning strategy in a parity game that is (informally) played as follows. The two players, Éloïse and Abelard move down the tree a pebble to which is attached a state of the automaton; the play starts at the root (with initial state attached to the pebble); at each round Éloïse provides a valid transition (w.r.t the current state and the current node label) of the automaton and Abelard moves the pebble to some son and update the state attached to the pebble according to the transition chosen by Éloïse. In case the pebble reach a leaf, the play ends and Éloïse wins iff the state is final (we have final states in the tree automaton to handle finite branches); otherwise the play is infinite and Éloïse wins iff the smallest infinitely visited priority is even.

For some t ϕ , the previous acceptance game is easily seen to be a collapsible pushdown games. The underlying arena is essentially a synchronised product of the transition graph of a collapsible pushdown process with the finite graph corresponding to B ϕ . Now consider a variant of this game where instead of checking whether a given t ϕ is accepted by B ϕ the players wants to check, for a given tree t, whether there exists some t ϕ such that t ϕ is accepted by B ϕ and t ϕ is a marking of t. The game is essentially the same, except that now Éloïse is also giving the marking of the current vertex (i.e. π ´1). Again, this leads to a collapsible pushdown game and one directly checks that Éloïse wins from the root iff there is a marking of t that is accepted by B ϕ . Call G this game and call A 1 the underlying CPDP.

Apply Theorem 5 to G. Then either Éloïse has no winning strategy from the initial configuration (call it pq 0 , r. . . r K s 1 . . .s n q) and we are done (there is no selector). Otherwise one can effectively construct an n-CPDA transducer T synchronised with A 1 realising a well-defined winning strategy for Éloïse in G from pq 0 , r. . . r K s 1 . . .s n q. As A 1 and T are synchronised, we can consider their synchronised product, call it A 2 . Hence in A 2 the configurations contain extra informations (coming from T ); in particular, for any configuration, if the control state from the A 1 component is controlled by Éloïse, then the control state from the T component provides the next move Éloïse should play: in particular, it provides a transition of the tree automaton, together with information regarding the marking. Transform A 2 by removing every transition that is not consistent with the strategy described by T : then the tree generated by this new CPDA is isomorphic to some t ϕ (that is a marking of t) together with an accepting run of B ϕ on it. Now if we forget the component from B ϕ we obtain a CPDA A ϕ that generates a marking t ϕ of t.

Finally, as we can transform A ϕ back to a labeled recursion scheme, we get S ϕ as expected.

The proof for CPDA follows the same line, except that one directly work on CPDP games.

2) Proof of Corollary 3: . Corollary 3. The µ-calculus model-checking of trees generated by recursion schemes is polynomial under the assumption that the arity of types and the formula are bounded above by a constant.

Proof: The µ-calculus model-checking of trees generated by recursion schemes reduces to solving CPDP parity games. If the arity of types and the formula are bounded above by a constant, the number of states in the CPDP generating the arena as well as the number of colours in the game are bounded as well (see Theorem 1). Then, thanks to the complexity analysis (see section D8) of Theorem 5, we easily conclude.

APPENDIX BIBLIOGRAPHY

[A1] T. Cachat and I. Walukiewicz. The complexity of games on higher order pushdown automata. CoRR, abs/0705.0262, 2007.