M Hague

A S Murawski

C.-H L Ong

O Serre

Collapsible Pushdown Automata and Recursion Schemes

Keywords: Higher-order (collapsible) pushdown automata, higher-order recursion schemes, ranked and ordered trees, solution of parity games over configuration graphs

Collapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addition to the higher-order stack operations push i and pop i , CPDA have an important operation called collapse, whose effect is to "collapse" a stack s to the prefix as indicated by the link from the top 1 -symbol of s. Our first result is that CPDA are equi-expressive with recursion schemes as generators of node-labelled ranked trees. In one direction, we give a simple algorithm that transforms an order-n CPDA to an order-n recursion scheme that generates the same tree, uniformly for all n ≥ 0. In the other direction, using ideas from game semantics, we give an effective transformation of order-n recursion schemes (not assumed to be homogeneously typed, and hence not necessarily safe) to order-n CPDA that compute traversals over a certain finite graph determined by the scheme, and hence paths in the tree generated by the scheme. Our equi-expressivity result is the first such automata-theoretic characterization of (general) recursion schemes.

An important consequence of the equi-expressivity result is that it allows us to translate decision problems on trees generated by recursion schemes to equivalent problems on CPDA and vice versa. For example, since the Modal Mu-Calculus Model-Checking Problem for trees generated by order-n recursion schemes is n-EXPTIME complete, we show that it follows that the same decidability result holds for the problem of solving a parity game played on an order-n collapsible pushdown graph i.e. the configuration graph of a corresponding (order-n) collapsible pushdown system; the latter subsumes several well-known results about the solvability of games over (higher-order) pushdown graphs by (respectively) Walukiewicz, Cachat, and Knapik et al. Moreover our approach yields techniques that are radically different from standard methods for solving model-checking problems on infinite graphs generated by finite machines. This transfer of techniques goes both ways. Another innovation of our work is a self-contained proof of the solvability of parity games on collapsible pushdown graphs by generalizing standard techniques in the field. By appealing to our equi-expressivity result, we obtain a new proof of the decidability (and optimal complexity) of the Modal Mu-Calculus Model-Checking Problem of trees generated by recursion schemes.

In contrast to higher-order pushdown graphs, we show that Monadic Second-Order (MSO) theories of collapsible pushdown graphs are undecidable. Hence collapsible pushdown graphs are, to our knowledge, the first example of a natural class of finitely-presentable graphs that have undecidable MSO theories while enjoying decidable modal mu-calculus theories.

Introduction

Higher-order pushdown automata (PDA) were first introduced by Maslov [17, 18] as accepting devices for word languages. As n varies over the natural numbers, the languages accepted by order-n pushdown automata form an infinite hierarchy. In op. cit. Maslov gave an equivalent definition of the hierarchy in terms of higherorder indexed grammars. Yet another characterization of Maslow's hierarchy was given by Damm and Goerdt [8, 9]: they studied higher-order recursion schemes that satisfy the constraint of derived types, and showed that the word languages generated by order-n such schemes coincide with those accepted by order-n PDA. Maslow's hierarchy offers an attractive classification of the semi-decidable languages: orders 0, 1 and 2 are respectively the regular, context-free and indexed languages, though little is known about languages at higher orders.

Higher-order PDA as a generating device for (possibly infinite) labelled ranked trees was first studied by Knapik, Niwiński and Urzyczyn [15]. As in the case of word languages, an infinite hierarchy of trees is defined, according to the order of the generating PDA; lower orders of the hierarchy are well-known classes of trees: orders 0, 1 and 2 are respectively the regular [22], algebraic [7] and hyperalgebraic trees [14]. Knapik et al. considered another method of generating such trees, namely, by higher-order (deterministic) recursion schemes that satisfy the constraint of safety. A major result in that work is the equi-expressivity of the two methods as tree generators. Open since the early 1980s, a question of fundamental importance in higher-type recursion is to find the class of automata that characterizes the expressivity of higher-order recursion schemes [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] . The results of Damm and Goerdt, and of Knapik et al. may be viewed as attempts to answer the question; they have both had to impose syntactic constraints (of derived types and safety respectively [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] , which seem awkward and rather unnatural) on recursion schemes in order to establish their results. An exact correspondence with (general) recursion schemes has never been proved before.

A partial answer was recently obtained by Knapik, Niwiński, Urzyczyn and Walukiewicz. In an ICALP'05 paper [16], they proved that order-2 homogeneously-typed (but not necessarily safe) recursion schemes are equi-expressive with a variant class of order-2 pushdown automata called panic automata. In this paper, we give a complete answer to the question. We introduce a new kind of higher-order pushdown automata (which generalizes pushdown automata with links [2], or equivalently panic automata, to all finite orders), called collapsible pushdown automata (CPDA), in which every symbol in the stack has a link to a (necessarily lowerordered) stack situated somewhere below it. In addition to the higher-order stack operations push i and pop i , CPDA have an important operation called collapse, whose effect is to "collapse" a stack s to the prefix as indicated by the link from the top 1 -symbol of s. The main result of this paper (Theorem 5 and Theorem 9) is that for every n ≥ 0, order-n recursion schemes and order-n CPDA are equi-expressive as generators of trees.

Our equi-expressivity result has a number of far-reaching consequences. It allows us to translate decision problems on trees generated by recursion schemes to equivalent problems on CPDA and vice versa. Chief among them is the Modal Mu-Calculus Model-Checking Problem (equivalently Alternating Parity Tree Automaton Acceptance Problem, or equivalently Monadic Second-Order (MSO) Model-Checking Problem). We observe that all these problems reduce to the problem of solving a parity game played on a collapsible pushdown graph i.e. the configuration graph of a corresponding collapsible pushdown system (CPDS). Recently one of us has shown [20] that the above decision problems for trees generated by order-n recursion schemes are n-EXPTIME complete. Thanks to our Equi-Expressivity Theorems, it follows that the same (n-EXPTIME complete) decidability result holds for the corresponding CPDS problems, which subsumes many known results [26, 3, 16]. Moreover our approach yields techniques that are radically different from standard methods for solving model-checking problems on infinite graphs generated by finite machines. We stress that this transfer of techniques goes both ways. Indeed another innovation of our work is a self-contained (and without recourse to game semantics) proof of the solvability of parity games on collapsible pushdown graphs by generalizing standard techniques in the field. By appealing to our Equi-Expressivity Theorems, we obtain new proofs for the decidability (and optimal complexity) of model-checking problems of trees generated by recursion schemes as studied in [20].

In contrast to higher-order pushdown graphs (which do have decidable MSO theories [5]), we show that MSO theories of collapsible pushdown graphs are undecidable. Hence collapsible pushdown graphs are, to our knowledge, the first example of a natural class of finitely-presentable graphs that have undecidable MSO theories while enjoying decidable modal mu-calculus theories.

Collapsible pushdown automata (CPDA)

We first introduce (higher-order) collapsible pushdown automata, assuming that the reader is familiar with the notion of higher-order pushdown automata as presented by Knapik et al. in their FOSSACS 2002 paper [15]. An order-n CPDA, or n-CPDA for short, is just an order-n pushdown automata (PDA) in which every non-⊥ symbol in the order-n stack has a link to a (necessarily lower-ordered) stack situated below it.

Stacks with links

Fix a stack alphabet Γ and a distinguished bottom-of-stack symbol ⊥ ∈ Γ. An order-0 stack (or simply 0-stack) is just a stack symbol. An order-(n + 1) stack (or simply (n + 1)-stack) s is a non-null sequence (written [s 1 • • • s l ]) of n-stacks such that every non-⊥ Γ-symbol a that occurs in s has a link to a stack of some order k (say, where 0 ≤ k ≤ n) situated below it in s; we call the link a (k + 1)-link. The order of a stack s is written ord(s).

As usual, the bottom-of-stack symbol ⊥ cannot be popped from or pushed onto a stack. Thus we require an order-1 stack to be a non-null sequence [a 1 • • • a l ] of elements of Γ such that for all 1 ≤ i ≤ l, a i = ⊥ iff i = 1. We define ⊥ k , the empty k-stack, as follows:

⊥ 0 = ⊥ and ⊥ k+1 = [⊥ k ].
We first define the operations pop i and top i with i ≥ 1: top i s returns the top (i -1)-stack of s, and pop i s returns s with its top (i -1)-stack removed. Precisely let s = [s 1 • • • s l+1 ] be a stack with 1 ≤ i ≤ ord(s):

top i [s 1 • • • s l+1 ] s = s l+1 if i = ord(s) top i s l+1 if i < ord(s) pop i [s 1 • • • s l+1 ] s = [s 1 • • • s l ] if i = ord(s) and l ≥ 1 [s 1 • • • s l pop i s l+1 ] if i < ord(s)
By abuse of notation, we set top ord(s)+1 s = s. Note that pop i s is undefined if top i+1 s is a one-element i-stack. For example pop 2 [[⊥ a b]] is undefined.

There are two kinds of push operations. First the first-order push. Let a be a non-⊥ stack symbol and 1 ≤ k ≤ ord(s), we define a new stack operation push a,k 1 that, when applied to s, first attaches a link from a to the (k -1)-stack immediately below the top (k -1)-stack of s, then pushes a (with its link) onto the top 1-stack of s. Formally for 1 ≤ k ≤ ord(s) and a ∈ (Γ \ { ⊥ }), we define

push a,k 1 [s 1 • • • s l+1 ] s =                [s 1 • • • s l push a,k 1 s l+1 ] if k < ord(s) [s 1 • • • s l s l+1 a † ] if k = ord(s) = 1 [s 1 • • • s l push a 1 s l+1 ] if k = ord(s) ≥ 2 and l ≥ 1
where

• a † denotes the symbol a with a link to the 0-stack s l+1

• a denotes the symbol a with a link to the (k -1)-stack s l ; and we define

push a 1 [t 1 • • • t r+1 ] t =        [t 1 • • • t r push a 1 t r+1 ] if ord(t) > 1 [t 1 • • • t r+1 a]
otherwise i.e. ord(t) = 1

The higher-order push j , where j ≥ 2, simply duplicates the top (j -1)-stack of s. Precisely, let s = [s 1 • • • s l+1 ] be a stack with 2 ≤ j ≤ ord(s):

push j [s 1 • • • s l+1 ] s =        [s 1 • • • s l+1 s l+1 ] if j = ord(s) [s 1 • • • s l push j s l+1 ] if j < ord(s)
Note that in case j = ord(s) above, the link structure of s l+1 is preserved by the copy that is pushed on top by push j .

Finally there is an important operation called collapse. We say that the n-stack s 0 is a prefix of an nstack s, written s 0 ≤ s, just in case s 0 can be obtained from s by a sequence of (possibly higher-order) pop operations. Take an n-stack s whose top 1 -element has a link to (a particular copy of) k-stack u somewhere in s, such that top k+1 s 0 is (that copy of) u for some s 0 ≤ s. Then collapse s is defined to be s 0 .

A formal definition of CPDA stack operations

One way to give a formal semantics of the stack operations is to work with appropriate numeric representations of the links. Knapik et al. have shown how this can be done in the order-2 case -called panic automata -in [16]. Here we introduce a different encoding of stacks with links that works for all orders. The idea is simple: take an order-n stack s and suppose there is a link from (a particular occurrence of) a symbol a in s to some (j -1)-stack. First denote by s the unique prefix of s whose top 1 -element is the occurrence of a. Then there exists a unique k such that collapse s = pop j ; • • • ; pop j k s. In s, we represent the occurrence of a with its link as a (j,k) , where the superscipt (j, k) is a shorthand for the iterated stack operation pop k j = pop j ; • • • ; pop j k .

In the formal definition, a symbol-with-link of an order-n CPDA is written a (j,k) , where a ∈ Γ, 1 ≤ j ≤ n and k ≥ 1, such that3 if j = 1 then k = 1. Further, purely for convenience, we require that if a = ⊥ then j = k = 1.

The set Op n of order-n CPDA stack operations comprises four types of operations:

1. pop k for each 1 ≤ k ≤ n 2. push j for each 2 ≤ j ≤ n 3. push a,k 1 for each 1 ≤ k ≤ n and each a ∈ (Γ \ { ⊥ }), and 4. collapse.

We define them in terms of the standard stack operations of an order-n PDA (namely, pop j 's, top j 's and push - 1 's) as follows, where 1 ≤ i ≤ ord(s) and 2 ≤ j ≤ ord(s): push b,i 1 s = push b (i,1) 1 s collapse s = pop f e s where top 1 s = a (e,f )

push j [s 1 • • • s l+1 ] s =        [s 1 • • • s l+1 s j l+1 ] if j = ord(s) [s 1 • • • s l push j s l+1 ] if j < ord(s)
where Θ j is the operation of replacing every superscript occurring in Θ of the form (j, k j ) (for some k j ) by (j, k j + 1). The meaning of pop j is the standard one. [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] ]]] [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] c [START_REF] Cachat | Higher order pushdown automata, the Caucal hierarchy of graphs and parity games[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] ]]] push 2 (push c,3 1 (push b,2 [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] c [START_REF] Cachat | Higher order pushdown automata, the Caucal hierarchy of graphs and parity games[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] ][⊥ a b [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] c [START_REF] Cachat | Higher order pushdown automata, the Caucal hierarchy of graphs and parity games[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] ]]] push 3 (push c,3 1 (push b,2 [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] c [START_REF] Cachat | Higher order pushdown automata, the Caucal hierarchy of graphs and parity games[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] ]] [[⊥][⊥ a b [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] c [START_REF] Cachat | Higher order pushdown automata, the Caucal hierarchy of graphs and parity games[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] ]]] and we have collapse(push 2 (push c,3 1 (push b,2 1 s))) = collapse(push 3 (push c,3 1 (push b,2

push c,3 1 (push b,2 1 s) = [[[⊥ a]] [[⊥][⊥ a b
1 s)) = [[[⊥ a]] [[⊥][⊥ a b
1 s)) = [[[⊥ a]] [[⊥][⊥ a b
1 s))) = [[[⊥ a]]]

Tree-generating CPDA

Collapsible pushdown automata are a generalization (to all finite orders) of pushdown automata with links [2, 1], which are essentially the same as panic automata [16]. There are various versions of CPDA, depending on whether the automaton is used as an accepting or generating device (for word language, or a labelled tree or graph, in which case there is an accompanying input alphabet of an appropriate kind) or to describe a computational process. Here we consider the version for generating Σ-labelled trees, for a given ranked alphabet Σ. (When it is used to generate graphs -see Section 6, we shall refer to the device as collapsible pushdown systems.) Definition 2.2 A tree generating order-n collapsible pushdown automaton (n-CPDA) is given by a 5-tuple A = Σ, Γ, Q, δ, q 0 where Σ is a ranked alphabet, Γ is a stack alphabet, Q is a finite set of control states, q 0 is the initial state, and δ is the transition function

δ : Q × Γ -→ (Q × Op n + { (f ; q 1 , • • • , q ar (f ) ) : f ∈ Σ, q i ∈ Q })
(We require δ to respect the standard convention that ⊥ cannot be pushed onto or popped from the stack.)

Configurations of an n-CPDA are pairs of the form (q, s) where q ∈ Q and s is an n-stack over Γ; we call (q 0 , ⊥ n ) the initial configuration. A generalized configuration (ranged over by γ, γ i , etc.) is either a configuration or a triple of the form (f ; q 1 , • • • , q ar (f ) ; s). We define a one-step labelled transition relation of A over generalized configuration by clauses, one for each of the three kinds4 of label I, P and O:

I. (q, s) (q ,θ)
> (q , s ), if for some θ ∈ Op n , we have δ(q, top 1 s) = (q , θ) and s = θ(s) P. (q, s)

(f ;q) > (f ; q 1 , • • • , q ar (f ) ; s), if δ(q, top 1 s) = (f ; q 1 , • • • , q ar (f ) ) O. (f ; q 1 , • • • , q ar (f ) ; s) (f,i) > (q i , s), for each 1 ≤ i ≤ ar (f ).
The labelled transition relation is deterministic in the sense that for any generalized configuration γ and for any label , if γ > γ 1 and γ > γ 2 then γ 1 = γ 2 . We write γ 1 > γ 2 just if γ 1 > γ 2 for some label . Note that the unlabelled > is not deterministic in general, but it is when restricted to configurations (because δ is).

A computation path of A is a finite or infinite transition sequence of the form

ρ = γ 0 0 > γ 1 1 > γ 2 2 > • • •
where γ 0 is the initial configuration. Every computation path is uniquely determined by the associated label sequence, namely, 0 1 2 • • • . Observe that such label sequences satisfy the regular expression (I * P O) ω + (I * P O) * I ω if the sequence is infinite, and (I * P O) * I * (ε + P + P O) if the sequence is finite. The Σprojection of ρ is the subsequence r 1 r 2 r 3 • • • of labels of the shape (f, i) (in which case ar (f ) ≥ 1) or of the shape (f ; ε) (in which case ar (f ) = 0, and the label occurs at the end of the Σ-projection). We say the CPDA A generates the Σ-labelled tree t just in case the branch language5 of t coincides with the Σ-projection of computation paths of A.

Remark 2.3

Order-2 collapsible pushdown automata (2-CPDA) are a slight variant of pushdown automata with links in [2, 1]. They are essentially the same as panic automata in the sense of Knapik et al. [16], which use numeric indices to represent links.

Recursion schemes

Types are generated by the grammar A ::= o | A → A. Every type A = o can be written uniquely as

A 1 → • • • → A n → o (
by convention arrows associate to the right) which we shall abbreviate to (A 1 , • • • , A n , o), for some n ≥ 1 which is called its arity; the base type o has arity 0. We define the order of a type by: ord(o) = 0 and ord(A → B) = max(ord(A) + 1, ord(B)). Let Σ be a ranked alphabet i.e. each Σ-symbol f has an arity

ar (f ) ≥ 0 which determines its type o → • • • → o → ar (f )
o. Further we shall assume that each symbol f ∈ Σ is assigned a finite set Dir(f ) = { 1, • • • , ar (f ) } of directions, and we define Dir(Σ) = f ∈Σ Dir(f ). Let D be a set of directions; a D-tree is just a prefix-closed subset of D * , the free monoid of D. A Σ-labelled tree is a function t : Dom(t) -→ Σ such that Dom(t) is a Dir(Σ)-tree, and for every node α ∈ Dom(t), the Σ-symbol t(α) has arity k if and only if α has exactly k children and the set of its children is { α 1, • • • , α k } i.e. t is a ranked (and ordered) tree. We write T ∞ (Σ) for the set of (finite and infinite) Σ-labelled ranked and ordered trees.

The tree generated by a (deterministic) recursion scheme

Let Ξ be a set of typed symbols. The set of applicative terms of type A generated from Ξ, written T A (Ξ), is defined by induction over the following rules: if

f : A is an element of Ξ then f ∈ T A (Ξ); if s ∈ T A→B (Ξ) and t ∈ T A (Ξ) then st ∈ T B (Ξ).
For simplicity we write T (Ξ) to mean T o (Ξ), the set of ground terms. In case Ξ is a ranked alphabet (and so every Ξ-symbol has an order-0 or order-1 type determined by its arity) we identify terms in T (Ξ) with the finite trees in T ∞ (Ξ).

For each type A, we assume an infinite set Var A of variables of type A, such that Var A and Var B are disjoint whenever A = B; and we write Var for the union of Var A as A ranges over types. We use letters x, y, ϕ, ψ, χ, ξ etc. to range over variables. We write s : A to mean "the expression s has type A". A (deterministic) recursion scheme is a 4-tuple G = Σ, N , R, S where

• Σ is a ranked alphabet of terminals (including a distinguished symbol ⊥ : o)
• N is a finite set of typed non-terminals; we use upper-case letters F, H, etc. to range over non-terminals

• S ∈ N is a distinguished start symbol of type o • R is a finite set of rewrite rules, one for each non-terminal F : (A 1 , • • • , A n , o), of the form F ξ 1 • • • ξ n → e
where each ξ i is a variable of type A i , and e is an applicative term in T (Σ ∪ N ∪ { ξ 1 , • • • , ξ n }). Note that the expressions on either side of the arrow are terms of ground type.

The order of a recursion scheme is defined to be the highest order of (the types of) its non-terminals.

Value tree [[ G ]] of a recursion scheme G

In this paper we use recursion schemes as generators of Σ-labelled trees. Informally the value tree6 of (or the tree generated by) a recursion scheme G, [[ G ]], is a possibly infinite applicative term (of ground type), constructed from the terminals in Σ, that is obtained by unfolding the rewrite rules of G ad infinitum, replacing formal by actual parameters each time, starting from the start symbol S.

To define [[ G ]], we first introduce a map (•) ⊥ : T (Σ ∪ N ) -→ T (Σ) that takes an applicative term and replaces each non-terminal, together with its arguments, by ⊥. We define (•) ⊥ by structural recursion as follows: we let f range over Σ-symbols, and F over non-terminals in N

f ⊥ = f F ⊥ = ⊥ (st) ⊥ = ⊥ if s ⊥ = ⊥ (s ⊥ t ⊥ ) otherwise.
Clearly if s ∈ T (Σ ∪ N ) is of ground type then s ⊥ ∈ T (Σ) is of ground type. Henceforth we shall identify ground-type terms in T (Σ) with finite trees in T ∞ (Σ).

Next we define a one-step reduction relation → G which is a binary relation over terms in T (Σ ∪ N ). Informally s → G s just if s is obtained from s by replacing some occurrence of a non-terminal F by the right-hand side of its rewrite rule in which all formal parameters are in turn replaced by their respective actual parameters, subject to the proviso that the F must occur at the head of a subterm of ground type. Formally → G is defined by induction over the following rules:

• (Substitution). F t 1 • • • t n → G e[t 1 /ξ 1 , • • • , t n /ξ n ] where F ξ 1 • • • ξ n → e is a rewrite rule of G. • (Context). If t → G t then (st) → G (st ) and (ts) → G (t s).
The relation ↓ G between terms and trees is then defined as follows: We say that s

↓ G t where s ∈ T (Σ ∪ N ) and t ∈ T ∞ (Σ) just if • there is a finite reduction sequence s = t 0 → G • • • → G t n = t,
and t is a finite tree, none of whose node is labelled ⊥; or

• there is an infinite reduction sequence s = t 0 → G t 1 → G t 2 • • • such that t = lim t ⊥ i : i ∈ ω
, and t may be a finite tree (in which case, some of t's nodes are labelled ⊥) or an infinite tree.

Recall that T ∞ (Σ) is a complete partial order with respect to the approximation ordering as defined by: t t just if Dom(t) ⊆ Dom(t ) and for all w ∈ Dom(t), we have t(w) = ⊥ or t(w) = t (w) (i.e. t is obtained from t by replacing some ⊥-labelled nodes by Σ-labelled trees). We can finally define the Σ-labelled ranked tree [[ G ]], called the value tree of (or the tree generated by) G, as follows:

[[ G ]] = sup{ t ∈ T ∞ (Σ) : S ↓ G t }.
The supremum is well-defined because the set in question is directed, which is a consequence of the Church-Rosser property of G viewed as a rewrite system. We write RecTree n Σ for the class of value trees [[ G ]] where G ranges over order-n recursion schemes.

Example 3.1 Let G be the order-2 (unsafe [START_REF] Courcelle | The monadic second-order logic of graphs IX: machines and their behaviours[END_REF] ) recursion scheme with rewrite rules:

S → H a H z → F (g z) F ϕ → ϕ (ϕ (F h))
where z : o and ϕ : (o, o), and the arities of the terminals g, h, a are 2, 1, 0 respectively, and the type of a variable is written as its superscript. The value tree [[ G ]] is the Σ-labelled tree representing the infinite term g a (g a (h (h (h

• • • )))): g w w w w w G G G G G a g w w w w w G G G G G a h h . . .
The only infinite path in the tree is the node-sequence ε

• 2 • 22 • 221 • 2211 • • • .

Graph representing a recursion scheme

We write [n] as a shorthand for { 1,

• • • , n } and [n] 0 for { 0, • • • , n }. Fix a ranked alphabet Σ. Typically 8 Dir(f ) = [ar (f )] (but we always have |Dir(f )| = ar (f ) for each Σ-symbol f ). We define Dir(Σ) = f ∈Σ Dir(f ).
We recall the long transform of a recursion scheme as introduced in [21]. Fix a recursion scheme G. Rules of the new recursion scheme G (which, we shall see, can be regarded as order 0) are obtained from those of G by applying the following four operations in turn, which we call long transform. For each G-rule:

1. Expand the RHS to its η-long form. I.e. we hereditarily η-expand every subterm -even if it is of ground type -provided it occurs in an operand position (i.e. it is the second argument of some occurrence of the application operator). Note that each applicative term s ∈ T (Σ ∪ N ∪ { ξ 1 , • • • , ξ l }) can be written uniquely as † s 1 • • • s m where † is either a variable (i.e. some ξ j ) or a non-terminal or a terminal. Suppose [START_REF] Courcelle | The monadic second-order logic of graphs IX: machines and their behaviours[END_REF] The safety constraint (on lambda terms) may be regarded as a reformulation of the constraint on lambda terms imposed by Damm's derived types, first introduced in his major study on the semantics of Algol-like languages [8]. To define safety, we first need to introduce homogeneous types: The base type o is homogeneous;

† s 1 • • • s m : (A 1 , • • • , A n , o). First we define † s 1 • • • s m = λϕ. † s 1 • • • s m ϕ 1 • • • ϕ n where ϕ is a list ϕ 1 • • • ϕ n of (fresh) pairwise-distinct variables (which is a null list iff n = 0) of types A 1 , • • • , A n respectively, none of which occurs free in † s 1 • • • s m . Take any e = † s 1 • • • s m of ground type. The η-long form of e is defined to be † s 1 • • • s m .
a function type A1 → (A2 → • • • → (An → o) • • • ) is homogeneous just if each Ai is homogeneous, and ord(A1) ≥ ord(A2) ≥ • • • ≥ ord(An).
We say that a term (or a rewrite rule or a recursion scheme) is homogeneously typed just if all types that occur in it are homogeneous. Knapik et al. [15] define safety as follows: A homogeneously-typed term of order k > 0 is said to be unsafe if it contains an occurrence of a parameter of order strictly less than k, otherwise the term is safe. An occurrence of an unsafe term t, as a subexpression of a term t , is safe if it occurs in an operand position (i.e. it is in the context • • • (ts) • • • ), otherwise the occurrence is unsafe. A recursion scheme is safe if no unsafe term has an unsafe occurrence in the right-hand side of any rewrite rule. Note that it follows from the definition that all recursion schemes of order at most 1 are safe. [START_REF] Damm | The IO-and OI-hierarchy[END_REF] The only exception is the symbol @A of the auxiliary alphabet ΛG, where we have Dir(@A) = [ar (@A) -1]0.

For example the η-long form of g a : o is g (λ.a); we shall see that the "dummy lambda-abstraction"9 λ.a (that binds a null list of variable) plays a useful rôle in the syntactic representation of the game semantics of a recursion scheme.

2. Insert long-apply symbols @ A : Replace each ground-type subterm of the shape D e

((A 1 , • • • , A n , o), A 1 , • • • , A n , o).
In the following, we shall often omit the type tag A from @ A .

3. Curry the rewrite rule. I.e. we transform the rule

F ϕ 1 • • • ϕ n → e to F → λϕ 1 • • • ϕ n .e .
In case n = 0, note that the curried rule has the form F → λ.e .

4.

Rename bound variables afresh, so that any two variables that are bound by different lambdas have different names.

For every recursion scheme G, the system of transformed rules in G defines an order-0 recursion scheme -called the long transform of G -with respect to an enlarged ranked alphabet Λ G , which is Σ augmented by certain variables and lambdas (of the form λξ which is a short hand for λξ 1 • • • ξ n where n ≥ 0) but regarded as terminals. The alphabet Λ G is a finite subset of the set

Σ ∪ Var ∪ { @ A : A ∈ ATypes } Non-lambdas ∪ { λξ : ξ ⊆ Var }

Lambdas

where ATypes is the set of types of the shape

((A 1 , • • • , A n , o), A 1 , • • • , A n , o) with n ≥ 1.
We rank the symbols in Λ G as follows:

• variable symbol ϕ : (A 1 , • • • , A n , o) in Var has arity n • long-apply symbol @ A where A = ((A 1 , • • • , A n , o), A 1 , • • • , A n , o) has arity n + 1
• lambda symbol λξ has arity 1, for every list of variables ξ ⊆ Var .

Further, for f ∈ Λ G , we define

Dir(f ) = [ar (@ A ) -1] 0 if f = @ A [ar (f )] otherwise
For technical reasons (to be clarified shortly), the leftmost child of an @-labelled node α is in direction 0 (i.e. it is α's 0-child); for all other nodes, the leftmost child is in direction 1. The non-terminals of G are exactly those of G, except that each is assigned a new type, namely, o. We can now define the computation tree λ(G) to be the value tree [[ G ]] of the order-0 recursion scheme G. It follows that λ(G) is a regular tree.

A Λ-labelled deterministic digraph (or DDG, for short) is a quadruple

K = V, E ⊆ V × V, l : V -→ Λ, v 0 ∈ V
where the underlying digraph V, E is vertex-labelled by the function l : V -→ Λ (where Λ is a ranked alphabet), and edge-labelled by Dir(Λ) in that E = i∈Dir(Λ) E i , such that (i) for each i ∈ Dir(Λ), we have

E i ⊆ V × V is a partial function (ii) for each v ∈ V , and each i ∈ Dir(l(v)), we have E i (v) is defined i.e. { v : (v, v ) ∈ E i } is a singleton set.
In the following we shall assume that V is finite. It is easy to see that every finite Λ-labelled tree can be presented as a DDG, and the unfolding of a Λ-labelled DDG is a Λ-labelled tree.

Fix a higher-order recursion scheme G and an associated long transform G. We define the HORS graph Gr(G) to be the Λ G -labelled DDG determined by G

Gr(G) = V, E ⊆ V × V, λ G : V -→ Λ G , v 0 ∈ V
thatq is obtained by the following procedure:

1. First we define the ranked alphabet

Λ + G = Λ G ∪ N G where each symbol in N G (i.e. a non-terminal of G) is given arity 0. 2. For each G-rule (say) F → λϕ 1 • • • ϕ n .e, the corresponding Λ + G -labelled DDG D F = V F , E F ⊆ V F × V F , l F : V F -→ Λ + G , r t F given by the Λ +
G -labelled tree that is determined by the right-hand side of the rule, namely, λϕ 1 • • • ϕ n .e. Note that we have l F (r t F ) = λϕ 1 • • • ϕ n with reference to the rule F given above.

3. Set the digraph D to be the disjoint union of the underlying digraph of D F , as F ranges over N G . We then define the underlying digraph of Gr(G) to be D quotiented by the equivalence classes E F , one for each F in N G ; where we define

E F =   H∈N G l -1 H ({ F })   ∪ { r t F }
I.e. in Gr(G) all vertices in E F are identified, for each F ∈ N G . Henceforth, as a vertex of Gr(G), we shall refer to the equivalence class E F by the representative r t F .

The edge-labels of Gr(G) are inherited from the edge-labels of the component DDGs D F (we define E i (r t F ) = E F i (r t F ) for each F ∈ N G ). The vertex-labels are defined by

λ G (v) = l F (r t F ) if v = E F for some F ∈ N G l H (v) otherwise, suppose v is a vertex in V H
The root v 0 of Gr(G) is r t S , where S is the start symbol of G.

In the following, we shall only concern ourselves with the connected component of Gr(G) that contains the root node (and assume that Gr(G) is that connected component). It is easy to see that unfolding Gr(G) gives the computation tree λ(G).

Example 3.2

We revisit the recursion scheme of Example 3.1 and consider the graph determined by it. First the long transform:

G :        S = G a G z = F (g z) F ϕ = ϕ (ϕ (F h)) → G :        S = λ.@ G (λ.a) G = λz.@ F (λy.g (λ.z) (λ.y)) F = λϕ.ϕ (λ.ϕ (λ.@ F (λx.h (λ.x))))
The graph Gr(G) is then given in Figure 1.

λ 1 @ 0 q q q x x q q 1 K K K 7 7 K K K λz 1 λ 1 @ 0 r r r x x r r 1 L L L 7 7 L L a λϕ 1 λy 1 ϕ 1 g 1 q q q x x q q q 2 K K K 7 7 K K K λ 1 λ 1 λ 1 ϕ 1 z y λ 1 @ 0 e e 1 M M M 8 8 M M λx 1 h 1 λ 1 x Figure 1:
The graph determined by an order-2 recursion scheme.

Notations and features of HORS graphs

Fix a HORS graph Gr(G) = V, E, λ G , v 0 . We shall call a node of Gr(G) prime just if it is the 0-child10 of a @-labelled node. By construction, a prime node is labelled by a lambda. We define the depth of a node to be the length of the shortest path from the root to the node (so that the root has depth 0). Let u be a node. We define pred(u) = { u ∈ V : (u , u) ∈ E } i.e. the set of predecessors of u. For every node u labelled by a variable ϕ i (say), its binder, written binder(u), is the node that is labelled λϕ, where ϕ is a list of variables that contains ϕ i . (Since bound variables are renamed to prevent any clash in the construction of G, every variable node in Gr(G) has a unique binder.) We say that u is the i-parameter of binder(u) just if ϕ i is the ith-item of the list ϕ. The span of the variable node u is defined to be the depth of binder(u) minus the depth of u.

We note the following features of HORS graphs:

(i) Except the root and possibly some prime nodes, every node u has a unique predecessor.

(ii) For every non-root node u, there is some j such that for every predecessor v of u, u is the j-child of v; hence (and in this case) we can say that u is a j-child. Indeed a node is a 0-child if and only if it is prime.

(iii) For every node u, there is a unique shortest path from binder(u) to u, and this path does not contain any prime node.

For convenience, and whenever it is safe to do so, we shall confuse a node u with its Λ G -label λ G (u).

From CPDA to recursion schemes

In this section we prove that for every n ≥ 0, and every n-CPDA A, there is an order-n recursion scheme G A such that A and G A define the same Σ-labelled tree. We begin by introducing a method to represent higher-order stacks and configurations by applicative terms constructed from non-terminals of the same order; the correctness of the representation is then established in Theorem 3. The Theorem is quite general: it is independent of the transition relation of the automaton, nor does it matter whether the automaton is for defining a tree or a graph. In case the automaton A is for generating a Σ-labelled tree t (say), we show in Section 4.3 how an order-n deterministic recursion scheme G A can be constructed that defines the same tree i.e. [[

G A ]] = t.
The correctness of the transform G A (Theorem 5) is then obtained as a corollary of Theorem 3.

Our construction simplifies the translation (order-2) in [16] and generalizes it to all finite orders. For convenience let the state-set of A be [m] where m ≥ 1. Let 0 be the base type. Inductively, for n ≥ 0, we define the type

n + 1 = n m → n where n m = n × • • • × n m times . Thus n + 1 = n m → (n -1) m → • • • → 0 m → 0.

Term representation of stacks and configurations

Fix an order-n CPDA A. We shall first introduce a general scheme for representing stacks and configurations of A by applicative terms generated from the non-terminals from N A . The key result in this section is a correctness theorem (Theorem 3) for the representation scheme.

Recall that every non-⊥ symbol in an n-stack has a link to some stack (of order necessarily less than n) that lies below it in the stack. If the stack pointed to is of order j -1 where 1 ≤ j ≤ n, the link is said to be a j-link. A 1-link from a symbol always points to the symbol immediately below it; no stack operation will alter it. Henceforth we shall use the formal definition of higher-order stacks, according to which a symbol with link takes the form a (j,k) . For technical convenience, we require that j = k = 1 in case a = ⊥. E.g. the initial configuration is (q 0 , ⊥ n ) with top 1 ⊥ n = ⊥ [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF][START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] .

For each stack symbol a, each 1 ≤ e ≤ n and each state 1 ≤ p ≤ m, we introduce a non-terminal

F a,e p : (n -e) m → (n -1) m → • • • → 0 m → 0
(Note that the type of F a,e p is non-homogeneous in the sense of Knapik et al. [15].) In addition, for each 0 ≤ i ≤ n -1, we introduce a non-terminal Ω i : i; and we fix a start symbol S : 0. The set N A of nonterminals is defined as follows:

N A = { F a,e p : a ∈ Γ, 1 ≤ p ≤ m, 1 ≤ e ≤ n } ∪ { Ω i : 0 ≤ i ≤ n -1 } ∪ { S : 0 }
where S : 0 is the distinguished start symbol. Let T j (N A ) be the set of applicative terms (or simply terms) of type j generated from the elements of N A . In the following we shall use the following shorthand. Let P (i) be a term with an occurrence of i; we write P (i) | i to mean the m-tuple P (1),

• • • , P (m) . E.g. F a,e i | i means F a,e 1 , • • • , F a,e m : ((n -e) m → n) m .
A term M : nj where 0 ≤ j ≤ n is said to be head normal if its head symbol is a non-terminal of the form F a,e p i.e. M has the shape F a,e p L M n-1 • • • M n-j , for some a, e and p and for some vectors of terms L, M n-1 , • • • , M n-j of the appropriate types; we shall call F a,e p the head non-terminal of M . Let 0 ≤ j ≤ n, 1 ≤ p ≤ m and let s be a j-stack, a pair of the form (p, s) is called a j-configuration (thus a configuration is an n-configuration). The idea is that we use head-normal terms of type nj -which has the general shape F a,e p L M n-1 • • • M n-j : nj -to represent j-configurations; equivalently we use m-tuples of the form

F a,e i L M n-1 • • • M n-j | i : (n -j) m
to represent j-stacks.

Suppose the head-normal ground-type term

F a,e p L M n-1 • • • M 0 : 0
represents the configuration (p, s). Then the 0-configuration (p, top 1 s) -where the top 1 -element of s, say, a with a link to the e-stack represented by the m-tuple L : (ne) m -is represented by F a,e p L : n. Further for each 1 ≤ j ≤ n and 1 ≤ p ≤ m, we have:

• The (j -1)-configuration (p, top j s) is represented by F a,e p L M n-1 • • • M n-(j-1) : n -(j -1). • The configuration (p, pop j s) is represented by M n-j,p M n-j-1 • • • M 0 : 0. • The configuration (p, collapse s) is represented by L p M n-e-1 • • • M 0 : 0.
Take a head-normal ground-type term F a,e p L M n-1 • • • M 0 : 0. For each 1 ≤ j ≤ n, we shall call the m-tuple M n-j : (nj) m its (nj)-factor; by abuse of language, we shall call L : (ne) m its n-factor. Let 1 ≤ j ≤ n; we say that ground-type terms M and N are (nj)-similar, written M ∼ n-j N , just if they have the same head non-terminal, and for each 0 ≤ k ≤ n, provided k = j, M and N have the same (nk)-factors. It follows from the definition that if M and N are (nj)-similar and have the same (nj)-factor, then they are (syntactically) identical terms.

Labelled rewrite rules and the labelled transition relation Definition 4.1 (i) We first consider labelled rewrite rules of the general form

F a,e p Φ Ψ n-1 • • • Ψ 0 (q,θ) - Ξ (q,θ)
where for each 0 ≤ j ≤ n -1, we have

Ψ j = Ψ j1 , • • • , Ψ jm is a vector of variables, with each Ψ ji : j; similarly Φ = Φ 1 , • • • , Φ m is a vector of variables, with each Φ i : n -e.
The shape of Ξ (q,θ) depends on the pair (q, θ), as shown in Table 1 below, where 2 ≤ j ≤ n and 1 ≤ e, k ≤ n in the following: In the following, Cases of (q, θ)

Corresponding Ξ (q,θ) (q, push b,k 1 ) F b,k q Ψ n-k F a,e i Φ Ψ n-1 | i Ψ n-2 • • • Ψ 0 (q, push j ) F a,e q Φ Ψ n-1 • • • Ψ n-(j-1) F a,e i Φ Ψ n-1 • • • Ψ n-j | i Ψ n-(j+1) • • • Ψ 0 (q, pop k ) Ψ n-k,q Ψ n-k-1 • • • Ψ 0 (q, coll.) Φ q Ψ n-e-1 • • • Ψ 0 Table 1: Definition of Ξ (q,θ)
whenever we use θ, instead of (p, θ), to label a rewrite rule

F a,e p Φ Ψ n-1 • • • Ψ 0 θ - Ξ (p,θ)
it is understood that the state p is preserved.

(ii) The labelled rewrite rules induce a family of outermost labelled one-step transition relations (q,θ)

-→ ⊆ T 0 (N A ) × T 0 (N A ), indexed by the label (q, θ), where q ranges over states and θ ranges over stack operations.

Informally we define M (q,θ) -→ M just if M is obtained from M by replacing the head (equivalently, outermost) non-terminal F by the right-hand side of the corresponding rewrite rule in which all formal parameters are in turn replaced by their respective actual parameters. Formally (q,θ) -→ is defined by the following rule schemes: for

a ∈ Γ, 1 ≤ p, q ≤ m, 1 ≤ e ≤ n, θ ∈ Op n , and for each rewrite rule F a,e p Φ Ψ n-1 • • • Ψ 0 (q,θ)
-Ξ (q,θ) , we have the rule scheme

F a,e p L M n-1 • • • M 0 (q,θ) -→ Ξ (q,θ) [L/Φ, M n-1 /Ψ n-1 • • • , M 0 /Ψ 0 ]
where L, M n-1 , • • • , M 0 range over vectors of terms respecting the type of F a,e p .

Note that each binary relation It is straightforward to check that for any head-normal ground-type term M , we have

(q,θ) -→ is a partial function. Let α = θ 1 ; • • • ; θ l be a (composite) sequence of stack operations. We write α -→ ⊆ T 0 (N A ) × T 0 (N A ) to be the sequential composition of the partial function θ 1 -→, • • • ,
(M push j -→ ) pop k -→ = M pop k -→ if j < k M if j = k
Lemma 1 Suppose, for a fixed 2 ≤ j ≤ n, M and N are (nj)-similar ground-type terms.

(i) If j 1 > j then M pop j 1 -→ and N pop j 1 -→ are identical terms; if j 1 < j then M pop j 1 -→ and N pop j 1 -→ are (n -j)- similar. (ii) Let F a,e
p be the head non-terminal of M and N with e ≥ 2. If e > j then M coll.

-→ and N coll.

-→ are identical terms; and if e < j then M coll.

-→ and N

coll.

-→ are (nj)-similar.

Proof Straightforward consequences of the definitions of the transition relation.

For example take a head normal ground-type term M with 2 ≤ j ≤ n; we have M and M push j -→ are (nj)-similar.

Correctness of the representation

The position of a given stack symbol in an n-stack s can be described by a sequence of pop operations that are needed to "collapse" the stack up to the point where that position becomes the top 1 -element. For example, the position of b in the 2-stack (the top of stack is at the right-hand end)

[[⊥ a a] [⊥ a b a] [⊥ a a] [⊥ a]] is pop 2 2 ; pop 1 .
In general such sequences are not unique, though they can be normalized to one in which the respective orders of the pop operations form a non-increasing sequence. (Equivalently A sequence is normalized if it is inequivalent to any sequence of shorter length.) We shall call a normalized sequence for a given stack s an s-probe. Informally we say that a ground-type term

M represents a configuration (p, s) if for every s-probe α if the top 1 -element of α s is a (j,k) , then the head non-terminal of M α -→ is F a,j p ; further (M α -→) pop k j -→ = (M α -→) coll.
-→, and it represents the configuration (p, collapse(α s)).

Definition 4.2

Let s be an n-stack. A sequence α of stack operations of the shape

pop k 1 j 1 ; • • • ; pop k l j l
such that l ≥ 0, and j 1 > • • • > j l ≥ 1, and each k i ≥ 1, is said to be an s-probe just in case α s is defined.

(i) We say that a ground-type term M represents the configuration (p, s) if for every s-probe α, we have M α-matches (p, s).

(ii) We say that M α-matches the configuration (p, s) just if for some j and k, we have top 1 (α s) = a (j,k) and there exist m-tuples

L n-j , N n-1 , • • • , N 0 of the required types such that M α -→ F a,j p L n-j N n-1 • • • N 0 ; further if a = ⊥ then (M α -→) pop k j -→ = (M α -→) coll.
-→

and (M α -→) pop k j -→ represents the configuration (p, collapse(α s)).
Henceforth whenever we assert that a term α-matches a configuration (p, s), it has the force that α is an s-probe. [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] , and id is the only ⊥ n -probe.

Note that F ⊥,1 p Ω n-1 Ω n-1 • • • Ω n-j : n -j represents the j-configuration (p, ⊥ n-j ). We have top 1 ⊥ n = ⊥ (1,
Lemma 2

(i) If M represents (p, s) then for every s-probe α, we have (M α -→) represents (p, α s). (ii) Let α be an s-probe. If (M α -→) represents (p, α s) then M α-matches (p, s).
Proof Straightforward consequences of the definitions.

Having pinned down the notion of a term representing a configuration, we now show that the representation is preserved by the stack operations. This confirms that our notion of representation is the right one.

Theorem 3 (Correctness) Let M be a ground-type term, (p, s) be a configuration, and θ be a stack operation.

If M represents (p, s) and M θ -→ is defined, then M θ -→ represents the configuration (p, θ s). Proof Suppose M = F a,e p U V n-1 • • • V 0 represents the configuration (p, s).
We aim to prove that M θ -→ represents (p, θs) for each of the four cases of the operation θ ∈ Op n .

Case 1: θ = push b,j 0 1 where b is a non-⊥ symbol and 1 ≤ j 0 ≤ n.

We have M θ -→ F b,j 0 p V n-j 0 F a,e i U V n-1 | i V n-2 • • • V 0 . Let α = pop k 1 j 1 ; • • • ; pop k l j l be an (θ s)-probe.
• Suppose l = 0 i.e. α is the identity operation id . We need to show that (M [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] ; assuming b = ⊥, we check that

θ -→) id -matches (p, θs). Now top 1 (θ s) = b (j 0 ,
(M θ -→) pop j 0 -→ = (M θ -→) coll. -→ = V n-j 0 ,p V n-j 0 -1 • • • V 0 . It remains to show that (M θ -→) pop j 0 -→ represents the configuration (p, collapse(id (θ s))) = (p, pop j 0 (θ s)), which is equivalent to    M represents (p, s) if j 0 = 1 (M pop j 0 -→ ) represents (p, pop j 0 s) if j 0 > 1
Both cases follow from the assumption that M represents (p, s): the former because (M

push b 1 j 0 -→ ) j 0
-→ = M , and the latter because of Lemma 2.

• Suppose l ≥ 1 and j 1 ≥ 2. We have (M θ -→) α-matches (p, θs) iff M α-matches (p, s), which follows from the assumption.

• Suppose j 1 = 1. It follows that l = 1 and α = pop k 1 1 where k 1 ≥ 1. Set α = pop k 1 -1 1 (we shall assume that pop 0 1 = id ). Plainly (M θ -→) α-matches (p, θs) iff M α -matches (p, s)
, which is an immediate consequence of the assumption.

Case 2: θ = push j where 2 ≤ j ≤ n.

We have M

θ -→ F a,e p U V n-1 • • • F a,e i U V n-1 • • • V n-j | i • • • V 0 . Let α = pop k 1 j 1 ; • • • ; pop k l j l
be an (θ s)-probe. There are two subcases: a. The probe α reaches into pop j (θ s) = S; i.e. l ≥ 1 and j 1 ≥ j.

b. The probe α is confined to top j (θ s); i.e. either l ≥ 1 and j 1 < j, or l = 0.

Case 2a: Since (M θ -→) pop j 1 -→ =    M pop j 1 -→ if j < j 1 M if j = j 1
and correspondingly

(p, pop j 1 (θ s)) = (p, pop j 1 s) if j < j 1 (p, s) if j = j 1
we have (M θ -→) α-matches (p, θ s) as required.

Case 2b: Let b be the set of (θ s)-probes of this case. We define a partial order < over b-probes by α 1 < α 2 just if there is a non-empty sequence of pop-operations such that β(α 2 (θ s)) = α 1 (θ s); in other words α 1 (θ s) is a prefix of α 2 (θ s). We shall show, by an induction argument, that (M

θ -→) α -→ represents (p, α (θ s)) for ev- ery b-probe α; note that this implies (M θ -→) α-matches (p, θ s) as required. The base case is trivial. Suppose for all b-probes α < α 0 , we have (M θ -→) α -→ represents (p, α (θ s)). We aim to show that (M θ -→) α 0 -→ rep- resents (p, α 0 (θ s))
. Take any α 0 (θ s)-probe β; we want to show that ((M

θ -→) α 0 -→) β-matches (p, α 0 (θ s)
). Now α 0 ; β is equivalent to a (θ s)-probe of either case a or case b. The former case has already been dealt with. In the latter case, either α 0 ; β < α 0 or β = id . If α 0 ; β < α 0 , then by the induction hypothe-

sis ((M θ -→) α 0 -→) β -→) represents (p, β(α 0 (θ s))), which implies that (M θ -→) α 0 -→ β-matches (p, α 0 (θ s)) as desired. It remains to prove ((M θ -→) α 0 -→) id -matches (p, α 0 (θ s)). Suppose the top 1 -element of α 0 (θ s) is b (e ,f ) . Since top j (θ s) = top j S, the top 1 -element of α 0 S is b (e ,g) where g = f if e = j f -1 if e = j
((M θ -→) α 0 -→) pop f e -→ = ((M θ -→) α 0 -→) coll.
-→

and

((M θ -→) α 0 -→) pop f e -→ represents (p, collapse(α 0 (θ s))). (2)
But since the top 1 -element of α 0 (θ s) is b (e ,f ) , we have

(p, pop f e (α 0 (θ s))) = (p, collapse(α 0 (θ s)))
; further, by the induction hypothesis (in case e < j) or the assumption of M representing (p, s) (in case e ≥ j) as appropriate, we have

((M θ -→) α 0 -→) pop f e -→ represents (p, pop f e (α 0 (θ s)))
; hence (2) holds. It now remains to prove (1). We consider the three cases of e in turn: i. Case of e < j: Since M and M θ -→ are (nj)-similar, by applying Lemma 1 repeatedly, we have

((M θ -→) α 0 -→) pop f e -→ ∼ n-j (M α 0 -→) pop f e -→ ((M θ -→) α 0 -→) coll. -→ ∼ n-j (M α 0 -→) coll. -→ Since M α 0 -→ represents (p, α 0 s) and α 0 S has top 1 -element b (e ,f ) , we have (M α 0 -→) pop f e -→ = (M α 0 -→) coll.
-→. Thus

((M θ -→) α 0 -→) pop f e -→ ∼ n-j ((M θ -→) α 0 -→) coll.
-→.

But observe that ((M

θ -→) α 0 -→) pop f e -→ and ((M θ -→) α 0 -→) coll.
-→ have the same (nj)-factor. Hence

((M θ -→) α 0 -→) pop f e -→ = ((M θ -→) α 0 -→) coll.
-→ as required.

ii. Case of e = j: By definition of push j , we have top 1 (α 0 s) = b (e ,f -1) and f ≥ 2. Since M represents (p, s) by assumption, we have M α 0 -matches (p, s). It follows that

(M α 0 -→) pop f -1 e -→ = (M α 0 -→) coll.
-→.

Now, as a consequence of Lemma 1, for some vectors P , N n-1 , • • • , N n-j+1 of terms of the appropriate types, we have

(M θ -→) α 0 -→ F b,e p P N n-1 • • • N n-j+1 F a,e i U V n-1 • • • V n-j | i V n-j-1 • • • V 0 M α 0 -→ F b,e p P N n-1 • • • N n-j+1 V n-j V n-j-1 • • • V 0 (4)
and hence we have

(M α 0 -→) coll. -→ = ((M θ -→) α 0 -→) coll.
-→.

In view of ( 3) and ( 5), in order to prove (1), it suffices to prove

(M α 0 -→) pop f -1 j -→ = ((M θ -→) α 0 -→) pop f j -→ . (6)
But it follows from (4) that

((M θ -→) α 0 -→) pop j -→ = F a,e p U V n-1 • • • V n-j V n-j-1 • • • V 0 and so, since f ≥ 2, we have ((M θ -→) α 0 -→) pop f e -→ = ((M θ -→) α 0 -→) coll.
-→ as required.

iii. Case of e > j: By applying Lemma 1 repeatedly, we have

((M θ -→) α 0 -→) pop f e -→ = (M α 0 -→) pop f e -→ ((M θ -→) α 0 -→) coll. -→ = (M α 0 -→) coll.
-→

Since (M α 0 -→) pop f e -→ = (M α 0 -→) coll.
-→ we have

((M θ -→) α 0 -→) pop f e -→ = ((M θ -→) α 0 -→) coll.
-→ as required.

Case 3: θ = pop k where 1 ≤ k ≤ n.
This is an immediate consequence of Lemma 2.

Case 4: θ = collapse.

Suppose top 1 S = a (e,k) and a = ⊥ so that θ s = pop k e s; we have

M θ -→ U p V n-e-1 • • • V 0 . By assumption, we have M id -matches (p, s). It follows that (M id -→) pop k e -→ U p V n-e-1 • • • V 0 ; further (M id -→) pop k e -→,
which equals M θ -→, represents the configuration (p, collapse(id s)) = (p, θ s), as required.

The recursion scheme G

A determined by a CPDA A Definition 4.3 Fix a tree-generating order-n CPDA A = Σ, Γ, Q, δ, q 0 with Q = [m] for some m ≥ 1, and q 0 = 1. The order-n recursion scheme determined by A, written G A , is defined by the following rewrite rules. There are two kinds of rewrite rules, corresponding to the labels I and P: I. For each (p, a, q, θ) ∈ δ and 1 ≤ e ≤ n, we have the rule:

F a,e p Φ Ψ n-1 • • • Ψ 0 (q,θ) - Ξ (q,θ)
where Ξ (q,θ) is as given in Table 1.

P.

For each (p, a, (f ; q 1 , • • • , q ar (f ) )) ∈ δ and 1 ≤ e ≤ n, we have the rule:

F a,e p Φ Ψ n-1 • • • Ψ 0 (f,q) - f (F a,e q 1 Φ Ψ n-1 • • • Ψ 0 ) • • • (F a,e q ar (f ) Φ Ψ n-1 • • • Ψ 0 ).
Finally there is the start rule:

S -F ⊥,1 1 Ω n-1 Ω n-1 • • • Ω 0 . We write -→ ⊆ T 0 (Σ ∪ N ) × T 0 (Σ ∪ N
) for the one-step reduction relation11 between ground-type applicative terms (or ground terms, for short), defined to be the substitutive and contextual closure of the rewrite rules. We write -→ * as the reflexive, transitive closure of -→.

A ground term R is called a redex if for some term R we have R -→ R is a substitutive instance of a rewrite rule of label (say), and the redex is said to be P-type or I-type according to the type of ; by abuse of notation, we shall write R -R . A ground term is either head non-terminal (i.e. the head symbol is a non-terminal) or head terminal (i.e. of the shape f N 1 • • • N ar (f ) ). A head non-terminal ground term is either atomic (i.e. S or Ω 0 ) or it is head normal (i.e. the head symbol is of the form F a,e p , in which case, the ground term is an I-type or P-type redex).

It follows from the definition that for every one-step reduction M -→ M , there are a unique redex R with R -R and a unique active context [START_REF] Engelfriet | Interated stack automata and complexity classes[END_REF]

E such that M = E[R] and M = E[R ].
To indicate the active redex (and its occurrence in the term), we shall sometimes write M as (E, R), and write the one-step reduction as (E, R) -→ (E, R ), which we shall call P-type or I-type according to the type of the label . We shall call expressions of the shape (E, R) an active term; in general the ground-type term R may be a redex or a head-terminal term.

Path reduction sequences

Path reduction sequences are finite or infinite sequences of one-step reductions starting from the start symbol S. In essence, they constitute a reduction strategy for computing paths in the tree generated by the recursion scheme G A . Given a path in [[ G A ]] as specified by a word in the branch language (e.g. (f, 2) (g, 1) a) the path reduction strategy (that computes it) begins rewriting from S in a sequence of macro steps; each macro step computes an element (i.e. a Σ-symbol and a direction) of the word. Take the word (f, 2) (g, 1) a. The path reduction sequence begins from S by rewriting the leftmost redex until it reaches a head terminal term f N 1 • • • N ar (f ) , upon which N 2 is selected, corresponding to the pair (f, 2); the next macro step then starts from N 2 by rewriting the leftmost redex until it reaches a head terminal term g P 1 • • • P ar (g) , whereupon P 1 is selected, corresponding to (g, 1); the (terminal) macro step then starts from P 1 by rewriting the leftmost redex until it reaches a, which is a terminal node of the tree.

A path reduction sequence is a finite or infinite sequence of macro steps. Formally a macro step is a finite or infinite sequence of one-step reductions (of active terms) organized into (up to) three stages, starting from a given active term (E, R 1 ); if it terminates, the macro step returns an active term (E , N ) such that (E, R 1 ) -→ * (E , N ). The three stages are as follows:

1. A finite (possibly empty) or infinite sequence of I-type one-step reductions

(E, R 1 ) (q 1 ,θ 1 ) -→ (E, R 2 ) (q 2 ,θ 2 ) -→ (E, R 3 ) (q 3 ,θ 3 ) -→ (E, R 4 ) • • •
for some active context E. The sequence terminates (at (E, R r+1 )) iff for some r ≥ 0, we have R r+1 is not an I-type redex (i.e. R r+1 is a P-type redex). If the I-type reduction sequence does not terminate, the macro step is said to be partial.

A P-type

one-step reduction (E, R r+1 ) (f ;q) -→ (E, f N 1 • • • N ar (f ) ) where q = q 1 • • • q ar (f ) . 3. A O-type one-step reduction: The head-terminal active term (E, f N 1 • • • N ar (f ) ) is transformed to (E , N i ) for some 1 ≤ i ≤ ar (f )
, where

E = E[f N 1 • • • N i-1 [-] N i+1 • • • N ar (f ) ]
if ar (f ) ≥ 1 (in which case, by abuse of notation, we write

(E, f N 1 • • • N ar (f ) ) (f,i) -→ (E , N i ), even though E[f N 1 • • • N ar (f )
] and E [N i ] are identical terms); otherwise (i.e. f is nullary), there is no transformation, and the macro step in question is the terminal step of the path reduction sequence. Thus a typical macro step is a sequence of one-step reductions that may have the following shape:

(E, R 1 ) (q 1 ,θ 1 ) -→ • • • (qr,θr) -→ (E, R r+1 ) (f ;q) -→ (E, f N 1 • • • N ar (f ) ) (f,i) -→ (E , N i ) with E = E[f N 1 • • • N i-1 [-] N i+1 • • • N ar (f )
] and r ≥ 0. There are two other possibilities, namely, ar (f ) = 0 (in which case the macro step in question is the final step), or the macro step may consist of an infinite I-type reduction (in which case it is a partial step).

Proposition 4

The path reduction sequences compute all maximal traces of the Σ-labelled tree generated by G A .

Proof Take a macro step starting from a given decomposed term (E, R); stages 1 and 2 are completely determined; and stage 3 is specified by an O-type label (f, i), in case ar (f ) ≥ 1, with 1 ≤ i ≤ ar (f ). Thus a (maximal) path reduction sequence starting from S can be specified by

• an infinite sequence of O-type labels, or

• a finite sequence of O-type labels (ending in an partial macro step), or

• a finite sequence of O-type labels ending in a terminal macro step (specified by a nullary Σ-symbol).

We are now in a position to state the second major result of the section.

Theorem 5 (Equi-Expressivity 1)

Let A be a tree-generating CPDA, and let G A be the recursion scheme determined by A. Then the CPDA and the recursion scheme generate the same Σ-labelled tree.

Proof Because of Proposition 4, it suffices to prove

Claim: For any (finite or infinite) computation path of A of the form γ 0

0 > γ 1 1 > γ 2 2 > • • • , there is a unique path reduction sequence S -→ (E 0 , R 0 ) 0 -→ (E 1 , R 1 ) 1 -→ (E 2 , R 2 ) 2 -→ • • • with E 0 = [-] such that for every i ≥ 0, if R i is head-normal, then R i represents γ i .
The converse also holds.

To see why the claim is true, suppose

R i = F a,e p U V n-1 • • • V 0 and R i represents γ i = (p, s).
We consider the various types of the label i in turn. First, thanks to Theorem 3, we have (p, s)

(q,θ) > γ i+1 iff R i (q,θ)
-→ R i+1 ; and if either side of the preceding bi-implication holds, then R i+1 represents γ i+1 , and we have

E i = E i+1 .
Secondly, it follows from Definition 4.3 that γ i

(f ;q) > (f ; q 1 , • • • , q ar (f ) ; s) = γ i+1 iff F a,e p U V n-1 • • • V 0 R i (f ;q) -→ f (F a,e q 1 U V n-1 • • • V 0 ) • • • (F a,e q ar (f ) U V n-1 • • • V 0 ) R i+1 ;
further if either side of the preceding bi-implication holds, and if ar (f ) ≥ 1, then for some 1 ≤ j ≤ ar (f ), we have

(f ; q 1 , • • • , q ar (f ) ; s) (f ;j) > (q j , s) = γ i+2 and R i+2 = F a,e q j U V n-1 • • • V 0 represents γ i+2 , with E i+2 = E i+1 [f (F a,e q 1 U V n-1 • • • V 0 ) • • • [-] • • • (F a,e q ar (f ) U V n-1 • • • V 0 )]
as required; and this concludes the proof.

From recursion schemes to CPDA

The previous section demonstrates that higher-order recursion schemes are at least as expressive as CPDAs. In this section we shall sketch a proof of the converse. Hence, CPDAs and recursion schemes are in fact equiexpressive. A number of related results can be found in the literature, but an exact correspondence with general recursion schemes has never been proved before. Notably, in order to establish a correspondence between recursion schemes and HOPDAs, Damm and Goerdt (for word languages [8, 9]) as well as Knapik, Niwiński and Urzyczyn (for labelled trees [15]), have had to impose constraints on the shape of the former (called derived types and safety respectively) and their translation techniques relied on the restrictions in a crucial way.

Our translation from recursion schemes to CPDA is novel: we transform an arbitrary order-n recursion scheme G to an order-n collapsible pushdown automaton A G that computes the traversals over the computation tree λ(G) (in the sense of Ong [20, 21]). The game-semantic interpretation of G is an innocent strategy (in the sense of Hyland and Ong [13]), which coincides with the value tree [[ G ]] of G, so that paths in the value tree are plays of the strategy. Traversals over the computation tree are just (appropriate representations of) uncoverings [13] of paths in the value tree.

CPDA(G) -the CPDA determined by a recursion scheme G

Fix an order-n recursion scheme G and the HORS graph

Gr(G) = V, E ⊆ V × V, λ G : V -→ Λ G , v 0 ∈ V
determined by it. Note that G is not assumed to be homogeneously typed, and hence, not necessarily safe. We shall construct an order-n collapsible pushdown automaton, written CPDA(G), that computes traversals over the computation tree λ(G). Thus it is an automaton that computes the innocent strategy [[ G ]] given by the value tree of G. (Traversals and computation trees are introduced in Ong's preprint [20, 21].)

Remark 5.1 For convenience, in the definition of the transform CPDA(G), we shall write push a,1 1 as push a 1 , effectively ignoring the 1-link (to the preceding stack symbol). This is harmless since 1-links are guaranteed not to feature in any of collapse operations in of the transform CPDA(G). Definition 5. 2 The transform CPDA(G) is an n-CPDA that has the set V of nodes as the stack alphabet. The initial configuration is the n-stack

[ • • • [⊥ v 0 ] • • • ] i.e. push v 0 1 ⊥ n
, where v 0 is the root of Gr(G). Let u range over the stack symbols of CPDA(G). For ease of explanation, we define the transition map δ as a function that takes a node u ∈ V to a sequence of stack operations, by a case analysis of the label (from Λ G ) of u. The definition is presented in Figure 2. In the Figure (andhenceforth), we shall write push a 1 for push a,1

1
for simplicity.

If u's label is not a variable, the action is just a push v 1 , where v is an appropriate child of the node u. Precisely:

(A) If the label is an @ then δ(u) = push E 0 (u) 1 . (S) If the label is a Σ-symbol f then δ(u) = push E i (u) 1
, where 1 ≤ i ≤ ar (f ) is the direction requested by the Environment, or Opponent.

Note that if f is nullary, the automaton terminates (since Opponent has no move to make).

(L) If the label is a lambda then δ(u) = push

E 1 (u) 1 .
Suppose u is labelled by a variable which is the i-parameter of the lambda node binder(u); and suppose binder(u) is a j-child. Let p be the span of the variable node u.

(V 1 )
If the variable has order l ≥ 1, then δ(u) = push n-l+1 ; pop p+1

1

; push

E i (top 1 ),n-l+1 1 if j = 0 push n-l+1 ; pop p 1 ; collapse ; push E i (top 1 ),n-l+1 1 otherwise
where pop p 1 means the operation pop 1 iterated p times, and push

E i (top 1 ),k 1
is defined to be the operation s → push

E i (top 1 s),k 1 s.
(V 0 ) Otherwise (i.e. the variable has order 0)

δ(u) = pop p+1 1
; push

E i (top 1 ) 1 if j = 0 pop p 1 ; collapse ; push E i (top 1 ) 1
otherwise.

Figure 2: Definition of the transform CPDA(G).

Let s and s range over configurations (i.e. n-stack contents) of CPDA(G). We define a binary relation → over configurations: we say that s → s just if s = δ(top 1 s)(s). We write → * for the reflexive, transitive closure of →.

Remark 5.3

(i) The definition of CPDA(G) as presented is not formally an instance of a CPDA: the transition function maps stack symbols to composites of stack actions, based on a case analysis. However it can be transformed to a proper CPDA, and in general the equivalent CPDA has more than one control states.

(ii) The transformation is radically different from the compilation method of Knapik et al. [15, 16]. To date, it is not known whether the approach in [16] is extendable to non-homogeneously typed recursion schemes of order 2. More generally, it is not known whether the method is extendable to arbitrary recursion schemes of all finite orders.

Question. Are order-n CPDA equi-expressive (for generating trees) with order-(n + 1) PDA?

How does CPDA(G) work?

The transform CPDA(G) computes traversals over the computation tree λ(G). Take a computation sequence of traversals [START_REF] Hyland | On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model[END_REF] :

t 1 > t 2 > t 3 > • • •
starting from the singleton traversal t 1 consisting of the root of the graph Gr(G) (so that for each i, the traversal t i+1 extends t i by one node). Let

s 1 → s 2 → s 3 → • • •
be the corresponding computation sequence of CPDA(G) starting from the initial configuration s 1 .

The two computation sequences are closely related in a lock-step fashion. First we shall see that for each i ≥ 1, the top 1-stack of s i (regarded as a sequence of nodes) is the P-view of t i i.e.

top 2 s i = t i .
Secondly we construct a kind of approximant of t i , written t i , which is obtained from t i by removing all segments w sandwiched between matching pairs of the shape

$ w λ i } }
where $ is either an order-1 variable or an @-symbol, and i ≥ 1. Note that by definition of traversal, the segment w necessarily has the shape

λϕ • • • x i y y
where x is an order-0 variable symbol and ϕ is a list of variables in which x occurs. We then transform each n-stack s i to a sequence of nodes s i , which will be shown to coincide with t i .

How to construct the sequence s i from an n-stack s i ?

We follow a simple recipe.

1. We "flatten" the n-stack s i so that it has the form of a well-bracketed sequence such as the following (top of stack is the right-hand end)

[[[ • • • ] • • • [ • • • ]][[ • • • ]] • • • [[ • • • ][ • • • ]]]
2. The target of any pointer to a stack is deemed to be the rightmost symbol representing the stack, i.e. it is always an occurrence of ].

3. The required subsequence -which we shall write as s i -is obtained by a right-to-left scan of the wellbracketed sequence above according to the following rules.

• When an occurrence of ] is encountered, we simply continue the scan without recording ].

• We record any stack symbols that are being scanned.

• Whenever we encounter the source of a link, the scan jumps to its target (an occurrence of ]) without recording any nodes sandwiched in-between. The source of the link is always recorded. • The scan ends when the first [ is hit.

Note that the last condition is necessary to ensure that s is suitably defined for any prefix of a reachable stack. This will be important in the proof of Proposition 7.

Here is a more formal definition. Definition 5. 4 Let s be an n-stack. The sequence s of stack symbols is defined as follows.

s =        ε top 2 s = [ ],
(pop 1 s) u top 1 s = u and u does not have a link, (collapse s) u top 1 s = u and u has a link.

Examples

We illustrate the workings of CPDA(G) by examples and point out the correspondence between runs of the automaton and the traversals it computes.

Example 5.5 Take the following traversal over the computation tree of G in Example 3.2:

@ λz 0 Ð Ð @ λϕ 0 Ð Ð ϕ 1 λy 1 { { g λ 2 Ó Ó y 1 { { λ 1 { { ϕ 1 x x λy 1 x x g λ 1 ~z 1 v v λ 1 v v a
We give a run of the corresponding 2-CPDA that computes the above traversal in Figure 3.

To save space, we only present the interesting configurations in which the top 1 -element of the stack is a variable node. In the picture, the top of a stack is at the right-hand end, and links are represented by dotted arrows. Set t to be the prefix of the above traversal that ends in the node labelled by z. We have

t = @ λz @ λϕ ϕ λ ϕ λy g λ z
which coincides with the 2-stack s (see Figure 3) by following the recipe. For ease of reference, we give nodes numeric names, which are indicated (within square-brackets) as superscripts. Take the traversal t in Figure 4.

[[@ λz @ λϕ ϕ]] → [[@ λz @ λϕ ϕ] [@ λz @ λy]] w w → * [[@ λz @ λϕ ϕ] [@ λz @ λy w w g λ y]] → [[@ λz @ λϕ ϕ λ]] → [[@ λz @ λϕ ϕ λ ϕ]] → [[@ λz @ λϕ ϕ λ ϕ] [@ λz @ λy]] v v → * [[@ λz @ λϕ ϕ λ ϕ] [@ λz @ λy v v g λ z]] s → [[@ λz @ λϕ ϕ λ ϕ] [@ λ]] → [[@ λz @ λϕ ϕ λ ϕ] [@ λ a]]
0 1 2 9 ~10 11 12 × × 3 Õ Õ 4 Ó Ó 9 Ò Ò 10 11 ~12 { { 5 z z 6 z z 13 y y 14 } } 3 | | 4 | | 9 | | 10 11 ~12 { { 5 z z 6 z z 15 y y 16 v v 17 v v
@ [0] i i i i i i i i i i Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z Z
λΨ [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] λϕz [START_REF] Damm | An automata-theoretical characterization of the OI-hierarchy[END_REF] Ψ [START_REF] Aehlig | Safety is not a restriction at level 2 for string languages[END_REF] p p p p p J J J J

f [START_REF] Miranda | Structures generated by higher-order grammars and the safety constraint[END_REF] s s s s

H H H H λx 1 x 2 [3]
λ [START_REF] Maslov | The hierarchy of indexed languages of an arbitrary level[END_REF] λ [START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF] λ Ψ [START_REF] Carayol | The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata[END_REF] n n n n n

N N N N N N ϕ [12] v v v v K K K K K λx 1 x 2 [5]
λ [START_REF] Courcelle | The monadic second-order logic of graphs IX: machines and their behaviours[END_REF] λ [START_REF] Hyland | On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model[END_REF] λ

x 1 [6] x 2 [8] ϕ [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF] t t t J J J J J λ [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF] λ z [START_REF] Knapik | Unsafe grammars and panic automata[END_REF] Figure 5: An example of an order-3 HORS graph.

We present a run of the 3-CPDA that computes the traversal t in Figure 6 followed by Figure 7 and Figure 8 (for ease of reading, we represent nodes by their labels).

To see the correspondence with the traversal t, note that configurations s 2 and s 3 in Figures 7 and8 respectively have the same top 1 -element which is node 6 (labelled by x 1 ). They correspond respectively to the two prefixes of t that end in node 6.

The traversal t corresponding to s 3 is the prefix of t that ends in the later occurrence of 6; we have

t = @ λΨ Ψ λϕz f λ ϕ λ ϕ λx 1 x 2 Ψ λϕz f λ ϕ λx 1 x 2 x 1
The reader might wish to check that t = s 3 . (Note that the justification pointers are uniquely reconstructible from the underlying sequence of nodes and their respective labels.)

Correctness of the transform

In this section we first set out (in Proposition 7), given any order-n recursion scheme G, the way in which the reachable configurations of the transform CPDA(G)

s 1 → s 2 → • • • → s n → • • •
can be said to compute traverals over the computation tree λ(G) (i.e. the Λ G -labelled tree obtained from Gr(G) by unfolding)

t 1 > t 2 > • • • > t n > • • •
in a lock-step fashion. It then follows (from the Correspondence Theorem in [21]) that CPDA(G) computes (all paths in) the Σ-labelled tree [[ G ]] generated by G.

Lemma 6

Let s be a reachable configuration of an n-CPDA, and let u be an occurrence of a stack symbol in s. Suppose u has a link to an i-stack σ. Then for every i < j ≤ n, the i-stack σ is contained in the same j-stack in which u occurs.

Proof Since the property is preserved by every n-CPDA instruction, the Lemma follows by induction on the number of instructions it takes to obtain s from the initial configuration.

For example, the following 3-stack is not reachable: b has a link to the 1-stack [ c ], but the source (i.e. b) and the target (i.e. [ c ]) of the link are not in the same 2-stack

[ [ [ c ] ] [ [ a ] [ b y y ] ] ]
Definition 5.7 Let G be an order-n recursion scheme, let s be a reachable configuration of CPDA(G), and let t be a traversal over λ(G). We shall say that s computes t if and only if the following conditions hold.

(a) top 2 (s) = t . (b) s = t. (c) Suppose top 2 (s) = [v 1 , • • • , v n ]. Let v 1 , • • • , v n be the respective occurrences of v 1 , • • • , v n in t that contribute to t . Then pop n-i 1 (s) computes t ≤v i for any 1 ≤ i < n.
(d) Using the same notation as in (c), suppose v i has a link to an l-stack σ. Let s σ be the prefix of s such that σ is its top l-stack, i.e. Note that the definition is not circular, since

s σ = collapse(pop n-i [[@ λΨ Ψ]] → [[@ λΨ Ψ] [@ λϕz]] z z → * [[@ λΨ Ψ] [@ λϕz | | f λ ϕ]] →    [[@ λΨ Ψ λx 1 x 2 ]] @ @ [[@ λΨ Ψ] [@ λϕz x x f λ ϕ]]    →    [[@ λΨ Ψ λx 1 x 2 9 9 Ψ]] [[@ λΨ Ψ] [@ λϕz y y f λ ϕ]]    →    [[@ λΨ Ψ λx 1 x 2 A A Ψ] [@ λϕz]] z z [[@ λΨ Ψ] [@ λϕz y y f λ ϕ]]    → *    [[@ λΨ Ψ λx 1 x 2 A A Ψ] [@ λϕz { { f λ ϕ]] [[@ λΨ Ψ] [@ λϕz y y f λ ϕ]]    →        [[@ λΨ Ψ λx 1 x 2 9 9 Ψ λx 1 x 2 ]] @ @ [[@ λΨ Ψ λx 1 x 2 B B Ψ] [@ λϕz x x f λ ϕ]] [[@ λΨ Ψ] [@ λϕz y y f λ ϕ]]        → Figure 6: A run of a 3-CPDA (Part 1 of 3). →        [[@ λΨ Ψ λx 1 x 2 8 8 Ψ λx 1 x 2 @ @ x 1 ]] [[@ λΨ Ψ λx 1 x 2 A A Ψ] [@ λϕz y y f λ ϕ]] [[@ λΨ Ψ] [@ λϕz y y f λ ϕ]]        s 2 → [[@ λΨ Ψ] [@ λϕz | | f λ ϕ λ]] → [[@ λΨ Ψ] [@ λϕz | | f λ ϕ λ ϕ]] →    [[@ λΨ Ψ λx 1 x 2 ]] A A [[@ λΨ Ψ] [@ λϕz x x f λ ϕ λ ϕ ]]    →    [[@ λΨ Ψ λx 1 x 2 @ @ Ψ]] [[@ λΨ Ψ] [@ λϕz y y f λ ϕ λ ϕ ]]    →    [[@ λΨ Ψ λx 1 x 2 B B Ψ] [@ λϕz]] z z [[@ λΨ Ψ] [@ λϕz y y f λ ϕ λ ϕ ]]    → *    [[@ λΨ Ψ λx 1 x 2 B B Ψ] [@ λϕz { { f λ ϕ]] [[@ λΨ Ψ] [@ λϕz y y f λ ϕ λ ϕ ]]    →        [[@ λΨ Ψ λx 1 x 2 @ @ Ψ λx 1 x 2 ]] @ @ [[@ λΨ Ψ λx 1 x 2 B B Ψ] [@ λϕz x x f λ ϕ]] [[@ λΨ Ψ] [@ λϕz y y f λ ϕ λ ϕ ]]        → Figure 7: A run of a 3-CPDA (Part 2 of 3). →        [[@ λΨ Ψ λx 1 x 2 @ @ Ψ λx 1 x 2 9 9 x 1 ]] [[@ λΨ Ψ λx 1 x 2 B B Ψ] [@ λϕz y y f λ ϕ]] [[@ λΨ Ψ] [@ λϕz y y f λ ϕ λ ϕ ]]        s 3 → [[@ λΨ Ψ] [@ λϕz | | f λ ϕ λ ϕ λ ]] → [[@ λΨ Ψ] [@ λϕz | | f λ ϕ λ ϕ λ z ]] → [[@ λΨ Ψ λ ]]
t ≤v i (1 ≤ i < n) and t <v i (1 ≤ i ≤ n) are strictly shorter than t.
In what follows we shall blur the distinction between v i and its occurrence v i , as it will be clear from the context which occurrence is meant.

Proposition 7

Let G be an order-n recursion scheme and let s be a reachable configuration of CPDA(G).

(i) Let u be a node of λ(G). Then u has a link in s if and only if it is a j-child (j > 0) labelled by a lambda of type A which has order l ≥ 1. Further, if u has a link, it points to an (nl)-stack.

(ii) There exists a traversal t over λ(G) such that s computes t.

Proof We prove the Proposition by induction on the number of →-steps s is from the initial configuration. Clearly, the above assertions are valid when s is the initial configuration.

For the inductive cases, suppose s → s . Assuming that (i) holds for s, (ii) holds for s and t, we shall prove that (i) holds for s and (ii) holds for s and t , where t is a suitable one-node extension of t. We shall do so by a case analysis of the label of top 1 (s) = u.

First suppose u's label is not a variable. Then s = push v 1 s, for an appropriate node v. In particular, no new link is created. For (i), observe that, because u's label is not a variable, it follows from the structure of λ(G) that if v was a j-child (j > 0) labelled by a lambda of type A, then u would have to be a Σ-symbol and, consequently, A would have order 0. Thus, (i) still holds, because no new links have been created. For (ii), let t = tv, where v has a pointer to a suitable node (there is only one way in which a pointer from v can be inserted so as to make t into a traversal). Then we have t > t . We shall show that s computes t .

For (a) we need to check that top 2 s = t . We have top 2 s = (top 2 s)v and, in all three cases corresponding to the rules (A), (S), (L), t = t v holds. Thus, by induction hypothesis, we get top 2 s = t . For (b) we note that s = sv and t = tv. So, by induction hypothesis, s = t . (c) follows immediately from the induction hypothesis and, because no new links have been created, so does (d).

Next suppose u's label is an order-l variable, which is the i-parameter of binder(u) (note that then we have i ≥ 1) and suppose binder(u) is a j-child. Then s = δ(u)s where δ(u) is given in Definition 5.2. There are four cases; in the following we shall use the notations from the Definition.

1. Case l ≥ 1 and j = 0. Suppose u's label is the order-l variable ϕ i .

By the induction hypothesis of (ii), u must be the last node of t. It then follows from the definition of a traversal that t has the following shape:

t = • • • u 0 u 1 0 Ø Ø • • • u i Ñ Ñ @ λϕ ϕ i
(in the figure, the label of a node is the symbol just below it). Since the P-view of a traversal is a path in the HORS graph, t has the shape

• • • u 0 u 1 • • • u θ
and the segment θ has length p + 1, where p is the span of the variable node u.

Consider the operation δ(u) = push n-l+1 ; pop p+1 1 ; push

E i (top 1 ),n-l+1 1
. By the induction hypothesis of (ii), the top 1-stack of s -call it σ -is the P-view of t. Since the top 1-stack of push n-l+1 s is a copy of σ, applying pop p+1 1 to push n-l+1 s returns a stack that has the @-labelled node u 0 as the top 1 -element. The node that is push 1 ed onto the top of the stack at this point is the i-child of u 0 , which we call v. Further, it has a link to the top (nl)-stack of the prefix s of s .

It follows from the structure of λ(G) that v must be labelled by λψ (say) of the same type as the label ϕ i of u, i.e. its type is also of order l ≥ 1. Thus, since i ≥ 1, (i) follows as required.

For (ii) set t = tv, where v has a pointer (labelled by i) to the occurrence of u 0 indicated in the figure above. Then t is a traversal and we have t > t . We shall show that s computes t . (c) Because the top 1-stack of s is (a copy of) a prefix of top 2 s extended with v, we can simply appeal to the induction hypothesis (c).

(d) For the same reason as above, (d) holds for all links in top 2 s except (possibly) the single new link. Let σ be the (nl)-stack pointed at from v. Then we have s σ = s. Because t = t <v and s computes t, (d) also holds for the new link.

2. Case l ≥ 1 and j > 0. Suppose the label of u is the order-l variable ϕ i , which is the ith item of the list ϕ.

By induction hypothesis (ii) and definition of a traversal, t has the following shape:

t = • • • u 0 u 1 • • • u i Ñ Ñ Ψ λϕ ϕ i
Further, the variable ψ has the same type as λϕ, which (say) is of order l . It follows that l > l and, consequently, l ≥ 1. By induction hypotheses (i) and (ii), s has the following shape

s = [ • • • • • • • • • [ • • • σ • • • [ • • • u 1 • • • u] top 1-stack of s ] top (n -l)-stack of s • • • ]
wherein u 1 has a link to some (nl )-stack σ. Since l > l, the (nl )-stack σ is embedded in the top (nl)-stack of s (Lemma 6), as indicated by the figure above. Note that, by induction hypothesis (iid), s σ computes t <u 1 . In particular the top 1 -element of σ must be u 0 . Now, to see the structure of s , consider the operation δ(u). Let w = top n-l+1 s. The operation push n-l+1 s pushes a copy of w on top of s. The rest of δ(u), namely, pop p 1 ; collapse; push

E i (top 1 ),n-l+1 1
, affects only the top (duplicate) copy of w. Applying pop p 1 to push n-l+1 s returns a stack that has u 1 as the top 1element; the collapse-operation then reduces it to a stack that has a copy σ (say) of σ as its top (nl )-stack, i.e. its top 1 -element is u 0 . The node that is push 1 ed onto the top of the stack at the end of the δ(u)-operation (to yield s ) is the i-child of u 0 , which we shall call v. Observe that the structure of λ(G) implies that v must then be labelled by λχ (say) whose type is the same as that of ϕ i , i.e. its order is l. Since v is linked to the (nl)-stack w, (i) is satisfied.

For (ii) let t = tv, where v has an i-pointer to the distinguished occurrence of u 0 . t is then a traversal such that t > t . We need to show that s computes t .

(a) Observe that t = t <u 0 u 0 v = t <u 1 v. Since s σ computes t <u 1 , so does s σ . Hence,

top 2 s = t <u 1 v = t .
(b) Observe that s = sv and t = tv. Thus, by induction hypothesis, s = t .

(c) Since s σ computes t <u 1 , (c) holds.

(d) We only need to verify (d) for the new link (all other links satisfy (d) because s σ computes t <u 1 ). Recall that v points at the stack w. Since s w = s and t <v = t, (d) holds because s computes t.

3. Case l = 0 and j = 0. Suppose u's label is the order-0 variable x.

By induction hypothesis (ii) and the definition of a traversal, t must have the following shape:

t = • • • u 0 u 1 0 Ø Ø • • • u i Ñ Ñ

@ λϕ x

As in 1., t has the shape

• • • u 0 u 1 • • • u θ
and the segment θ has length p + 1, where p is the span of the variable node u.

Consider the operation δ(u) = pop p+1 1 ; push

E i (top 1 ) 1
. Applying pop p+1 1 to s returns a stack that has the @-labelled node u 0 as the top 1 -element. The node that is push 1 ed onto the top of the stack at this point is the i-child of u 0 , which we call v. It follows from the structure of λ(G) that v must be labelled by λ, i.e. its type has order 0. Thus, since v has no link, (i) follows as required.

For (ii) set t = tv, where v has a pointer (labelled by i) to the occurrence of u 0 indicated above. Then t is a traversal and we have t > t . We shall show that s computes t .

(a) We need to show top 2 s = t . By definition of s , we have top 2 s = (top 2 s) ≤u 0 v. By induction hypothesis (ii), we have top 2 s = t . Thus

top 2 s = t ≤u 0 v = t ≤u 0 v = t
as required (the second equation holds because u 0 appears in t ).

(b) We have s = (pop p+1 1 s) v and t = t ≤u 0 v. By induction hypothesis (iic), pop p+1 1 s computes t ≤u 0 , in particular pop p+1 1 s = t ≤u 0 . Thus, (b) holds.

(c) We simply appeal to the induction hypothesis (iic).

(d) Note that no new links have been created in this case, so it suffices to appeal to the induction hypothesis (iid).

4. Case l = 0 and j > 0. Suppose the label of u is the order-0 variable x, which is the ith item of the list ϕ.

By induction hypothesis (ii) and definition of a traversal, t has the following shape:

t = • • • u 0 u 1 • • • u i Ñ Ñ ψ λϕ x
Further, the variable Ψ has the same type as λϕ, which (say) is of order l . It follows that l > l. By induction hypotheses (i) and (ii), s has the following shape

s = [ • • • • • • σ • • • [ • • • u 1 • • • u] top 1-stack • • • ]
wherein u 1 has a link to some (nl )-stack σ. Note that, by induction hypothesis (iid), s σ computes t <u 1 . In particular the top 1 -element of σ must be u 0 . Now, to understand what s looks like, consider the operation δ(u) = pop p 1 ; collapse; push

E i (top 1 ) 1
. Applying pop p 1 to s returns a stack that has u 1 as the top 1 -element; the collapse-operation then reduces it to a stack that has σ as its top (nl )-stack, i.e. its top 1 -element is u 0 . The node that is then push 1 ed onto the top of the stack at the end of the δ(u)-operation (to yield s ) is the i-child of u 0 , which we shall call v. Observe that the structure of λ(G) implies that v must then be labelled by λ. Since v does not have a link, (i) is satisfied.

For (ii) let t = tv, where v has an i-pointer to the distinguished occurrence of u 0 . t is then a traversal such that t > t . We need to show that s computes t .

(a) Observe that t = t <u 1 v. Since s σ computes t <u 1 , we have top 2 s = t <u 1 v = t .

(b) Observe that s = s σ v and t = t <u 1 v. Again, since s σ computes t <u 1 , we have s σ = t <u 1 and (b) follows.

(c) Because s σ computes t <u 1 , (c) holds.

(d) Again, it suffices to appeal to the fact that s σ computes t <u 1 , because no new links have been created.

Note that in the above proof t was constructed from s in a lock-step fashion. Moreover, observe that, when the last node of a traversal is not a Σ-symbol, traversals (as well as the corresponding runs of CPDA(G)) can be extended in a unique way. Similarly, when the last node of a traversal is a Σ-symbol f , both traversals and the corresponding runs of CPDA(G) can be extended in ar (f ) matching ways. Consequently, we have: Corollary 8 Suppose s computes t. Then s and t are "bisimilar" with regard to → and > respectively:

(i) If s → s then there exists t such that t > t and s computes t .

(ii) If t > t then there exists s such that s → s and s computes t .

Theorem 9 (Equi-Expressivity 2) For every order-n recursion scheme G, CPDA(G) computes all paths in the value tree [[ G ]] generated by G.

Games over collapsible pushdown graphs

We are interested in solving parity games over collapsible pushdown graphs i.e. we want to know whether one can decide, for any position in such a game, if Éloïse has a winning strategy from it, and if so, determine its complexity. An order-n collapsible pushdown system [START_REF] Knapik | Deciding monadic theories of hyperalgebraic trees[END_REF] (n-CPDS) is given by a quadruple A = Γ, Q, ∆, q 0 where Γ is the stack alphabet, Q is a finite state-set, ∆ ⊆ Q × Γ × Q × Op n is the transition relation, and q 0 is the initial state. Configurations of an n-CPDS are pairs of the form (q, s) where q ∈ Q and s is an n-stack over Γ. We define a one-step labelled transition relation of the CPDS A, written > where ∈ Q × Op n , which is a family of binary relations over configurations, as follows: (q, s)

(q ,θ)
> (q , s ) just if we have (q, top 1 s, q , θ) ∈ ∆ and s = θ(s). The initial configuration is (q 0 , ⊥ n ). We can now define the configuration graph of A: vertices are just the (reachable) configurations, and the edge relation is the relation > restricted to the reachable configurations. wheremeans any symbol, † means any non-⊥ symbol, and t, a, b, 0 and 1 are shorthand for the stack operations push 2 , push a,2 1 , push b,2 1 , collapse and pop 1 respectively. We present its configuration graph (with edges labelled by stack operations only) as follows:

0[[]] t G G 1[[][]] a G G b 0[[][a]] t G G 1[[][a][a]] a G G b 0[[][a][a a]] t G G 1[[][a][a a][a a]] • • • b 2[[][b]] 1 0 g g P P P P P P 2[[][a][a b]] 1 0 i i T T T T T T T T 2[[][a][a a][a a b]] • • • 1 0 k k X X X X X X X X X X X X 2[[][]] 2[[][a][a]] 1 0 k k V V V V V V V V V V V V V V V V V V V V V V V V V V V V V V V V 2[[][a][a a][a a]] • • • 1 0 l l YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY Y 2[[][a][]] 2[[][a][a a][a]] • • • 1 0 l l YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY YY 2[[][a][a a][]]
14 We use collapsible pushdown system (as opposed to automaton) whenever the device is used to generate a graph. [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF] This is inspired by an example in [6].

Let G = V, E denote the configuration graph of A, let Q E ∪Q A be a partition of Q and let Ω : Q -→ C ⊂ N be a colouring function. Altogether they define a partition V E ∪ 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 = G, V E , V A is an n-CPDS game graph and the pair G = G, Ω is an n-CPDS parity game. A play in G from the initial vertex v 0 = (q 0 , ⊥ n ) is defined as follow: the player that controls v 0 ( Éloïse if v 0 ∈ V E or Abelard otherwise) moves a token from v 0 to some neighbour v 1 (we assume here that G has no dead-end), then the player that controls the token moves it to a neighbour v 2 of v 1 and so on.

A play is therefore an infinite path v 0 v 1 • • • and is won by Éloïse iff lim inf Ω(v i ) : i ≥ 0 is even. Finally, v 0 is winning for a player if he has a winning strategy from it. See [25, 28, 27] for more details.

In this section we consider the following problem:

(P 1 ) Given an n-CPDS parity game decide if Éloïse has a winning strategy from the initial configuration.

From the well-known techniques of [11], it follows that (i) Problem (P 1 ) is polynomially equivalent to Problems (P 2 ) and (P 3 ) in the following; and (ii) Problem (P 1 ) is equivalent to Problem (P 4 ) -the reduction from (P 1 ) to (P 4 ) is polynomial, but non-elementary one in the other direction :

(P 2 )
Given an n-CPDS graph G, and a mu-calculus formula ϕ, does ϕ hold at the initial configuration of G? (P 3 ) Given an alternating parity tree automaton and n-CPDS graph G, does it accept the unravelling of G?

(P 4 ) Given an MSO formula ϕ and an n-CPDS graph G, does ϕ holds at the root of the unravelling of G?

An useful fact is that the unravelling of an n-CPDS graph is actually generated by an n-CPDA (one mainly has to note that putting labels on the edges makes the n-CPDS graph deterministic and hence its unravelling as desired).

Lemma 10 Let A = Γ, Q, ∆, q 0 be some n-CPDS and let G be its configuration graph. Then let t be the tree obtained by unravelling G and by labeling every node by control state and top 1 stack element of the corresponding configuration in G. Then t is generated by an n-CPDA of polynomial size in the one of A.

Proof Consider the following n-CPDA A = Σ, Γ, Q , δ, q 0 where we set:

• T rans = {(q, θ) | ∃p ∈ Q, a ∈ Γ s.t.
(p, a, q, θ) ∈ ∆} is the set of all transitions that can be applied in A.

• Q = Q ∪ T rans • Σ = Q × Γ
is the set of shapes (here are do not care of the link) and the arity of (q, a) ∈ Σ is |{(q , θ) | (q, a, q , θ) ∈ ∆}|.

• For every q ∈ Q, and every a ∈ Γ, δ(q, a) = ((q, a);

(q 1 , θ 1 ), • • • , (q k , θ k )) where {(q 1 , θ 1 ), • • • , (q k , θ k )} = {(q , θ) | (q, a, q , θ) ∈ ∆}.
• For every (q, θ) ∈ T rans, and every a ∈ Γ, δ((q, θ), a) = (q, θ).

Then one easily checks that A generates t.

The section is organized as follows. We start by giving a general overview of the proof. Then we prove a technical result (Lemma 14) which allows to restrict our attention to a specific class of n-CPDS (collapse rank-aware CPDS). For this class, we provide a reduction of an n-CPDS game to an (n -1)-CPDS games, which allows to conclude using an inductive argument.

Overview of the proof and preliminaries

We follow the general approach of [26] and [16]. In [26], in order to solve a pushdown parity game, one builds a simulation game that is played on a finite game graph and is equipped with a parity condition. Then one proves that a configuration in the pushdown game is winning for Éloïse iff a corresponding configuration is winning for her in the simulation game. Moreover from a winning strategy in the simulation game, one can built a winning strategy in the pushdown game. The increase of memory results in the use of a stack. In [16] the authors consider parity games on 2-CPDS [START_REF] Knapik | Unsafe grammars and panic automata[END_REF] and mostly adapt the construction of [26]. To handle the collapse actions, they need to make the CPDS rank aware. Assume that the play is in some configuration v where collapse may be applied. Applying collapse leads to some configuration v , and the stack content in v has already appeared before v in the play. The collapse ancestor of v is the latest configuration in the play with this stack content. A CPDS is rank aware (to be defined formally) if the top stack symbol contains the collapse rank which is the minimal rank of a state occurring between the collapse ancestor of the current configuration and the current configuration. Now solving a 2-CPDS game when the 2-CPDS is rank aware, can be done by adapting the reduction in [26] (now the simulation game is no longer played on a finite graph but can still be solved). Let us mention an important point here. In [16], the authors proves the following: if one player win the 2-CPDS game then he wins the simulation game. Hence this proves the equivalence of both games but do not provide a way to build a strategy in the 2-CPDS game.

Here, we extend the result of [16] to n-CPDS parity game for any n. Moreover, from our proof, we can effectively build winning strategies in the n-CPDS game. The proof works by induction on n. Note that the special case where n = 1 is the one of parity pushdown game studied in [26].

What follows do not rely on a specific representation of the links and therefore we do not make it more precise.

We start with some definitions adapted from the one introduced in [16]. Definition 6.2 Consider a partial play Λ in G ending in a configuration (q, s) such that top 1 (s) has an n-link. Hence there is in Λ at least one configuration of the form (q , collapse(s)) for some q ∈ Q. Then the closest to (q, s) is called the collapse ancestor of (q, s). The collapse rank of (q, s) is the minimal colour of a state occurring in Λ between the panic ancestor of (q, s) and (q, s). Note that these notions are not defined if top 1 (s) has an k-link for some k < n: indeed it may happen that no configuration of the form (q , collapse(s)) was visited in Λ, and therefore the collapse ancestor notion can not be adapted. Definition 6.3 An n-CPDS equipped with a colouring function is collapse rank-aware iff there exists a function ColRk : Γ → N such that, when defined, the collapse rank of every configuration (q, s) is equal to ColRk(top 1 (s)). In other words, the collapse rank is stored in the top 1 -element of the stack.

We also introduce a notion of ancestor.

Definition 6.4 Consider a play

Λ = v 1 v 2 • • • in G
and consider that we attach to every k-stack (for any 1 ≤ k ≤ (n -1)) an identifier (which is an integer) as follows: if a push k operation is applied at configuration [START_REF] Knapik | Unsafe grammars and panic automata[END_REF] They use the terminology panic automata instead of collapsible pushdown automata.

v m in Λ, the top (k -1)-stack of configuration v m+1 is assigned identifier m, and all identifiers for the j-stacks for j < (k -1) in this new top (k -1)-stack are copied from the former top (k -1)-stack. Now, for 2 ≤ k ≤ n the k-ancestor of some configuration v in Λ is the configuration v m where m is the identifier of v's top (k -1)stack, and the level rank for k is the minimal colour of a state occurring in Λ between the (k -1)-ancestor of v and v. Example 6. 5 In the following (order-3) example, we assume that the colour of v i is i, and the identifier j of a stack

[ • • • ] is denoted by [ • • • ] j . Starting from v 1 = [[[] 0 ] 0 ], consider the following sequence of stack actions: [[[] 0 ] 0 ] = v 1 push 2 -→ [[[] 0 [] 1 ] 0 ] = v 2 push a,2 1 -→ [[[] 0 [a (2,1) ] 1 ] 0 ] = v 3 push 3 -→ [[[] 0 [a (2,1) ] 1 ] 0 [[] 0 [a (2,1) ] 1 ] 3 ] = v 4 push 2 -→ [[[] 0 [a (2,1) ] 1 ] 0 [[] 0 [a (2,1) ] 1 [a (2,1) ] 4 ] 3 ] = v 5
Then the 2-ancestor of v 5 is v 4 and hence the level rank for 2 of v 5 is 4. The 3-ancestor of v 5 is v 3 and the level rank for 3 of v 5 is therefore 3. The 2 ancestor of v 4 is v 1 and therefore the level rank for 2 of v 4 is 1.

We show, as in [16, Lemma 6.3], that we can restrict our attention to CPDS games where the underlying CPDS is collapse rank-aware.

Lemma 14 For any n-CPDS P and any parity game G on it, one can construct a collapse rank-aware n-CPDS P and an associated parity game G such that Éloïse has a winning strategy in G from some configuration (p in , ⊥ n ) iff she has a winning strategy in G from the same configuration.

Proof

The proof is an non-trivial adaptation of the one of [16, Lemma 6.3] to the general setting of n-CPDS (instead of 2-CPDS).

Fix an n-CPDS

P = Γ, Q, ∆ , a partition Q E ∪ Q A of Q and a colouring function Ω : Q → C ⊂ N.
Denote by G the induced parity game. We define a collapse rank-aware (to be proven) n-CPDS P = Γ , Q , ∆ such that Q ⊂ Q and Γ = Γ × C × C {2,...,n} × C {2,...,n} . A configuration (q, s) of P with its top 1 (s) = (a, m c , τ, τ old ) having a (k + 1)-link will satisfy the following.

• m c is the minimal colour seen since the k-ancestor of the k-stack pointed to by the (k + 1)-link. In particular, when the link is an n-link, equivalently when the collapse rank is defined, m c will be the collapse rank: indeed the (n -1)-stack pointed by the n-link is such that its n-ancestor is exactly the collapse ancestor of the current configuration and hence m c is the smallest colour seen since the collapse ancestor. By abuse of notation, we designate in the sequel m c as the collapse rank.

• τ is the level rank, that is, for any i = 2, • • • , n, τ (i) is the level rank for i.

• τ old is such that τ old (k) = h where h = τ (k) with top 1 (pop k (s)) = (a , m c , τ , τ old ) if exists and otherwise may be any h. In other word τ old (k) gives the level rank for k for the (k -1)-stack just above the current one. Note that τ old is introduced here only for technical reasons and is actually easy to maintain (one has to care only when pushing).

The transition relation of P mimics the one of P and updates the ranks as explained below.

In order to save space and to make the construction more understandable, we do not describe formally ∆ but explain how P is supposed to behave. It should be clear that ∆ can be formally described to fit this informal description (and that some extra control states are needed). Note also that the following description contains also the inductive proof of its validity, namely that m c , τ and τ old are as stated above.

Assume P is in some configuration (q, s) with top 1 (s) = (a, m c , τ, τ old ). The following behaviours are those allowed in such a configuration. 1. For every (q, a, q , pop k ) ∈ ∆ with 1 ≤ k ≤ n, let pop k (s) = s and let top 1 (s ) = (a , m c , τ , τ old ).

Then P can go to the configuration (q , s ) where s is obtained from s by replacing top 1 (s ) by (a , min(m c , τ (k), Ω(q )), τ , τ old ), with

τ (i) = min(τ (i), τ (k), Ω(q )) if i ≤ k min(τ (i), Ω(q )) if i > k
Indeed the play since this move was ending by a sequence (q 1 , s 1 )(q 2 , s 2 ) • • • (q, s) (here the dots are for intermediate configurations that have no importance for the current argument) where (q 2 , s 2 ) is the k-ancestor of (q, s) and was reached from (q 1 , s 1 ) by applying a push k move, and top k (s 1 ) = top k (s ), which in particular means that (q 1 , s 1 ) and (q , s ) have the same i-ancestors for i ≤ k and that top 1 (s 1 ) and top 1 (s ) are equal and point to two respective (h -1)-stacks (for some h) that both have the same hancestor. Hence, the collapse rank in (q , s ) being the smallest colour since the h-ancestor of the pointed (h -1)-stack it is equal to the minimum of the collapse rank in (q 1 , s 1 ) (namely m c ) with Ω(q ) and with the minimal colour visited in (q 2 , s 2 ) • • • (q, s), which is (as (q 2 , s 2 ) is the k-ancestor of (q, s)) equal to τ (k). Hence the collapse rank is min(m c , τ (k), Ω(q )). Now the level rank in (q , s ) for some i ≤ k being the smallest colour seen since the i-ancestor of (q , s ), and this i-ancestor being the same as in (q 1 , s 1 ), the level rank is the minimum of the level rank for i in (q 1 , s 1 ) (namely τ (i)) with Ω(q ) and with the minimal colour visited in (q 2 , s 2 ) • • • (q, s) (namely τ (k)). Hence it is equal to min(τ (i), τ (k), Ω(q )).

The i-ancestor of (q , s ) for some i > k equals the i-ancestor of (q, s), and hence the level rank for i has to be simply updated from the one in (q, s) (namely τ (i)) by taking the minimum with Ω(q ). Finally the τ old information needs not to be updated.

2. For every (q, a, q , push j ) ∈ ∆ with 2 ≤ j ≤ n, let push j (s) = s and then top 1 (s ) = (a, m c , τ, τ old ).

Then P can go to the configuration (q , s ) where s is obtained from s when replacing top 1 (s ) by (a, min(m c , Ω(q )), τ , τ old ) with τ (i) = min(τ (i), Ω(q )) if i = j and τ (j) = Ω(q ), and τ old (i) = τ old (i) if i = j and τ old (j) = τ (j).

Indeed, in the new configuration, the h-ancestor of the (h -1)-stack pointed by top 1 (s ) (for some h) is the same as the h-ancestor of the (h -1)-stack pointed by top 1 (s) and hence the collapse rank simply needs to be updated by taking the minimum of the former one (namely m c ) with the current colour (namely Ω(q )). Now, the i-ancestors for any i = j in (q, s) and (q , s ) are the same and therefore the level rank for i simply needs to be updated by taking the minimum of the former one (namely τ (i)) with the current colour (namely Ω(q )).

The j-ancestor of (q , s ) is (q, s), and hence the level rank for j in (q , s ) equals Ω(q ). Finally, one has top 1 (pop i (s)) = top 1 (pop i (s )) for every i = j and therefore τ old (i) = τ old (i) gives the correct value, and as top 1 (pop j (s )) = (a, m c , τ, τ old ), one must set τ old (j) = τ (j).

3. For every (q, a, q , push b 1,k ) ∈ ∆ with 1 ≤ k ≤ n, and b ∈ (Γ \ {⊥}), then P apply push

(b,m c ,τ ,τ old ) 1,k
where m c = min(τ old (k), τ (k), Ω(q )), τ (i) = min(τ (i), Ω(q )) for every i and τ old (i) = τ old (i) for every i.

In order to define the correct value for m c one needs to consider the minimal colour since the k ancestor of the (k -1)-stack pointed by the new k-link. The play since the last move was ending by a sequence of the form (q 1 , s 1 ) • • • (q 2 , s 2 )(q 3 , s 3 ) • • • (q, s) (here the dots are for intermediate configurations that have no importance for the current argument) where (q 1 , s 1 ) is the k-ancestor of the (k -1) stack pointed by the new link, (q 3 , s 3 ) is the k-ancestor of (q, s) and therefore the move from (q 2 , s 2 ) is a push k one. Moreover it is easily checked that top k (s 2 ) = top k (pop k (s)) and therefore top 1 (s 2 ) = top 1 (pop k (s)).

Hence, τ old (k) is the level rank for k in (q 2 , s 2 ). Now note that the smallest colour visited since (q 3 , s 3 ) is by definition the level rank for k in (q, s) (namely τ (k)) and therefore the correct value for m c is the minimum of the minimum between (q 1 , s 1 ) and (q 2 , s 2 ) with the minimum between (q 3 , s 3 ) and (q, s) and Ω(q ), that is m c = min(τ old (k), τ (k), Ω(q )). Note that here τ old (k) makes sense as if top 1 (pop k (s)) is not defined it would means that pop k (s) would be empty and then push b 1,k is not allowed (there is no (k -1)-stack to target).

Then the i-ancestors for all i in (q, s) and (q , s ) are the same and therefore the level rank for i simply needs to be updated by taking the minimum of the former one (namely τ (i)) with the current colour (namely Ω(q )).

Finally, one has top 1 (pop i (s)) = top 1 (pop i (s )) for every i and therefore τ old (i) = τ old (i) gives the correct value. 4. For every (q, a, q , collapse) ∈ ∆, let collapse(s) = s and let top 1 (s ) = (a , m c , τ , τ old ). Then P can go to the configuration (q , s ) where s is obtained from s by replacing top 1 (s ) by (a , min(m c , m c , Ω(q )), τ , τ old ) with τ (i) = min(τ (i), m c , Ω(q )) for every i.

Indeed the play since the last move (namely collapse) was ending by a sequence of the form (q 1 , s 1 ) • • • (q 2 , s 2 )(q 3 , s 3 ) • • • (q, s) (here the dots are for intermediate configurations that have no importance for the current argument) where (q 1 , s 1 ) is the k-ancestor of the (k -1)-stack pointed by the k-link in the top symbol of (q, s), (q 2 , s 2 ) is such that top k (s 2 ) = top k (s ) and (q 3 , s 3 ) is reached from (q 2 , s 2 ) by a push k move. Consider the i ancestor for (q , s ): it is the same than the one in (q 2 , s 2 ) and therefore the minimum colour seen since the i-ancestor is the minimum colour of the one seen since the i-ancestor in (q 2 , s 2 ) (namely τ (i)) of the minimum colour visited since (q 3 , s 3 ) and of Ω(q ). As m c is the minimum colour since (q 1 , s 1 ) and as the i-ancestor of (q , s ) must appear before (q 1 , s 1 ) the previous minimum is the same as min(τ (i), m c , Ω(q )).

Using exactly the same arguments, one deduces that the collapse rank in (q , s ) equals min(m c , m c , Ω(q )).

Finally the τ old information needs not to be updated.

From the previous description (and the included inductive proof) we conclude that P is collapse rankaware. Now, in order to conclude the proof of Lemma 14, one considers the parity game G on P defined using the same partition as the from Q (the control state of Q \ Q inducing configurations with exactly one successor can be controlled by any player), and extending Ω to Q by assigning the maximal colour to states in Q \ Q (hence not modifying the winner). For this game, it should then be clear that we have the desired property. Remark 6.6 Note that building a collapse rank-aware n-CPDS from a non-aware one increases the stack alphabet by C 2n+1 and the state set by C n (recall that we need extra states, that where hidden in the previous description, mainly to store τ )

Main reduction

In order to solve CPDS parity games, we give a reduction that built from an n-CPDS parity game G an equivalent (n -1)-CPDS parity game G. By equivalent we mean the following.

1. A configuration (p in , ⊥ n ) is winning for Éloïse in G iff (p in , ⊥ n-1
) is winning for Éloïse in G, where p in depends on p in (and can be easily constructed);

2. From a winning strategy for Éloïse from (p in , ⊥ n ) in G, one can deduce a strategy for her in G from (p in , ⊥ n-1 );

3. From a winning strategy for Éloïse from (p in , ⊥ n-1 ) in G, one can effectively construct a strategy for her in G from (p in , ⊥ n );

Note the last two points implies the first one, and our proof will actually establish these two points. Also note that we get a similar statement for Abelard, by considering the game defined by the colouring function Ω where we set Ω (v) = Ω(v) + 1 for every state vertex v in the game graph. Also note that the last point is effective. Hence, applying inductively the reduction will give an effective construction of strategies for both players in an n-CPDS game. This was not the case in the proof for 2-CPDS game in [16].

The reduction we present below (i.e. the description of G) can be though as a generalization of those presented in [26] and in [16]. The proof generalizes the one in [26] and partially (for the easy implication) the one in [16].

From now on we fix a collapse rank-aware n-CPDS

P = Γ, Q, ∆ , a partition Q E ∪ Q A of Q and a colouring function Ω : Q → C = {0, .
. . , d}. The mapping computing the collapse rank is denoted ColRk. By G, we denote the implied parity game, and we fix an initial configuration (p in , ⊥ n ).

For a configuration v = (q, s) of P, we define its stack height sh(v) to be length of s seen as an n-stack. More precisely, sh(v) is such that s

= [s 1 • • • s sh(v) ].
For an infinite play Λ = v 0 v 1 • • • , 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 Λ = {i ∈ N | ∀j ≥ i sh(v j ) ≥ sh(v i )}. Note that Steps Λ is always infinite and hence induces a decomposition of the play Λ into finite pieces.

For all pair (i, j) ∈ Steps Λ , with i = j and such that there is no k ∈ Steps Λ such that i < k < j, we define

mcol(i, j) = min{Ω(v k ) | i ≤ k ≤ j} and kind(i, j) = S if sh(v j ) = sh(v i ) + 1 B if sh(v j ) = sh(v i )
In the factorization induced by Steps Λ , a factor v i • • • v j will be called a bump if kind(i, j) = B, and will be called a

Stair if kind(i, j) = S. A bump v i • • • v j where j = i + 1 is called a trivial bump.

For any play Λ with Steps

Λ = {n 0 < n 1 < • • • }, one defines the sequences (mcol Λ i ) i≥0 ∈ C N where mcol Λ i = mcol(n i , n i+1 ) and (kind Λ i )) i≥0 ∈ {B, S} N where kind Λ i = kind(n i , n i+1
). The sequence (mcol Λ i ) i≥0 fully characterizes the parity condition.

Proposition 15 For a play Λ the following equivalences hold: Λ is winning for Éloïse iff lim inf((mcol Λ i ) i≥0 ) is even.

The main idea to solve G is to build an (n-1)-CPDS parity game G played on a game graph G defined by an exponentially larger (n -1)-CPDS with the same set of colours. This new game simulates the pushdown game, in the sense that the sequences of visited colours during a correct simulation play are exactly the sequences (mcol Λ i ) i≥0 for plays Λ in the original game. Moreover, a play in which a player does not correctly simulate the n-CPDS game is loosing for that player.

Before providing a description of the game graph G, let us consider the following informal description of this simulation game.

In this simulation game, the players only recall an (n -1)-stack with some extra information. Such an (n -1)-stack aims at simulate a configuration in G whose top (n -1) is that stack.

The most interesting case is when, simulating a configuration v with a control state p and a top (n -1)stack s, the player owning p wants to apply a transition push n and change the control state to q. For every strategy of Éloïse, there is a (possibly empty) set of possible finite continuations of the play that will end with returning to a configuration with the same stack content as the one in v. If this happens, it means that eventually a configuration with stack height equal to sh(v) is reached. Hence, in the simulation game Éloïse, is required to declare a vector -→ R = (R 0 , . . . , R d ) of (d + 1) subsets in 2 Q , where R i is the set of all states the game can be in when coming back to a configuration with stack height sh(v) along these plays where in addition the smallest visited colour while the stack height is greater than sh(v) is i.

Then Abelard has two options. He can continue the game by simulating the push n transition and update the control state (we call this a pursue move). Otherwise, he can pick a set R i and a state r ∈ R i , and continue the simulation from that state r (we call this a jump move). If he does a pursue move, the players now remember the vector -→ R claimed by Éloïse; if, later on, a pop n transition is simulated, a special configuration is reached where Éloïse wins if and only if the resulting state is in R κ where κ is the smallest colour seen since the stack height was greater than sh(v) (this information is 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 r in R i , the currently stored value for κ is updated to min(κ, i, Ω(r)), which is the smallest colour seen since the current stack level was reached). Now we discuss the other kinds of transitions, including collapse, that can be simulated.

• push k , pop k , or push a 1,k for some k < n and some a ∈ Γ: the simulation is an exact one and hence s is modifies and the control state is updates.

• collapse if the top 1 symbol has a k-link for some k < n: the simulation is an exact one and hence modifies s and updates the control state.

• push a 1,n : in this case as we only recall an (n -1)-stack there is no meaning of putting an n-link. Hence instead we apply a rule push

(a, - → R )
1,1 , where -→ R is the last vector declared by Éloïse (it is stored in the control state and easily retrieved). The idea behind this is that, if one simulates a collapse from this new stack content, then the play is returning to the previous stack height, and hence one has to check whether the vector -→ R , that Éloïse claimed to describe the possible behaviours on returning to the previous stack level, was correct with respect to this collapse (see below). We equip this symbol with a 1-link but actually we will never allow to apply collapse from it so one could consider that we do not have a link at all here (but we did not formally allow this in our definition of CPDS).

• collapse if the top 1 symbol simulates one with an n-link, equivalently is of the form (a, -→ R ): in this case we check whether the new control state r reached when applying collapse belongs to R ColRk(a) (recall that the n-CPDS P is collapse rank aware and that ColRk computes this rank in P). If it is the case, Éloïse wins, otherwise Abelard does.

(q, push (b, -→ R )

1,1 (s), -→ R , min(κ, Ω(q))) (q, θ(s), -→ R , min(κ, Ω(q))) Therefore the main vertices of the simulation game graph are configurations of the form (p, s, -→ R , κ) where s is an (n -1)-stack on the alphabet Γ ∪ (Γ × P(Q) d+1 ) and they are controlled by the player that controls p. Intermediate configurations are used to handle the previously described intermediate steps. The local structure is given in Figure 9 (circled vertices are those controlled by Éloïse). Two special vertices tt and ff are used to simulate pop n moves and collapse moves from configurations with an n-link on their top 1 symbol. Here vertices tt and ff are designed so that the player that controls it looses a game that reaches such a vertex: for this, tt is assigned an even colour while ff is assigned an odd colour, and both vertices have a loop on them and no other outgoing edge.

tt ff (p, s, -→ R , κ) (p, s, -→ R , κ, q) (p, s, -→ R , κ, q, -→ T ) (q, s, -→ T , Ω(q)) (t, s, -→ R , min(κ, i, Ω(t))) i If ∃ (r, pop n ) ∈ ∆(p,
The simulation game graph is equipped with a colouring function on the vertices and on the edges: vertices of the form (p, s, -→ R , κ) have colour Ω(p), and an edge leaving from a vertex (p, s, -→ R , κ, q, -→ T ) has a colour in {0, . . . , d} only if it simulates a bump (the colour is i iff the bump has colour i). It is easily seen that intermediate vertices can be introduced to have only colours on vertices. A precise description of the graph is given in the detailed proof of the following main result. The simulation parity game is denoted G.

Theorem 16 A configuration (p in , ⊥ n ) is winning for Éloïse in G if and only if (p in , ⊥ n-1 , (∅, . . . , ∅), Ω(p in ))
is winning for Éloïse in G. Moreover the game G is an (n -1)-CPDS parity game.

Proof of Theorem 16

We start with a precise description of G and with some extra definitions. Then we give a full proof of Theorem 16 44 The game graph G Let us first precisely describe the game graph G. As what follows is only a formal definition of the graph represented in Figure 9, one could skip this or refer only in case the figure is not clear enough.

• The main vertices of G are those of the form (p, s, -→ R , κ), where p ∈ Q, s is any (n -1)-stack (with links) on the stack alphabet Γ ∪ (Γ × P(Q) d+1 ), -→ R = (R 0 , . . . , R d ) ∈ P(Q) d+1 and κ ∈ {0, . . . , d}. A vertex (p, s, -→ R , κ) is reached when simulating a partial play Λ in G such that:

-The last vertex in Λ has control state p and its top (n -1)-stack s is such that π(s )=ν(s) where π(s ) denotes the stack obtained from s by replacing every n-link by a 1-link and ν(s) is the stack obtained from s by replacing every symbol (γ, -→ S ) by γ (and by preserving the link structure). This roughly means that s and s are very slightly different representations of a same stack.

-Éloïse claimed that she has a strategy to continue Λ in such a way that if s is eventually popped (by a pop n action), the control state reached after popping α belongs to R m , where m denotes the minimal colour visited since the current stack height (of the n-stack) was reached.

-The colour κ is the smallest one since the current stack height was reached from a lower stack level.

-Moreover, if top 1 (s) is of the form (a, -→ S ) then the top 1 symbol of the last vertex in Λ has an nlinked and if collapse is applied in the next move in Λ then Éloïse claimed that the control state of the configuration that is reached belongs to S k where k is the collapse rank, i.e. k = ColRk(a).

A vertex (p, s, -→ R , κ) is controlled by Éloïse if and only if p ∈ Q E .
• Vertices tt and ff are there to ensure the correctness of the vectors -→ R encoded in the main vertices and of the vectors -→ S encoded in the stack for symbols of the form (a, -→ S ). Vertex tt is controlled by Abelard, whereas vertex of the form ff belongs to Éloïse. There is a loop on each of these vertices and it is the only edge from it. We assign an odd colour to ff and an even colour to tt: hence the player controlling such a vertex is loosing.

There is a transition from some vertex (p, s, -→ R , κ) to tt, if and only if one of the two cases happens:

top 1 (s) = a or (a, -→ S ) and there is a transition rule (r, pop n ) ∈ ∆(p, a) such that r ∈ R κ (this means that -→ R is correct with respect to this transition rule).

top 1 (s) = (a, -→ S ) and there is a transition rule (r, collapse) ∈ ∆(p, a) such that r ∈ S ColRk(a)

(this means that -→ S is correct with respect to this transition rule).

Symmetrically, there is a transition from a vertex (p, s, -→ R , κ) to vertex ff if and only one of the two cases happens:

top 1 (s) = a or (a, -→ S ) and there is a transition rule (r, pop n ) ∈ ∆(p, α) such that r / ∈ R κ (this means that -→ R is not correct with respect to this transition rule).

top 1 (s) = (a, -→ S ) and there is a transition rule (r, collapse) ∈ ∆(p, a) such that r / ∈ S ColRk(a)

(this means that -→ S is not correct with respect to this transition rule).

• To simulate a transition rule that does not remove the topmost (n -1)-stack, one only has to update the control state, the component κ and apply the corresponding transformation on the stack. More precisely -there is a transition to (q, θ(s), -→ R , min(κ, Ω(q))) if (q, θ) ∈ ∆(p, a), top 1 (s) = a or (a, -→ S ) and θ = push k , pop k or push b 1,k for some b ∈ Γ and some k < n.

-there is a transition to (q, collapse(s), -→ R , min(κ, Ω(q))) if (q, collapse) ∈ ∆(p, a) and top 1 (s) = a (this means that there is a k-link for some k < n and hence the simulated collapse do not remove the top (n -1)-stack).

-there is a transition to (q, push (b, -→ R )

1,1 (s), -→ R , min(κ, Ω(q))) if (q, push b 1,n ) ∈ ∆(p, a) and top 1 (s) = a or (a, -→ S ), for some b ∈ Γ. In this case, as we only have (n -1)-stacks in G, we replace the n-link by a (dumb) 1-link and annotate the symbol b by the last vector -→ R claimed by Éloïse (if one wants to simulate collapse for b then the control state reached should be in a set described in -→ R because the stack level reached is the one just behind the current one).

• To simulate a transition rule (q, push n ) ∈ ∆(p, a), the player that controls (p, s, -→ R , κ) goes in (p, s, -→ R , κ, q). This vertex is controlled by Éloïse who has to give a vector -→ T = (T 0 , . . . , T d ) ∈ P(Q) d+1 that describes the control states that can be reached if the play eventually comes back to the stack height just left by performing the push n action. To describe this vector, she goes to the corresponding vertex (p, s, -→ R , κ, q, -→ T ).

The vertex (p, s, -→ R , κ, q, -→ T ) 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 in this bump. To simulate a bump with minimal colour i, he goes to a vertex (t, s, -→ R , min(κ, i, Ω(t))), for some t ∈ T i , through an edge coloured by i.

To simulate a stair, Abelard goes to the vertex (q, s, -→ T , Ω(q)).

The last component (that stores the smallest colour seen since the currently simulated stack level was reached) has to be updated in each of these cases. After simulating a bump of minimal colour i, the minimal colour is min(κ, i, Ω(s)). After simulating a stair, the colour has to be initialized (since a new stack height is simulated). Its value, is therefore Ω(q), which is the unique colour since the (new) stack level was reached.

The only vertices that are coloured are those of the form (p, s, -→ R , κ) and the colour of such a vertex is Ω(p). Some edges are also coloured. See Figure 9 for details. Remark 6.7 In the definition of parity games we were requiring to have a total colouring function working only on vertices. For this, one can add extra intermediate states and introduce a new colour larger than d to fit the definition without changing the issue of that game.

Finally the following fact is easily checked.

Property 17

The game graph G is generated by a (n -1)-CPDS.

Proof It is immediate. The only point to note is that the vertices tt and ff can be simulated using a control state where the CPDS is looping.

Factorization of a play in G

Recall that in G some edges are coloured. Hence, to represent a play, we have to encode this information on edge colouring. A play will be represented as a sequence of vertices together with colours in {0, . . . , d} that correspond to colours appearing on edges.

For any play in G, a round is a factor between two visits through vertices of the form (p, s, -→ R , κ). We have the following possible forms for a round:

• The round is of the form (p, s, -→ R , κ)(q, θ(s), -→ R , min(κ, Ω(q))) and corresponds therefore to the simulation of a trivial bump.

• The round is of the form (p, s, -→ R , κ)(p, s, -→ R , κ, q)(p, s, -→ R , κ, q, -→ T )i(t, s, -→ R , min(κ, i, Ω(t))) and corresponds therefore to the simulation of a rule push n followed by a sequence of moves that ends by coming back to the former stack level. Moreover the minimal colour in this sequence of moves is i.

• The round is of the form (p, s, -→ R , κ)(p, s, -→ R , κ, q)(p, s, -→ R , κ, q, -→ T )i(q, s, -→ T , Ω(q)) and corresponds therefore to the simulation of a rule push n leading to a new stack height below which the play will never go. We designate it has a stair.

For any play

λ = v 0 v 1 v 2 • • • in G,
we consider the subset of indices corresponding to vertices of the form (p, s, -→ R , κ). More precisely:

Rounds λ = {n ∈ N | v n = (p, s, -→ R , κ), for some p, s, - → R , κ}
Therefore, the set Rounds λ induces a natural factorization of λ into rounds.

λ = {n 0 < n 1 < n 2 < • • • }, then for all 0 ≤ i < |Rounds λ |, λ i = v n i • • • v n i+1 .
Therefore, for every i ≥ 0, the first vertex in λ i+1 equals the last one in λ i . Moreover, λ = λ 1 λ 2 λ 3 • • • , where λ i λ i+1 denotes the concatenation of λ i with λ i+1 without its first vertex.

Finally, the colour of a round is the smallest colour in {0, . . . , d} appearing in the round.

In order to prove both implications of Theorem 16, 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 factorizations of plays in both games.

Direct implication Assume that the configuration (p in , ⊥) is winning for Éloïse in G, and let Φ be a corresponding strategy for her.

Using Φ, we define a strategy ϕ for Éloïse in G from (p in , ⊥ n-1 , (∅, . . . , ∅), Ω(p in )). Strategy Φ stores a partial play in G, that is an element in V * (where V denotes the set of vertices of G). This memory will be denoted by Λ. At the beginning Λ is initialized to the vertex (p in , ⊥ n ). 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 (p, s, -→ R , κ) for p ∈ Q E . The move given by ϕ depends on Φ(Λ):

• If Φ(Λ) = (r, pop n ), then Éloïse goes to tt (Proposition 18 will prove that this move is always possible).

• If Φ(Λ) = (r, collapse) and top 1 (s) is of the form (a, -→ S ), then Éloïse goes to tt (Proposition 18 will prove that this move is always possible).

• If Φ(Λ) = (q, θ), for some θ = push k , pop k or push b 1,k with b ∈ Γ and k < n, or θ = collapse and top 1 (s) ∈ Γ, then Éloïse goes to (q, θ(s), -→ R , min(κ, Ω(q))).

• If Φ(Λ) = (q, push b 1,n ), then Éloïse goes to (q, push

(b, - → R ) 1,1 (s),
-→ R , min(κ, Ω(q))).

• If Φ(Λ) = (q, push n ), then Éloïse goes to (p, s, -→ R , κ, q).

In this last case, or in the case where p ∈ Q A and Abelard goes to (p, s, -→ R , κ, q), we also have to explain how Éloïse behaves from (p, s, -→ R , κ, q). She has to provide a vector -→ T ∈ P(Q) d+1 that describes which states can be reached if the play eventually comes back to the previous stack height, depending on the minimal colour visited in the meantime. In order to define -→ T , she considers the set of all possible continuation of Λ • (q, push n (σ)) (where (p, σ) denotes the last vertex of Λ) where she respects her strategy Φ. For each such play, she checks whether some configuration of the form (s, σ ) with sh(σ ) = sh(σ) is visited after Λ • (q, push n (σ)), that is if the new top (n -1)-stack is eventually removed (note that it could be due either to a pop n action either to a collapse). If it is the case, she considers the first such configuration (s, σ ) and the smallest colour i visited between (q, push n (σ)) (included) and (s, σ ) (excluded). For every i ∈ {0, . . . d}, T i is exactly the set of states s ∈ Q such that the preceding case happens. Finally, we set -→ T = (T 0 , . . . , T d ) and Éloïse moves to (p, s, -→ R , κ, q, -→ T ).

Update of Λ.

The memory Λ is updated after each visit to a vertex of the form (p, s, -→ R , κ). We have three cases depending on the kind of the round:

• The round is a trivial bump and therefore a transition (q, θ) where θ is of the form push k , pop k , push b 1,k , push b 1,n or collapse was simulated. Let (p, σ) be the last vertex in Λ, then the updated memory is Λ • (q, θ(σ)).

• The round is a bump. Therefore a bump of colour i (where i is the colour of the round) starting with some transition (q, push n ) and ending in a state s ∈ S i was simulated. Let (p, σ) be the last vertex in Λ. Then the memory becomes Λ extended by (q, push n (σ)) followed by a sequence of moves, where Éloïse respects Φ, that ends by some configuration (s, σ ) with sh(σ) = sh(σ ) 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 the transition (q, push n ). If (p, σ) denotes the last vertex in Λ, then the updated memory is Λ • (q, push n (σ)).

Therefore, with any partial play λ in G in which Éloïse respects her strategy ϕ, is associated a partial play Λ in G. 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 (p in , ⊥ n ) and Éloïse respects Φ in that play. Therefore she wins in Λ.

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

Proposition 18 Let λ be a partial play in G that starts from (p in , ⊥ n-1 , (∅, . . . , ∅), Ω(p in )), ends in a vertex of the form (p, s, -→ R , κ), and where Éloïse respects ϕ. Let Λ be the play associated to λ built by the strategy ϕ. Then the following holds:

1. Λ ends in a vertex of the form (p, σ) where π(top n (σ)) = ν(s). [START_REF] Maslov | The hierarchy of indexed languages of an arbitrary level[END_REF] 2. κ is the smallest visited colour in Λ since the last configuration with a stack height strictly smaller than sh(σ).

3. Assume that Λ is extended, that Éloïse keeps respecting Φ and that the next move after (p, σ) is to apply a transition (r, pop n ). Then r ∈ R κ . [START_REF] Maslov | The hierarchy of indexed languages of an arbitrary level[END_REF] Recall that π(σ ) denotes the stack obtained from σ by replacing every n-link by a 1-link and ν(s) is the stack obtained from s by replacing every symbol (γ, -→ S ) by γ (and by preserving the link structure).

4. Assume that Λ is extended, that Éloïse keeps respecting Φ, that the next move after (p, σ) is to apply a transition (r, collapse) and that top 1 (σ) has an n-link. Then top 1 (s) = (a, -→ S ) and r ∈ S ColRk(a) . Remark 6.9 Proposition 18 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 infinite plays that do not reach tt, using the definitions of G and ϕ, we easily deduce the following proposition.

Proposition 19 Let λ be an infinite play in G that starts from (p in , ⊥ n-1 , (∅, . . . , ∅), Ω(p in )), and where Éloïse respects ϕ. We additionally suppose that λ never reaches the vertex tt. Let Λ be the associated play built by the strategy ϕ. Let (λ i ) i≥0 be the round factorization of λ. Then, for every i ≥ 1 the following hold:

1. λ i is a bump if and only if kind Λ i = B.
2. λ i has colour mcol Λ i .

Proposition 19 implies that for any infinite play λ in G starting from (p in , ⊥ n-1 , (∅, . . . , ∅), Ω(p in )) where Éloïse respects ϕ, if λ never reaches tt then the minimum colour infinitely often visited in λ is lim inf((mcol Λ i ) i≥0 ) for the corresponding play Λ in G. Hence, using Proposition 15 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. Hence ϕ is a winning strategy for Éloïse, as any play where she respects it either reaches tt (and therefore satisfies the parity condition) or satisfies the parity condition (by proposition 15 and 19).

Converse implication For the converse implication, one could adapt the proof of the direct implication to show that if Abelard has a winning strategy in G he also has one in G. The construction is the same as for Éloïse except that now Abelard has to decide whether to do a pursue move or a jump move. For this he computes his own vector -→ T (as Éloïse was doing in the previous construction) and checks for consistency with the one ( -→ T ) claimed by Éloïse: if they are consistent (i.e. there is some t ∈ T i ∩ T i for some i) he does a jump move for this t, otherwise he does a pursue move. One can check that this strategy is winning for him in G.

Here we give a different proof, that builts a winning strategy in G from one in G. This is more involved than the proof sketched just above, but it has the major interest to provide an effective construction for strategies in CPDS parity games.

Assume now that Éloïse has a winning strategy ϕ in G from (p in , ⊥ n-1 , (∅, . . . , ∅), Ω(p in )). Using ϕ, we build a strategy Φ for Éloïse in G for plays starting from (p in , ⊥ n ).

Strategy Φ uses, as memory, a (1-) stack Π, to store the complete description of a play in G. Recall here that a play in G is represented as a sequence of vertices together with colours in {0, . . . d}.

Therefore the stack alphabet of Π is the set of vertices of G together with {0, . . . , d}. In the following, top(Π) will denote the top stack symbol of Π while StCont(Π) will be the word obtained by reading Π from bottom to top (without considering the bottom-of-stack symbol of Π). In any play where she respects Φ, StCont(Π) will be a play in G that starts from (p in , ⊥ n-1 , (∅, . . . , ∅), Ω(p in )) and where Éloïse respects her winning strategy ϕ. Moreover, for any play Λ where Éloïse respects Φ, we will always have that top(Π) = (p, s, -→ R , κ) if and only if the current configuration (p, σ) is such that π(top n (σ)) = ν(s). Finally, if Éloïse keeps respecting Φ, and if the next move is to a configuration with a stack height smaller than sh(σ), then its control state will be in R κ if the configuration is reached by applying a pop n action, and will be in S ColRk (a) where (a, -→ S ) = top 1 (s). Initially, Π only contains (p in , ⊥ n-1 , (∅, . . . , ∅), Ω(p in )).

1. top(Π) = (p, s, -→ R , κ) with -→ R ∈ P(Q) d+1 , 0 ≤ θ ≤ d and π(top n-1 (σ)) = ν(s).

2. StCont(Π) is a partial play in G that starts from (p in , ⊥ n , (∅, . . . , ∅), Ω(p in )), that ends with (p, s, -→ R , κ) and where Éloïse respects ϕ.

3. κ is the smallest colour visited since the stack height is greater or equal than sh(σ).

4. If Λ is extended by some move (r, pop n ), then r ∈ R θ .

5. If Λ is extended by some move (r, collapse) and if top 1 (σ) has an n-link, then top 1 (s) = (a, -→ S ) and the control state in the new configuration belongs to S ColRk(a) .

Proof

The proof goes by induction on Λ. We first show that the fourth point is a consequence of the second and third points. Assume that the next move after (p, σ) is to apply an action (r, pop n ). The second point implies that (p, s, -→ R , κ) is winning for Éloïse in G. If p ∈ Q E , by definition of Φ, there is some edge from that vertex to tt, which means that r ∈ R θ and allows us to conclude. If p ∈ Q A , note that there is no edge from (p, s, -→ R , κ) (winning position for Éloïse) to the loosing vertex ff . Hence we conclude the same way.

We now show that the fifth point is a consequence of the second and third points. Assume that the next move after (p, σ) is to apply an action (r, collapse) and that it involves an n-link. The second point implies that (p, s, -→ R , κ) is winning for Éloïse in G. If p ∈ Q E , by definition of Φ, there is some edge from that vertex to tt, which means that r ∈ S ColRk(a) and allows us to conclude. If p ∈ Q A , note that there is no edge from (p, s, -→ R , κ) (winning position for Éloïse) to the loosing 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 Λ be some extension of Λ. We have several cases, depending on how Λ extends Λ:

• Λ is obtained by applying a rule of type push k , pop k or push b 1,k for some k < n, k ≤ n and b ∈ Γ. The result is trivial in that case.

• Λ is obtained by applying a collapse rule involving a k-link for some k < n. The result is also immediate in this case.

• Λ is obtained by applying a pop n rule. Let (p, σ) be the last configuration in Λ, and let -→ R be the last vector in top(Π) when being in configuration (p, σ). By induction hypothesis, it follows that Λ = Λ • (r, σ ) is such that r ∈ R θ . Considering how Π is updated, and using the fourth point, we easily deduce that the new strategy stack Π is as desired.

• Λ is obtained by applying a collapse rule involving an n-link. Let (p, σ) be the last configuration in Λ, and let (a, -→ S ) be top 1 (Π) when being in configuration (p, σ). By induction hypothesis, it follows that Λ = Λ • (s, σ ) is such that s ∈ S ColRk(a) . Considering how Π is updated, and using the fifth point, we easily deduce that the new strategy stack Π is as desired. Now, the following result is an easy consequence of the previous lemma.

Lemma 21 Let Λ be a partial play in G starting from (p in , ⊥ n ) and where Éloïse respects Φ. Let λ = StCont(Π), where Π denotes the strategy stack in the last vertex of Λ. Let (λ i ) i=0,...,k be the round factorization of λ. Then the following holds:

• λ i is a bump if and only if kind Λ i is a bump.

that R 0 and R 1 can be forced to be singletons: this follows from the fact that all vertices in G are controlled by Éloïse (and then from the proof's details). Therefore, one concludes that the size of the game graph associated with G is polynomial in the size of A. Hence, one has shown the following: checking emptiness for an order-(n + 1) nondeterministic higher order pushdown automaton whose input alphabet is reduced to a single letter can be polynomially reduced to solve a reachability game over the transition graph of an order-n higher order pushdown automaton. In conclusion, this last problem is n-EXPTIME hard (and actually n-EXPTIMEcomplete).

Strategies

We finally focus on winning strategies. From the proof of the converse implication of Theorem 16 one can infer that it is possible to construct effectively strategies for both player in a parity CPDS game. Here, we give a more precise statement by providing a precise information on the memory needed in such a game. Recall that for regular games on finite graph, it is well know since Büchi Landweber seminal paper that a finite automaton with output suffices to represent winning strategies. For pushdown parity game, Walukiewicz has shown in [26] that pushdown automaton with output suffices to compute a winning strategy and this result was then extended (without proof) by Thierry Cachat [3] who showed that higher-order pushdown automata with output (of order n) allow to compute winning strategy for higher order pushdown game (of order n). Here we extend this last result to CPDS parity games, which terminates the proof of Theorem 13.

Theorem 23

In an n-CPDS parity game one can build, for the player having a winning strategy from a given configuration with an empty stack, a (deterministic) n-CPDA with output [START_REF] Moggi | Notions of computation and monads[END_REF] realizing a winning strategy. Moreover the stack used by the strategy automaton has exactly the same structure [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF] has the one in the game.

Proof The following proof is not totally formal. Indeed, we believe that a totally formal and detailed proof would be very hard to understand (and to write) and we expect the following sketch to be rather convincing.

First note that in the proof of Lemma 14, if one has an n-CPDA with output realizing a winning strategy in the rank-aware game one also has an n-CPDA with output realizing a winning strategy in the non-aware game.

Hence it suffices to consider the proof of the converse implication of Theorem 16 and infers that if the winning strategy ϕ in G is realized by an (n -1)-CPDA with output, the strategy Φ in G can be realized by an n-CPDA with output.

Recall that strategy Φ was using a stack Π to store plays in G. Then it considers the value of ϕ on that stack content to decide which move to play. Hence, if strategy ϕ can be realized by an (n -1)-CPDA with output, one can instead of representing a play in Π represent the sequence of memory values used by ϕ: the resulting structure is an n-stack (stack of (n -1)-stack). Nevertheless there is still some work to do. Indeed the new strategy stack (that we also denote Π) has not the same shape as the one in the game: this is mainly because in the former Π we where storing all bumps which may cause the stack to be much larger than the one in the game G. Nevertheless, we only need the information on the last vertex of a bump, and never need to retrieve information on an intermediate vertex in previous bumps in the current stack level; actually the only important information is the one concerning vertices corresponding to stack height such that no vertex later has a stack height smaller or equal to this one. Hence after performing a bump we can forgot about the information on the initial vertex of the bump and only recall the one on the last vertex of the bump. Therefore, the resulting strategy stack (again denoted Π) has the same shape (except for n-links) than the current stack in the game. Moreover Assume that Éloïse has a winning strategy in G from some vertex (v, s 0 ). Let ϕ : (V × S) * → (V × S) be such a winning strategy [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF] . From ϕ we define a winning strategy ϕ for Éloïse in G. First note that as G is edge-labeled, a play is now an infinite sequence of the form (v 0 , a 0 , v 1 )(v 1 , a 1 , v 2 )(v 2 , a 2 , v 3 ) • • • and hence a strategy is a mapping from (V ×A×V ) * into (V ×A×V ). Let λ = (v 0 , a 0 , v 1 )(v 1 , a 1 , v 2 ) • • • (v k-1 , a k-1 , v k ) be some partial play ending in a vertex v k controlled by Éloïse. Let s 0 s 1 • • • s k be the (unique) run of S on a 0 a 1 • • • a k-1 . Then it easily follows that λ = (v 0 , s 0 )(v 1 , s 1 ) • • • (v k , s k ) is a partial play in G and hence ϕ (λ ) = (v k+1 , s k+1 ) is well defined. As ((v k , s k ), (v k+1 , s k+1 )) ∈ E then there is at least one a k ∈ A such that (v k , a k , v k+1 ) ∈ E. Let us pick any such a k and set ϕ(λ) = (v k , a k , v k+1 ). The strategy ϕ is trivially well-defined, and we claim that it is wining. Indeed, consider an infinite play λ = (v 0 , a 0 , v 1 )(v 1 , a 1 , v 2 )(v 2 , a 2 , v 3 ) • • • in G where Éloïse respects ϕ. From how ϕ was defined, we deduce that if s 0 s 1 s 2 • • • is the unique run of S on a 0 a 1 a 2 • • • , then λ = (v 0 , s 0 )(v 1 , s 1 )(v 2 , s 2 ) • • • is a play in G where Éloïse respects her winning strategy ϕ and hence is winning for her. Therefore, it follows that s 0 s 1 s 2 • • • is an accepting run of S on a 0 a 1 a 2 • • • and hence that a 0 a 1 a 2 • • • ∈ Ω, equivalently that λ is winning for Éloïse.

Conversely, using the same construction for Abelard, one built from a winning strategy for him in G a winning strategy in G.

One should note that the increase of memory from a winning strategy in G to a winning strategy in G can be handled by a finite automaton, namely S.

Hence we have the following corollary of Theorem 13.

Corollary 25

Given any n-CPDA game equipped with an ω-regular winning condition it is decidable whether Éloïse has a winning strategy from the initial configuration. Moreover one can construct an n-CPDS with output that realizes a winning strategy for the player that wins from the initial configuration.

Proof Applying Proposition 24, one gets an equivalent parity game. It is then easy to check that if one starts with a collapsible pushdown graph, the resulting graph is still a collapsible one (of same order) as the transformation only operates on the control states. Then decidability follows from the one for parity collapsible pushdown games.

ε-closure of CPD graphs

Theorem 13 can easily be generalized to the case where the game is played on the ε-closure of the configuration graph of an n-CPDS graph.

Hence One considers an order-n collapsible pushdown automaton with input and ε-transition A, that is an order-n collapsible pushdown automaton with input alphabet A containing a special symbol denoted ε. As explain previously, it defines an A-labeled transition graph G = (V, E ⊆ V × A × V ). The ε-closure of G, denoted G ε * , is the graph (V ε * , E ε * ⊆ V ε * × (A \ {ε}) × V ε * ) where • V ε * ⊆ V is the subset of vertices reachable from the initial configuration by a finite sequence of transitions such that the last one is not labeled by ε.

• (v, a, v ) ∈ E ε * if and only if v, v ∈ V ε * and there is a path in G from v to v labeled by a (possibly empty) sequence of ε transition followed by a transition labeled by a.

Example 2 . 1

 21 Take the 3-stack s = [[[⊥ a]] [[⊥][⊥ a]]]. (To save writing, we omit the superscript (1, 1).) We have push b,2 1 s = [[[⊥ a]] [[⊥][⊥ a b

  in this order). As α -→ is a partial function, whenever there is an M such that M α -→ M , we shall often use the postfix notation M α -→ to denote (the necessarily unique) M .

(-→ and M α 0 -

 0 Note that in case e = j, by definition of push j we have f ≥ 2.) Since M represents (p, s) by assumption, it follows that the head non-terminal of M α 0 -→ is F b,e p . Now M θ -→ and M are (nj)-similar. Since α 0 is a b-probe, by applying Lemma 1 repeatedly, we have (M θ → are (nj)-similar. Hence the head non-terminal of (M θ also F b,e p . It remains to prove that, assuming b = ⊥, we have

Figure 3 : 5 . 6

 356 Figure 3: A run of a 2-CPDA

Figure 4 :

 4 Figure 4: An order-3 traversal

Figure 8 :

 8 Figure 8: A run of a 3-CPDA (Part 3 of 3).

  (a) We need to show top 2 s = t . By definition of s , we have top 2 s = (top 2 s) ≤u 0 v, i.e. top 2 s is the prefix of the 1-stack top 2 s -regarded as a sequence -up to and including the occurrence of u 0 described above, extended by v. By induction hypothesis (a) we have top 2 s = t . Thustop 2 s = t ≤u 0 v = t ≤u 0 v = tas required (the second equation holds because u 0 appears in t ).(b) We have s = sv and t = tv. Since s = t by induction hypothesis (b), we have s = t .

Example 6 . 1

 61 Take the 2-CPDS[START_REF] Knapik | Higher-order pushdown trees are easy[END_REF] with state-set { 0, 1, 2 }, stack alphabet { a, b, ⊥ } and transition relation given by (0, -, 1, t), (1, -, 0, a), (1, -, 2, b), (2, †, 2, 1), (2, †, 0, 0)

∀Figure 9 :

 9 Figure 9: Local structure of G.

Definition 6 . 8 (

 68 Rounds factorization) For a (possibly partial) play λ = v 0 v 1 v 2 • • • , we call rounds factorization of λ, the (possibly finite) sequence (λ i ) i≥0 of rounds λ defined as follows. Let Rounds

  • • • e n , where D : (A 1 , • • • , A n , o) is a non-terminal and n ≥ 1 (i.e. D has order at least 1), by @ A D e 1 • • • e n where A =

Higher-order recursion schemes are essentially simply-typed lambda calculus with general recursion and uninterpreted first-order function symbols

As constraints on recursion schemes, derived types and safety are actually equivalent; see[START_REF] Miranda | Structures generated by higher-order grammars and the safety constraint[END_REF] for a proof.

Thus 1-links are invariant -they always point to the preceding symbol and no stack operation will change that.

I for internal or hidden Player-move, P for Player-move, and O for Opponent-move.

The branch language of t :Dom(t) -→ Σ consists of infinite words (f1, d1)(f2, d2) • • • just if for 0 ≤ i < n, we have t(d1 • • • di) = fi+1; and of finite words (f1, d1) • • • (fn, dn)a just if for 0 ≤ i < n, we have t(d1 • • • di) = fi+1 and t(d1 • • • dn) = a.

We would like to refer to the Σ-labelled tree generated by a recursion scheme as its value tree, because the name is a good counterpoint to computation tree. We have in mind here the distinction between value and computation emphasized by Moggi[START_REF] Moggi | Notions of computation and monads[END_REF]. The idea is that the value tree is obtained from the computation tree by a (possibly infinite) process of evaluation.

To my knowledge, Colin Stirling was the first to use a tree representation of lambda terms in which "dummy lambdas" are employed; see his CSL 2005 paper[START_REF] Stirling | Higher-order matching and games[END_REF]. Motivated by property-checking games in Verification, he has introduced a game that is played over such trees as a characterization of higher-order matching[START_REF] Stirling | Decidability of higher-order matching[END_REF].

The leftmost child of a @-labelled node is the latter's 0-child (i.e. the child is at the end of a 0-labelled edge); the leftmost child of any other node is a 1-child.

When defining -→ and the tree generated by the recursion scheme GA, we simply ignore the labels that annotate the rewrite rules -.

An active context is just an ground-type applicative term that contains a ground-typed hole, into which a term may be inserted.

Here traversals are justified sequences of nodes of the graph Gr(G), as opposed to nodes of the computation tree λ(G) which is the unfolding of Gr(G). The latter is the notion defined in the preprint[START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF], but the difference is of no significance for the purpose we have in mind.

s). Then s σ computes t <v i .

As an example: solving a reachability game on a finite graph is in P while checking emptiness for an alternating automata on finite word (even if one considers a 1 letter alphabet) is PSPACE-complete

An n-CPDA with output is defined as a CPDA except that the transition function also provide a symbol (in a specific alphabethere one describing moves in the game) to be output for every

transition[START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF] Here we mean that if one replaces every symbol in the CPDA stack and in the strategy stack by a fixed new symbol then the two resulting stacks are the equal

One could consider for ϕ a memoryless strategy, but we prefer to consider the general case here has we may later argue that one can build effective winning strategies for ω-regular collapsible pushdown games from winning strategies for parity collapsible pushdown games that we may not choose memoryless.

4. The algorithm that transforms recursion schemes to CPDA (briefly sketched in Section 5) uses ideas in game semantics. It would be an interesting (and we believe challenging) problem to obtain a translation that uses only first principles.

An important consequence of the Equi-Expressivity Theorem is the following.

Theorem 11 Let t be a tree generated by an order-n recursion scheme. Consider the following problems: (P 2 ) Given t and a modal mu-calculus formula ϕ, does ϕ hold at the root of t? (P 3 ) Given t and an alternating parity tree automaton, does the automaton accept t? (P 4 ) Given t and an MSO formula ϕ, does ϕ hold at the root of t?

Then problem (P i ) is polynomially equivalent to problem (P i ) for every i = 2, 3, 4.

Since the modal Mu-calculus model checking problem for trees generated by (higher-order) recursion schemes is decidable [20], we obtain the following as an immediate consequence.

Theorem 12 Problems (P 1 ) -(P 4 ) are decidable with complexity n-EXPTIME complete.

Hence the Equi-Expressivity Theorem is a powerful tool to transfer decidability properties from recursion schemes to CPDS. Another remarkable consequence is that it gives totally new techniques for modelchecking or solving games played on infinite structure generated by automata. In particular it leads to new proofs/optimal algorithms for the special cases that were considered previously [26, 3, 16]. Conversely, as the Equi-Expressivity Theorem works in both directions, one can note that a solution of problem (P 1 ) would give a new proof of the decidability of problems (P 1 )-(P 1 ), and would give a new approach to problems on recursion schemes.

Actually, the techniques of [26, 16] can be generalized to solve n-CPDS parity games without referring to [20]. Further it gives effective winning strategies for the winning player (which was not the case in [16] where the special case n = 2 was considered).

Theorem 13 Solving an n-CPDS parity game is n-EXPTIME complete and it can be achieved without appealing to a translation to recursion schemes and to the decidability result in [20]. Moreover, one can build an n-CPDA with output that realizes a winning strategy for the winning player.

The next section is devoted to the proof of Theorem 13

Solving games over collapsible pushdown games: a direct proof

We an order-n collapsible pushdown system

We denote by G = (V, E) the transition graph of P, by G = G, V E , V A the game graph associated with the previous partition of Q, and by G = G, Ω the parity game on P induced by the previous colouring function.

In this section, we give a proof of Theorem 13, i.e. we explain how to solve the parity game G defined from P. Here, we only focus on deciding the winner from a configuration of the form (p in , ⊥ n ), that is a configuration with an empty stack. Then it is easy to solve the game from any configuration. Indeed if one wants to decide for some configuration (p, σ) ∈ V , it suffices to construct a new n-CPDS that mimics P excepts that from its initial configuration it starts by reaching configuration (p, σ) and only when this has happens the simulation of P starts. Therefore (p, σ) is winning for the same player in G and in the (naturally defined) new n-CPDS game. Note that this reduction is linear in the size of both P and in the length of (p, σ).

In order to describe Φ, we assume that we are in some configuration (p, σ) and that top(Π) = (p, s, -→ R , κ). We first describe how Éloïse plays if p ∈ Q E , and then we explain how the Π is updated.

• Choice of the move. Assume that p ∈ Q E and that Éloïse has to play from some vertex (p, σ). For this, she considers the value of ϕ on StCont(Π).

If it is a move to tt, she plays an action (r, pop n ) for some state r ∈ R κ if exists or she play (r, collapse) for some r ∈ S ColRk(a) where top 1 (s) = (a, -→ S ). Lemma 20 will prove that such a move always exists.

If the move given by ϕ is to go to some vertex (q, θ(s), -→ R , min(κ, Ω(q))) with θ = push k , pop k or push b 1,k for some k < n and b ∈ Γ, she plays the transition (q, θ). If the move given by ϕ is to go to some vertex (q, push b, -→ R 1,1 (s), -→ R , min(κ, Ω(q))), then she applies the transition (q, push b 1,n ).

If the move given by ϕ is to go to some vertex (p, s, -→ R , κ, q), then Éloïse applies the transition (q, push n ).

• Update of Π. Assume that the last move, played by Éloïse or Abelard, was to go from (p, σ) to some configuration (r, σ ) with sh(σ ) < sh(σ) (i.e. the move was either a pop n or a collapse involving an n-link).

-If the move is a pop n one, then Éloïse pops in Π until she finds some configuration of the form (p , s , -→ R , κ , p , -→ R ) that is not preceded by a colour in {0, . . . , d}. This configuration is therefore in the stair that simulates the step where the stack level sh(σ) is reached. Eve updates Π by pushing κ in Π followed by (r, s , -→ R , min(κ , κ, Ω(r))).

-If the move is a collapse one, then let d = sh(s)sh(s ) (d denotes the decrease of the stack height). Then Éloïse pops in Π until she finds some configuration of the form (p , s , -→ R , κ , p , -→ R ) that is not preceded by a colour in {0, . . . , d}. If d = 1 she stops otherwise she keeps popping until she finds another such configuration (and so on until she found d such configurations). Let (p , s , -→ R , κ , p , -→ R ) be the d-th such configuration (this configuration is therefore in the stair that simulates the step where the stack level sh(σ ) was left). Eve updates Π by pushing ColRk(a), where (a, -→ S ) = top 1 (s) in Π followed by (r, s , -→ R , min(κ , ColRk(a), Ω(r))). Note that we actually have

Assume that the last move, played by Éloïse or Abelard, was to go from (p, σ) to some configuration (q, σ ) with sh(σ) = sh(σ ): hence the simulated move is (q, θ) for some θ = push k , pop k , push b 1,k or push b 1,n for some k < n and b ∈ Γ. Then Éloïse updates Π by pushing (q, θ(s),

Finally, assume that the last move, played by Éloïse or Abelard, was to go from (p, σ) to some configuration (q, σ ) with sh(σ

Intuitively, -→ S describes which states Éloïse can ensure to reach if a configuration with stack height sh(s) is eventually reached (while not visiting a configuration of lower stack height). Éloïse updates Π by successively pushing (p, s, -→ R , κ, q), (p, s, -→ R , κ, q, -→ S ), and (q, s, -→ S , Ω(q)).

The following lemma gives the meaning of the information stored in Π.

Lemma 20

Let Λ be a partial play in G, where Éloïse respects Φ, that starts from (p in , ⊥ n ) and that ends in a configuration (p, σ). We have the following facts:

Both lemmas 20 and 21 are for partial plays. A version for infinite plays would allow to conclude. Let Λ be an infinite play in G. We define an infinite version of λ by considering the limit of the stack contents (StCont(Π i )) i≥0 where Π i is the strategy stack after the i-th first moves in Λ. It is easily seen that such a limit exists, is infinite and corresponds to a play won by Éloïse in G. Moreover the results of Lemma 21 apply.

Let Λ be a play in G with initial vertex (p in , ⊥ n ), and where Éloïse respects Φ, and let λ be the associated infinite play in G. In particular λ is won by Éloïse. Thus, using Lemma 21 and Proposition 15, we conclude, as in the direct implication, that Λ is winning.

Complexity issues

The following Theorem gives the decidability and complexity bound of Theorem 13.

Theorem 22 Solving an n-CPDS parity game is an n-EXPTIME complete problem.

Proof The proof is by induction on n. Case n = 1 is the one of pushdown parity games [26]. Assume the result holds for n -1 and consider an n-CPDS parity game given G by an n-CPDS P = Γ, Q, ∆ for some n > 1. In a first step one transforms G into an equivalent game generated by a collapse rank-aware n-CPDS. By remark 6.6 this increases both the states set and the stack alphabet by a factor in |C| O(n) (C is the set of colors). Then one solves the game G and concludes. Solving G can be achieved in (n -1)-EXPTIME and the game G is built from a CPDS with a states set of size

Hence solving G can be achieved in n-EXPTIME.

Hardness follows from hardness for solving a parity game played on a (non-collapsible) higher order pushdown graph. A self content proof of this result was established by Thierry Cachat and Igor Walukiewicz, but was unfortunately not published.

Here we sketch another proof of this result that relies on the following result: checking emptiness of a nondeterministic higher-order pushdown automaton of order n is an (n -1)-EXPTIME complete problem [12]. Trivially this result is still true if we assume that the input alphabet is reduced to a single letter. The following result is also proved in [12]: checking emptiness of an alternating higher-order pushdown automaton of order n is an n-EXPTIME complete problem. Nevertheless note that this last result does not imply directly hardness for games on higher order pushdown graphs (because in general it is more difficult to check emptiness for an alternating device than to solve a reachability game on the corresponding class of graphs [START_REF] Maslov | Multilevel stack automata[END_REF] : the problems are trivially equivalent only when considering infinite words on a single letter alphabet). Now consider an order-(n+1) nondeterministic higher order pushdown automaton A whose input alphabet is reduced to a single letter. The language accepted by A is non-empty if and only if there is a path from the initial configuration of A to a final configuration of A in the transition graph G of A. Equivalently the language accepted by A is non-empty if and only if Éloïse wins the reachability game G over G where she controls all vertices (and where the play starts from the initial configuration of A and where final vertices are those corresponding to final configurations of A). Now consider the reduction used to prove Theorem 13 and apply it to G: it leads to an equivalent reachability game G that is now played on the transition graph of an order-n higher order pushdown automaton. In the new game graph, the main vertices are of the form (p, s, -→ R , κ): here -→ R is actually a pair (R 0 , R 1 ) (we consider a reachability condition) and κ is either 0 or 1. The important fact is the update after a pop n move is now very easy, as one simply needs to perform a pop n in Π (recall that we no longer keep information on intermediate nodes appearing on successive bumps on a same stack level). It remains to explain how the update can be handled for a collapse involving an n-link. This is very simple: one only has to attach n-links in Π when simulating a push a 1,n action and follow this link if a collapse is applied later. Note that now the stack Π and the one in the game have the same shape.

Extensions, consequences

Solving games with an ω-regular winning condition Theorem 13 can easily be generalized to the case where on considers on ω-regular winning condition.

In order to define such a winning condition, we may assume that the collapsible pushdown graph comes with an edge labeling. More precisely we start with an order-n collapsible pushdown system with input

where Γ is the stack alphabet, Q is a finite set of control states, A is an input alphabet, ∆ is the transition relation and q 0 is the initial state. We require ∆ to respect the standard convention that ⊥ cannot be pushed onto or popped from the stack. Configurations are defined as for the case without input. Now the one-step transition relation → is the union of the one-step transition relations → a (where a ranges over A) defined by (q, s) → a (q , s ) iff for some θ ∈ Op n , we have (q, top 1 s, a, q , θ) ∈ ∆, and s = θ(s). Then the configuration graph of A is defined as the graph whose vertices are the reachable configurations of A (defined as previously) and the edge relation is the relation → restricted to the reachable configurations. As for the unlabeled case, we partition the control states into E-states and A-states, and this extends naturally to a partition of the vertices of the CPD graph. Finally, the winning condition is given by an ω-regular language Ω ⊆ A ω , and a play is winning for Éloïse iff its underlying A-labeling belongs to Ω.

In order to prove the decidability of games over collapsible pushdown graphs with an ω-regular winning condition we give a more general reduction result.

Proposition 24 Let G be a game over some A-labeled graph G = (V, E ⊆ V × A × V ) with an ω-regular winning condition Ω. Then one can define a parity game G over a graph G = (V × S, E ) for some set S containing a distinguished state s 0 such that the following holds: for any vertex v ∈ V , Éloïse wins from v in G if and only if she wins from (v, s 0 ) in G .

Moreover, from a winning strategy from (v, s 0 ) in G , one can effectively build a corresponding winning strategy from v in G that only requires a finite amount of extra memory.

Proof

The main idea of the construction is to consider a deterministic parity automaton accepting Ω and to plug it in G in order to compute on the fly the unique run of it on the labeling of the current play.

Let S = S, A, δ, s 0 , ρ be a deterministic parity automaton accepting Ω: S is a finite set of control states, A is an input alphabet, δ :

Let V E ∪ V A be the partition of the vertices in G. Then one considers the partition V E × S ∪ V A × S and defines G to be the parity game defined on G equipped with this partition together with the priority function assigning to any vertex (v, s) the priority ρ(s).

We consider a partition of the control states of A into E-states and A-states, and assign a priority to each control state. The game structure extends naturally to a partition of and a priority function on the vertices of G ε * . We aim at deciding the winner in the resulting game from the initial configuration. For this we prove a more general reduction result.

Proposition 26 Let G ε * be a parity game on the ε-closure of some (A ∪ {ε})-labeled graph G = (V, E). Then one can define a parity game G over an unlabeled graph G = (V = V ∪ V × {E, A}, E ) such that the following holds: for any vertex v ∈ V , Éloïse wins from v in G ε * iff she wins from v in G .

Moreover, from a winning strategy from v in G , one can effectively build a corresponding winning strategy from v in G ε * .

Proof By definition, a transition in G ε * can be naturally decomposed as a sequence of ε transitions in G ended by a non-ε transition in G. The graph G aims at making this decomposition explicit: in G when some player (let us say Éloïse) wants to mimic an a-transition from v to v (for some a, v, v ), then she moves from v to (v 1 , E) then to (v 2 , E) and so on until reaching a vertex (v k , E) from which she finally moves to v . Such a sequence of moves is possible provided

) is a valid sequence of moves in G (note here that we may have k = 0 in which case this sequence is replaced by (v, a, v ) and the simulation is an exact one). Note that to make this work, one has to assign every vertex in V × E to Éloïse. A symmetrical simulation is defined for Abelard.

Hence we have the following corollary of Theorem 13.

Corollary 27

Given any parity game over the ε-closure of a collapsible pushdown graph, it is decidable whether Éloïse has a winning strategy from the initial configuration. Moreover one can construct an n-CPDS with output that realizes a winning strategy for the player that wins from the initial configuration.

Proof Applying Proposition 26, one gets an equivalent parity game. It is then easy to check that if one starts with the ε-closure of a collapsible pushdown graph, the resulting graph is still a collapsible one (of same order) as the transformation only operates on the control states. Then decidability follows from the one for parity collapsible pushdown games.

Using the same techniques, one can get a result that generalizes both Corollary 25 and Corollary 27.

Corollary 28

Given game over the ε-closure of a collapsible pushdown graph equipped with an ω-regular winning condition, it is decidable whether Éloïse has a winning strategy from the initial configuration. Moreover one can construct an n-CPDS with output that realizes a winning strategy for the player that wins from the initial configuration.

CPDS graphs vs Caucal graphs

The class of ε-closure of configuration graphs of CPDS admits decidable Mu-calculus theories, as parity games are decidable from Corollary 27. Moreover this class contains the class of Caucal graphs [5] as these graphs are exactly those obtained by taking the ε-closure of the transition graphs of (non-collapsible) higher-order pushdown graphs [4]. Now recall that Caucal graphs enjoy decidable MSO theories [5], and therefore one can consider the similar problem for (ε-closure) configuration graphs of CPDS. The next result proves that the MSO theories of those graphs are not decidable in general, and this implies that the inclusion of Caucal graphs inside the class of ε-closure of configuration is a strict one.

Theorem 29 (Undecidability) MSO theories of configuration graphs of CPDS are not in general decidable. Hence the class of ε-closure of configuration of CPDS graphs strictly contains the Caucal graphs.

Proof Consider the following MSO interpretation I of the configuration graph of the 2-CPDS in Example 6.1.

* b a t b 1 * and R = 0 t a 0 ∨ 1 0 t a 0 1. We observe that the (image of the) interpretation is the following "infinite half-grid"

Note that for the A-edges, the constraint C requires that the target vertex should be in the next column to the right, while R specifies the correct row. Since the interpretation I preserves MSO decidability, and its image has an undecidable MSO theory (because the Halting Problem of Turing machines can be reduced to it), the MSO theory of the above configuration graph must be undecidable.

Conclusions and further directions

In this paper, we introduce collapsible pushdown automata and prove that they are equi-expressive with (general) recursion schemes for generating trees. This is the first automata-theoretic characterization of higher-order recursions schemes. We argue that the equi-expressivity result is significant because it acts as a bridge, enabling inter-translation between model-checking problems about trees generated by recursion scheme and solvability of games on collapsible pushdown graphs. We show (Theorem 29) that order-n CPDS are strictly more expressive then order-n pushdown systems for generating graphs.

As for further directions:

1. The most pressing open problem is whether order-n CPDA are equi-expressive with order-n PDA for generating trees. The conjecture is that the former are strictly more expressive. Specifically it is conjectured that Urzyczyn tree [2] is definable by a 2-CPDA but not by any 2-PDA.

2. Is there a finite way to represent the set of winning positions of an n-CPDS parity game (equivalently to represent the set of vertices where a given modal mu-calculus formula holds)?

3. Is there an à la Caucal definition for the ε-closure of CPDS graphs? As trees generated by n-CPDA are exactly those obtained by unravelling an n-CPDS graph, is there a class of transformations T from trees to graphs such that every (n + 1)-CPDS graph is obtained by applying a T -transformation to some tree generated by an n-CPDA. Note that a T -transformation may in general not preserve MSO decidability, but should preserve modal mu-calculus decidability of trees generated by n-CPDA.