Unboundedness and Downward Closures of HigherOrder Pushdown Automata
Matthew Hague 
Abstract: We show the diagonal problem for higherorder pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important rôle in verifying concurrent higherorder programs expressed as HOPDA or safe higherorder recursion schemes.
Recent work by Zetzsche [40] has given a new technique for computing the downward closure of classes of languages. The downward closure ↓(L) of a language L is the set of all subwords of words in L (e.g. a a is a subword of b a b a b). It is well known that the downward closure is regular for any language [19]. However, there are only a few classes of languages for which it is known how to compute this closure. In general it is not possible to compute the downward closure since it would easily lead to a solution to the halting problem for Turing machines.
However, once a regular representation of the downward closure has been obtained, it can be used in all kinds of analysis, since regular languages are well behaved under all kinds of transformations. For example, consider a system that waits for messages from a complex environment. This complex environment can be abstracted by the downward closure of the messages it sends or processes it spawns. This corresponds to a lossy system where some messages may be ignored (or go missing), or some processes may simply not contribute to the remainder of the execution. In many settings – e.g. the analysis of safety properties of certain kinds of systems – unread messages or unscheduled processes do not effect the precision of the analysis. Since many types of system permit synchronisation with a regular language, this environment abstraction can often be built into the system being analysed.
Many popular languages such as JavaScript, Python, Ruby, and even C++, include higherorder features – which are increasingly important given the popularity of eventbased programs and asynchronous programs based on a continuation or callback style of programming. Hence, the modelling of higherorder function calls is becoming key to analysing modern day programs.
A popular approach to verifying higherorder programs is that of recursion schemes and several tools and practical techniques have been developed [23, 38, 26, 24, 30, 5, 6, 34]. Recursion schemes have an automaton model in the form of collapsible pushdown automata (CPDA) [18] which generalises an order2 model called 2PDA with links [1] or, equivalently, panic automata [22]. When these recursion schemes satisfy a syntactical condition called safety, a restriction of CPDA called higherorder pushdown automata (HOPDA or nPDA for ordern HOPDA) is sufficient [29, 21]. HOPDA can be considered an extension of pushdown automata to a “stack of stacks” structure. It remains open as to whether CPDA are strictly more expressive than nondeterministic HOPDA when generating languages of words. It is known that, at order 2, nondeterministic HOPDA and CPDA generate the same word languages [1]. However, there exists a language generated by a deterministic order2 CPDA that cannot be generated by a deterministic HOPDA of any order [31].
It is well known that concurrency and firstorder recursion very quickly leads to undecidability (e.g. [33]). Hence, much recent research has focussed on decidable abstractions and restrictions (e.g. [14, 4, 20, 27, 13, 37, 28, 10, 16]). Recently, these results have been extended to concurrent versions of CPDA and recursion schemes (e.g. [35, 25, 15, 32]). Many approaches rely on combining representations of the Parikh image of individual automata (e.g. [13, 17, 16]). However, combining Parikh images of HOPDA quickly leads to undecidability (e.g. [17]). In many cases, the downward closure of the Parikh image is an adequate abstraction.
Computing downward closures appears to be a hard problem. Recently Zetzsche introduced a new general technique for classes of automata effectively closed under rational transductions – also referred to as a full trio. For these automata the downward closure is computable iff the simultaneous unboundedness problem (SUP) is decidable.
Zetzsche used this result to obtain the downward closure of languages definable by 2PDA, or equivalently, languages definable by indexed grammars [2]. Moreover, for classes of languages closed under rational transductions, Zetzsche shows that the simultaneous unboundedness problem is decidable iff the diagonal problem is decidable. The diagonal problem was introduced by Czerwiński and Martens [11]. Intuitively, it is a relaxation of the SUP that is insensitive to the order the characters are output. For a word w, let w_{a} be the number of occurrences of a in w.
Diagonal_{a1, …, aα}  ⎛ ⎝  L  ⎞ ⎠  = ∀ m . ∃ w ∈ L . ∀ 1 ≤ i ≤ α .  ⎪ ⎪  w  ⎪ ⎪  _{ai} ≥ m . 
Proof. The onlyif direction follows from Theorem 1 since given a language L ⊆ a_{1}^{∗}… a_{α}^{∗} the diagonal problem is immediately equivalent to the SUP. In the if direction, the result follows since L satisfies the diagonal problem iff ↓(L) also satisfies the diagonal problem. Since the diagonal problem is decidable for regular languages and ↓(L) is regular, we have the result.
In this work, we generalise Zetzsche’s result for 2PDA to the general case of nPDA. We show that the diagonal problem is decidable. Since HOPDA are closed under rational transductions, we obtain decidability of the simultaneous unboundedness problem, and hence a method for constructing the downward closure of a language defined by a HOPDA.
Proof. From Theorem 3 (proved in the sequel), we know that the diagonal problem for HOPDA is decidable. Thus, using Corollary 1, we can construct the downward closure of P.
This result provides an abstraction upon which new results may be based. It also has several immediate consequences:
We present our decidability proof in two stages. First we show how to decide Diagonal_{a}(P) for a single character and HOPDA P in Sections 3 and 4. In Sections 5, 6, and 7 we generalise our techniques to the full diagonal problem.
In Section 3.1 we give an outline of the proof techniques for deciding Diagonal_{a}(P). In short, the outermost stacks of an nPDA are created and destroyed using push_{n} and pop_{n} operations. These push_{n} and pop_{n} operations along a run of an nPDA are “wellbracketed” (each push_{n} has a matching pop_{n} and these matchings don’t overlap). The essence of the idea is to take a standard tree decomposition of these wellbracketed runs and observe that each branch of such a tree can be executed by an (n−1)PDA. We augment this (n−1)PDA with “regular tests” that allow it to know if, each time a branch is chosen, the alternative branch could have output some a characters. If this is true, then the (n−1)PDA outputs a single a to account for these missed characters. We prove that, although the (n−1)PDA outputs far fewer characters, it can still output an unbounded number iff the nPDA could. Hence, by repeating this reduction, we obtain a 1PDA, for which the diagonal problem is decidable since it is known how to compute their downward closures [39, 9].
In Section 6.1 we outline the generalisation of the proof to the full problem Diagonal_{a1, …, aα}(P). The key difficulty is that it is no longer enough for the (n−1)PDA to follow only a single branch of the tree decomposition: it may need up to one branch for each of the a_{1}, …, a_{α}. Hence, we define HOPDA that can output trees with a bounded number (α) of branches. We then show that our reduction can generalise to HOPDA outputting trees (relying essentially on the fact that the number of branches is bounded).
Given two words w = γ_{1} … γ_{m}∈ Σ^{∗} and w′ = σ_{1} … σ_{l}∈ Σ^{∗} for some alphabet Σ, we write w ≤ w′ iff there exist i_{1} < … < i_{m} such that for all 1 ≤ j ≤ m we have γ_{j}= σ_{ij}. Given a set of words L ⊆ Σ^{∗}, we denote its downward closure ↓(L) = {w  w ≤ w′ ∈ L}.
A Σlabelled finite tree is a tuple T = (D, λ) where Σ is a set of node labels, and D ⊂ ℕ^{∗} is a finite set of nodes that is prefixclosed, that is, η δ ∈ D implies η ∈ D, and λ : D → Σ is a function labelling the nodes of the tree.
We write ε to denote the root of a tree (the empty sequence). We also write
a  ⎡ ⎣  T_{1}, …, T_{m}  ⎤ ⎦ 
to denote the tree whose root node is labelled a and has children T_{1}, …, T_{m}. That is, we define a[T_{1}, …, T_{m}] = (D′, λ′) when for each δ we have T_{δ}= (D_{δ}, λ_{δ}) and D′ = {δη  η ∈ D_{δ}} ∪ {ε} and
λ′  ⎛ ⎝  η  ⎞ ⎠  = 
 . 
Also, let T[a] denote the tree ({ε}, λ) where λ(ε) = a. A branch in T = (D, λ) is a sequence of nodes of T, η_{1} ⋯ η_{n}, such that η_{1} = є, η_{n} = δ_{1} δ_{2} ⋯ δ_{n−1} is maximal in D, and η_{j+1} = η_{j} δ_{j} for each 1 ≤ j ≤ n−1.
HOPDA are a generalisation of pushdown systems to a stackofstacks structure. An ordern stack is a stack of order(n−1) stacks. An ordern push operation pushes a new order(n−1) stack onto the stack that is a copy of the existing topmost order(n−1) stack. Rewrite operations update the character that is at the top of the topmost stacks.

Stacks are written with the top part of the stack to the left. We define several operations.

and set
Ops_{n} =  ⎧ ⎨ ⎩  rew_{γ}  ⎪ ⎪  γ ∈ Γ  ⎫ ⎬ ⎭  ⋃  ⎧ ⎨ ⎩  push_{k}, pop_{k}  ⎪ ⎪  1 ≤ k ≤ n  ⎫ ⎬ ⎭ 
to be the set of ordern stack operations.
For example

We write (p, γ) —^{a}→ (p′, o) for a rule (p, γ, a, o, p′) ∈ R.
A configuration of an nPDA is a tuple ⟨ p, s ⟩ where p ∈ P and s is an ordern stack over Γ. We have a transition ⟨ p, s ⟩ —^{a}→ ⟨ p′, s′ ⟩ whenever we have (p, γ) —^{a}→ (p′, o), top_{1}(s) = γ, and s′ = o(s).
A run over a word w ∈ Σ^{∗} is a sequence of configurations c_{0} —^{a1}→ ⋯ —^{am}→ c_{m} such that the word a_{1}…a_{m} is w. It is an accepting run if c_{0} = ⟨ p_{in}, [[ γ_{in} ]] ⟩ — where we write [[ γ ]] for [⋯[γ]_{1}⋯]_{n} — and where c_{m}= ⟨ p, s ⟩ with p ∈ F. Furthermore, for a set of configurations C, we define
Pre_{P}^{∗}  ⎛ ⎝  C  ⎞ ⎠ 
to be the set of configurations c such that there is a run over some word from c to c′ ∈ C. When C is defined as the language of some automaton A accepting configurations, we abuse notation and write Pre_{P}^{∗}(A) instead of Pre_{P}^{∗}(L(A)).
For convenience, we sometimes allow a set of characters to be output instead of only one. This is to be interpreted as outputing each of the characters in the set once (in some arbitrary order). We also allow sequences of operations o_{1}; …; o_{m} in the rules instead of single operations. When using sequences we allow a test operation γ? that only allows the sequence to proceed if the top_{1} character of the stack is γ. All of these extensions can be encoded by introducing intermediate control states.
We will need to represent sets of stacks. To do this we will use automata to recognise stacks. We define the stack automaton model of Broadbent et al. [8] restricted to HOPDA rather than CPDA. We will sometimes call these bottomup stack automata or simply automata. The automata operate over stacks interpreted as words, hence the opening and closing braces of the stacks appear as part of the input. We annotate these braces with the order of the stack the braces belong to. Let Γ_{[]} = {[_{n−1},…,[_{1}, ]_{1},…,]_{n−1}} ⊎ Γ. Note, we don’t include [_{n}, ]_{n} since these appear exclusively at the start and end of the stack.
Representing higher order stacks as a linear word graph, where the start of an orderk stack is an edge labelled [_{k} and the end of an orderk stack is an edge labelled ]_{k}, a run of a bottomup stack automaton is a labelling of the nodes of the graph with states in Q such that
The run is accepting if the leftmost (initial) node is labelled by q ∈ Q_{F}. An example run over the word graph representation of [ [ [γ σ]_{1}[σ]_{1} ]_{2} [ [σ]_{1} ]_{2} ]_{3} is given in Figure 1.
Let L(A) be the set of stacks with accepting runs of A. Sometimes, for convenience, if we have a configuration c = ⟨ p, s ⟩ of a HOPDA, we will write c ∈ L(A) when s ∈ L(A).
We assume Σ = {a, ε} and use b to range over Σ. This can be obtained by simply replacing all other characters with ε. We also assume that all rules of the form (p, γ) —^{b}→ (p′, o) with o = push_{n} or o = pop_{n} have b = ε. We can enforce this using intermediate control states to first apply o in one step, and then in another output b (the stack operation on the second step will be rew_{γ} where γ is the current top character). We start with an outline of the proof, and then explain each step in detail.
For convenience, we assume acceptance is by reaching a unique control state in F with an empty stack (i.e. the lowermost stack was removed with a pop_{n} and F = {p_{f}}). This can easily be obtained by adding a rule to a new accepting state whenever we have a rule leading to a control state in F. From this new state we can loop and perform pop_{n} operations until the stack is empty.
The approach is to take an nPDA P and produce an (n−1)PDA P_{−1} that satisfies the diagonal problem iff P does. The idea behind this reduction is that an (accepting) run of P can be decomposed into a tree with outdegree at most 2: each push_{n} has a matching pop_{n} that brings the stack back to be the same as it was before the push_{n}; we cut the run at the pop_{n} and hang the tail next to the push_{n} and repeat this to form a tree from a run. This is illustrated in Figure 2 where nodes are labelled by their configurations, and the push_{n} and pop_{n} points are marked. The dotted arcs connect nodes matched by their pushes and pops – these nodes have the same stacks. Notice that at each branching point, the left and right subtrees start with the same order(n−1) stacks on top. Notice also that for each branch, none of its transitions remove the topmost order(n−1) stack. Hence, we can produce an (n−1)PDA that picks a branch of this tree decomposition to execute and only needs to keep track of the topmost order(n−1) stack of the nPDA. When picking a branch to execute, the (n−1)PDA outputs a single a if the branch not chosen could have output some a characters. We prove that this is enough to maintain unboundedness.
In more detail, we perform the following steps.
Diagonal_{a}  ⎛ ⎝  P  ⎞ ⎠  ⇐⇒ Diagonal_{a}  ⎛ ⎝  P′  ⎞ ⎠  . 
The (n−1)PDA with tests P_{−1} will simulate the nPDA P in the following way.
Although P_{−1} will output far fewer a characters than P (since it does not execute the full run), we show that it still outputs enough as for the language to remain unbounded.
We thus have the following theorem.
Proof. We construct via Lemma 2 an (n−1)PDA P′ such that Diagonal_{a}(P) iff Diagonal_{a}(P′). We repeat this step until we have a 1PDA. It is known that Diagonal_{a}(P) for an 1PDA is decidable since it is possible to compute the downward closure [39, 9].
When executing a branch of the tree decomposition, to be able to ensure the branch is correct and whether we should output an extra a we need to know how the system could have behaved on the skipped branch. To do this we add tests to the HOPDA that allow it to know if the current stack belongs to a given regular set. We show in the following sections that the properties required for our reduction can be represented as regular sets of stacks. Although we take Broadbent et al.’s logical reflection as the basis of our proof, HOPDA with tests can be seen as a generalisation of pushdown systems with regular valuations due to Esparza et al. [12].
R ⊆ P × Γ ×  ⎧ ⎨ ⎩  A_{1}, …, A_{m}  ⎫ ⎬ ⎭  × Σ × Ops_{n} × P 
We write (p, γ, A_{i}) —^{b}→ (p′, o) for (p, γ, A_{i}, b, o, p′) ∈ R. We have a transition ⟨ p, s ⟩ —^{b}→ ⟨ p′, s′ ⟩ whenever (p, γ, A_{i}) —^{b}→ (p′, o) ∈ R and top_{1}(s) = γ, s ∈ L(A_{i}), and s′ = o(s).
We know from Broadbent et al. that these tests do not add any extra power to HOPDA. Intuitively, we can embed runs of the automata into the stack during runs of the HOPDA.
Proof. This is a straightforward adaptation of Broadbent et al. [8]. A more general theorem is proved in Theorem 1.
When the HOPDA is in a configuration of the form ⟨ p, [s]_{n} ⟩ – i.e. the outermost stack contains only a single order(n−1) stack – we require the HOPDA to be able to know whether,
Given P, we first augment P to record whether an a has been produced. This can be done simply by recording in the control state whether a has been output.
P_{a} =  ⎛ ⎝  P ⋃ P_{a}, Σ, Γ, R ⋃ R_{a}, F ⋃ F_{a}, p_{in}, γ_{in}  ⎞ ⎠ 

It is easy to see that P and P_{a} accept the same languages, and that P_{a} is only in a control state p_{a} if an a has been output.
Fix some P = (P, Σ, Γ, R, F) and P_{a} = (P_{a}, Σ, Γ, R_{a}, F_{a}). To obtain a HOPDA with tests, we need, for each p_{1}, p_{2} ∈ P the following automata. Note, we define these automata to accept order(n−1) stacks since they will be used in an (n−1)PDA with tests.
To do this we will use a reachability result due to Broadbent et al. that appeared in ICALP 2012 [7]. This result uses an automata representation of sets of configurations. However, these automata are slightly different in that they read full configurations “top down”, whereas the automata of Theorem 2 (Removing Tests) read only stacks “bottom up”.
It is known that these two representations are effectively equivalent, and that both form an effective boolean algebra [8, 7]. In particular, for a topdown automaton A and a control state p we can build a bottomup stack automaton B such that ⟨ p, s ⟩ ∈ L(A) iff s ∈ L(B) and vice versa. We recall the reachability result.
Let A_{p, γ} be a topdown automaton accepting configurations of the form ⟨ p, [s]_{n} ⟩ where top_{1}(s) = γ. Next, let
A_{p} = 
 A_{p′, γ} 
and
A_{p}^{a}= 
 A_{p′a, γ} 
I.e. A_{p} and A_{p}^{a} accept configurations of P_{a} from which it is possible to perform a pop_{n} operation to p and reach the empty stack.
It is easy to see both A_{p1, p2} and A_{p1, p2}^{a} are regular and representable by bottomup automata since both
Pre_{P}^{∗}  ⎛ ⎝  A_{p2}  ⎞ ⎠  and Pre_{Pa}^{∗}  ⎛ ⎝  A_{p2}^{a}  ⎞ ⎠ 
are regular from Theorem 3, and bottomup and topdown automata are effectively equivalent. To enforce only stacks of the form [s]_{n} we intersect with an automaton A_{1} accepting all stacks containing a single order(n−1) stack (this is clearly regular).
We are now ready to complete the reduction. Correctness is shown in Section 4. Let A_{tt} be the automaton accepting all stacks. In the following definition, a control state (p_{1}, p_{2}) means that we are currently in control state p_{1} and are aiming to empty the stack on reaching p_{2}, and the rules R_{sim} simulate all operations apart from push_{n} and pop_{n} directly, R_{fin} detect when the run is accepting, R_{push} follow the push branch of the tree decomposition, using tests to ensure the existence of the pop branch, and R_{pop} follow the pop branch of the tree decomposition, also using tests to check the existence of the push branch.
P_{−1} =  ⎛ ⎝ 
 ⎞ ⎠ 

⎛ ⎝ 
 ⎞ ⎠  —^{b}→  ⎛ ⎝ 
 ⎞ ⎠ 
⎛ ⎝ 
 ⎞ ⎠  —^{ε}→  ⎛ ⎝  f, rew_{γ}  ⎞ ⎠ 
⎛ ⎝ 
 ⎞ ⎠  —^{ε}→  ⎛ ⎝ 
 ⎞ ⎠ 
⎛ ⎝ 
 ⎞ ⎠  —^{a}→  ⎛ ⎝ 
 ⎞ ⎠ 
⎛ ⎝ 
 ⎞ ⎠  —^{ε}→  ⎛ ⎝ 
 ⎞ ⎠ 
⎛ ⎝ 
 ⎞ ⎠  —^{a}→  ⎛ ⎝ 
 ⎞ ⎠ 
In the next section, we show the reduction is correct.
To complete the reduction, we convert the HOPDA with tests into a HOPDA without tests.
Diagonal_{a}  ⎛ ⎝  P  ⎞ ⎠  ⇐⇒ Diagonal_{a}  ⎛ ⎝  P′  ⎞ ⎠  . 
Proof. From Definition 4 (P_{−1}) and Lemma 1 (Correctness of P_{−1}), we obtain from P an (n−1)PDA with tests P_{−1} satisfying the conditions of the lemma. To complete the proof, we invoke Theorem 2 (Removing Tests) to find P′ as required.
This section is dedicated to the proof of Lemma 1 (Correctness of P_{−1}).
The idea of the proof is that each run of P can be decomposed into a tree: each push_{n} operation creates a node whose left child is the run up to the matching pop_{n}, and whose right child is the run after the matching pop_{n}. All other operations create a node with a single child which is the successor configuration.
Each branch of such a tree corresponds to a run of P_{−1}. To prove that P_{−1} can output an unbounded number of as we prove that any tree containing m edges outputting a must have a branch along which P_{−1} would output log(m) a characters. Thus, if P can output an unbounded number of a characters, so can P_{−1}.
Given a run
ρ = c_{0} —^{b1}→ c_{1} —^{b2}→ ⋯ —^{bm}→ c_{m} 
of P where each push_{n} operation has a matching pop_{n}, we can construct a tree representation of ρ inductively. That is, we define Tree(c) = T[ε] for the singleconfiguration run c, and, when
ρ = c —^{b}→ ρ′ 
where the first rule applied does not contain a push_{n} operation, we have
Tree  ⎛ ⎝  ρ  ⎞ ⎠  = b  ⎡ ⎣ 
 ⎤ ⎦ 
and, when
ρ = c_{0} —^{ε}→ ρ_{1} —^{ε}→ ρ_{2} 
with c_{1} being the first configuration of ρ_{2} and where the first rule applied in ρ contains a push_{n} operation, c_{0} = ⟨ p, s ⟩ and c_{1} = ⟨ p′, s ⟩ for some p, p′, s and there is no configuration in ρ_{1} of the form ⟨ p″, s ⟩, then
Tree  ⎛ ⎝  ρ  ⎞ ⎠  = ε  ⎡ ⎣ 
 ⎤ ⎦  . 
An accepting run of P has the form ρ —^{ε}→ c where ρ has the property that all push_{n} operations have a matching pop_{n} and the final transition is a pop_{n} operation to c = ⟨ p, []_{n} ⟩ for some p ∈ F. Hence, we define the tree decomposition of an accepting run to be
Tree  ⎛ ⎝  ρ —^{ε}→ c  ⎞ ⎠  = ε  ⎡ ⎣ 
 ⎤ ⎦  . 
In the above tree decomposition of runs, the tree branches at each instance of a push_{n} operation. This mimics the behaviour of P_{−1}, which performs such branching nondeterministically. Hence, given a run ρ of P, each branch of Tree(ρ) corresponds to a run of P_{−1}.
We formalise this intuition in the following section. In this section, we assign scores to each subtree T of Tree(ρ). These scores correspond directly to the largest number of a characters that P_{−1} can output while simulating a branch of T.
Note, in the following definition, we exploit the fact that only nodes with exactly one child may have a label other than ε. We also give a general definition applicable to trees with outdegree larger than 2. This is needed in the simultaneous unboundedness section. For the moment, we only have trees with outdegree at most 2.
Let
 = 
 and 
 = 
 . 
Then,
Score  ⎛ ⎝  T  ⎞ ⎠  = 

We then have the following lemma for trees with outdegree 2.
Score  ⎛ ⎝  T  ⎞ ⎠  ≥ log  ⎛ ⎝  m  ⎞ ⎠ 
Proof. The proof is by induction over m. In the base case m = 1 and there is a single node η in T labelled a. By definition, the subtree T′ rooted at η has Score(T′) = 1. Since the score of a tree is bounded from below by the score of any of its subtrees, we have Score(T) ≥ log(1) as required.
Now, assume m > 1. Find the smallest subtree T′ of T containing m nodes labelled a. We necessarily have either
In case (1) we have by induction
Score  ⎛ ⎝  T′  ⎞ ⎠  = 1 + log  ⎛ ⎝  m − 1  ⎞ ⎠  ≥ log  ⎛ ⎝  m  ⎞ ⎠ 
In case (2) we have
Score  ⎛ ⎝  T′  ⎞ ⎠  = max  ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠  . 
We pick whichever of T_{1} and T_{2} has the most nodes labelled a. This tree has at least ⌈m / 2⌉ nodes labelled a. Note, since both trees contain nodes labelled a, the righthand side of the addition is always 1. Hence, we need to show
log  ⎛ ⎝ 
 ⎞ ⎠  + 1 ≥ log  ⎛ ⎝  m  ⎞ ⎠ 
which follows from

By our choice of T′ we thus have Score(T) = Score(T′) ≥ log(m) as required.
Proof. Let p_{f} be the final (accepting) control state of P and let T = Tree(ρ). We begin at the root node of T, which corresponds to the initial configuration of ρ. Let ⟨ p, [s]_{n} ⟩ be this initial configuration and let ⟨ (p, p_{f}), s ⟩ be the initial configuration of P_{−1}.
Thus, assume we have a node η of T, with a corresponding configuration c = ⟨ p, s ⟩ of P and configuration c_{−1} = ⟨ (p, p_{pop}), top_{n}(s) ⟩ of P_{−1} and a run ρ_{−1} of P_{−1} ending in c_{−1} and outputting (m − Score(T′)) a characters where T′ is the subtree of T rooted at η. The subtree T′ corresponds to a subrun ρ′ of ρ where the transition immediately following ρ′ is a pop_{n} transition to a control state p_{pop}.
There are two cases when we are dealing with internal nodes.
In this case there is a transition c —^{b}→ c′ via a rule (p, γ) —^{b}→ (p′, o) where o ∉ {push_{n}, pop_{n}}. Hence, we have the rule ((p, p_{pop}), γ, A_{tt}) —^{b}→ ((p′, p_{pop}), o) in P_{−1} and thus we can extend ρ_{−1} with a transition c_{−1} —^{b}→ c′_{−1} via this rule where ρ_{−1}, c′ and c′_{−1} maintain the assumptions above.
In this case we have that T′ corresponds to a subrun
c —^{ε}→ ρ_{1} —^{ε}→ ρ_{2} 
of ρ. The transition from c to the beginning of ρ_{1} is via a rule r_{1} = (p, γ) —^{ε}→ (p_{1}, push_{n}) and the transition from the end of ρ_{1} to the start of ρ_{2} is via a rule r_{2} = (p_{2}, γ_{1}) —^{ε}→ (p_{3}, pop_{n}). Moreover, from the definition of the decomposition, the final configuration in ρ_{2} is followed in ρ by a pop rule r_{3} = (p_{4}, γ_{2}) —^{ε}→ (p_{pop}, pop_{n}).
There are two further cases depending on whether the score of T′ is derived from the score of T_{1} or T_{2}.
If an a is output, we have c_{−1} ∈ L(A_{p3, ppop}^{a}) and Score(T′) − Score(T_{1}) = 1. We can extend ρ via an application of the rule ((p, p_{pop}), γ, A_{p3, ppop}^{a}) —^{a}→ ((p_{1}, p_{3}), rew_{γ}) that exists in P_{−1} since c_{−1} ∈ L(A_{p3, ppop}^{a}). This transition maintains the property on the stacks since the push_{n} copies the topmost stack, hence P_{−1} does not need to change its stack. It maintains the property on the scores since it outputs a, accounting for the part of the score contributed by T_{2}. Finally, the condition on control states is satisfied since the second component is set to p_{2}.
If an a is not output, then the case is similar to the above, except T_{2} does not contribute to the score, we have c_{−1} ∈ L(A_{p3, ppop}), and the transition of P_{−1} is labelled ε instead of a.
If an a is output, we have c_{−1} ∈ L(A_{p1, p3}^{a}) and Score(T′) − Score(T_{2}) = 1. We can extend ρ via an application of the rule ((p, p_{pop}), γ, A_{p1, p3}^{a}) —^{a}→ ((p_{3}, p_{pop}), rew_{γ}) that exists in P_{−1} since c_{−1} ∈ L(A_{p1, p3}^{a}) This transition maintains the property on the stacks since the stack after the pop_{n} is identical to the stack before the push_{n}, hence P_{−1} does not need to change its stack. It maintains the property on the scores since it outputs a, accounting for the part of the score contributed by T_{1}. Finally, the condition on control states is satisfied since the second component is unchanged.
If an a is not output, then the case is similar to the above, except T_{1} does not contribute to the score, we have c_{−1} ∈ L(A_{p1, p3}) and the transition of P_{−1} is labelled ε instead of a.
Finally, we reach a leaf node η with a run outputting the required number of as. We need to show that the run constructed is accepting. Let η′ be the first ancestor of η that contains η in its leftmost subtree. Let T′ be the subtree rooted at η′. This tree corresponds to a subrun ρ′ of ρ that is followed immediately by a pop_{n} rule (p, γ) —^{ε}→ (p_{pop}, pop_{n}). Moreover, we have ((p, p_{pop}), γ, A_{tt}) —^{ε}→ (f, rew_{γ}) with which we can complete the run of P_{−1} as required.
Finally, we need to show that each accepting run of P_{−1} gives rise to an accepting run of P containing at least as many as.
Proof. Let p_{f} be the unique accepting conrol state of P. Take an accepting run ρ_{−1} of P_{−1}. We show that there exists a corresponding run ρ of P outputting at least as many as.
Let
c_{0} —^{b}→ ⋯ —^{b}→ c_{m}—^{ε}→ ⟨ f, s ⟩ 
for some s be the accepting run of P_{−1}. We define inductively for each 0 ≤ i ≤ m a pair of runs ρ_{1}^{i}, ρ_{2}^{i} of P such that
Initially we have c_{0} = ⟨ (p_{in}, p_{f}), s ⟩ and s = [[ γ_{in} ]]. We define ρ_{1}^{0} = ⟨ p_{in}, [s]_{n} ⟩ and ρ_{2}^{0} = ⟨ p_{f}, []_{n} ⟩ which immediately satisfy the required conditions.
Assume we have ρ_{1}^{i} and ρ_{2}^{i} as required. We show how to obtain ρ_{1}^{i+1} and ρ_{2}^{i+1}. There are several cases depending on the rule used on the transition c_{i}—^{bi+1}→ c_{i+1}. Let c_{i}= ⟨ (p, p_{pop}), s ⟩, the final configuration of ρ_{1}^{i} be ⟨ p, [s s_{1} … s_{l}]_{n} ⟩ and the first configuration of ρ_{2}^{i} be ⟨ p_{pop}, [s_{1} … s_{l}]_{n} ⟩.
The required conditions are inherited from ρ_{1}^{i} and ρ_{2}^{i} since o only changes the top_{n} stack, the final configuration of ρ_{2}^{i+1} is the same as ρ_{2}^{i}, p_{pop} is not changed, and the rule of P outputs an a iff the rule of P_{−1} does.
Since the final configuration of ρ_{1}^{i+1} is ⟨ p′, [s s s_{1} … s_{l}]_{n} ⟩ it is easy to check the required correspondence with the first configuration ⟨ p′_{pop}, [s s_{1} … s_{l}]_{n} ⟩ of ρ_{2}^{i+1}.
The remaining conditions are immediate since no a is output and the final configuration of ρ_{2}^{i+1} is the same as ρ_{2}^{i}.
To verify that the properties hold, we observe that c_{i+1} = ⟨ (p_{2}, p_{pop}), s ⟩, and ρ_{1}^{i+1} ends with ⟨ p_{2}, [s s_{1} … s_{l}]_{n} ⟩ and ρ_{2}^{i+1} still begins with ⟨ p_{pop}, [s_{1} … s_{l}]_{n} ⟩ and has the required final configuration. The property on the number of as holds since the rule of P_{−1} did not output an a.
Finally, when we reach i = m we have from the final transition of the run of P_{−1} that there is a rule (p, γ) —^{ε}→ (p_{pop}, pop_{n}). We combine ρ_{1}^{m} and ρ_{2}^{m} with this pop transition, resulting in an accepting run of P that outputs at least as many a characters as the run of P_{−1}.
We generalise the previous result to the full diagonal problem. Naïvely, the previous approach cannot work. Consider the HOPDA executing
push_{1}^{m}; push_{n}; pop_{1}^{m}; pop_{n}; pop_{1}^{m} 
where the first sequence of pop_{1} operations output a_{1} and the second sequence output a_{2}.
The corresponding run trees are of the form given in Figure 3. In particular, P_{−1} can only choose one branch, hence all runs of P_{−1} produce a bounded number of a_{1}s or a bounded number of a_{2}s. They cannot be simultaneously unbounded.
For P_{−1} to be able to output both an unbounded number of a_{1} and a_{2} characters, it must be able to output two branches of the tree. To this end, we define a notion of αbranch HOPDA, which output trees with up to α branches. We then show that the reduction from nPDA to (n−1)PDA can be generalised to αbranch HOPDA.
We define nPDA outputting trees with at most α branches, denoted (n, α)PDA. Note, an nPDA that outputs a word is an (n, 1)PDA. Indeed, any (n, α)PDA is also an (n, α′)PDA whenever α ≤ α′.
We use the notation (p, γ) —^{b}→ (p_{1}, …, p_{m}, o) to denote a rule (p, γ, b, o, p_{1}, …, p_{m}) ∈ R. Intuitively, such a rule generates a node of a tree with m children. The purpose of the mapping θ is to bound the number of branches that this tree may have. Hence, at each branching rule, the quota of branches is split between the different subtrees. The existence of such a mapping implies this information is implicit in the control states and an (n, α)PDA can only output trees with at most α branches.
From the initial configuration c_{0} = ⟨ p_{in}, [[ γ_{in} ]] ⟩ a run of an (n, α)PDA is a tree T = (D, λ) whose nodes are labelled with nPDA configurations, and generates an output tree T′ = (D, λ′) whose nodes are labelled with symbols from the output alphabet. Precisely
The run is accepting if for all leaf nodes η we have λ(η) = ⟨ p, []_{n} ⟩ and p ∈ F. Let L(P) be the set of output trees of P.
Given an output tree T we write T_{a} to denote the number of nodes labelled a in T. For an (n, α)PDA P, we define
Diagonal_{a1, …, aα}  ⎛ ⎝  P  ⎞ ⎠  = 
∀ m . ∃ T ∈ L  ⎛ ⎝  P  ⎞ ⎠  . ∀ 1 ≤ i ≤ α .  ⎪ ⎪  T  ⎪ ⎪  _{ai} ≥ m . 
Given an (n, α)PDA P we construct an (n−1, α)PDA P_{−1} such that
Diagonal_{a1, …, aα}  ⎛ ⎝  P  ⎞ ⎠  ⇐⇒ Diagonal_{a1, …, aα}  ⎛ ⎝  P_{−1}  ⎞ ⎠  . 
Moreover, we show Diagonal_{a1, …, aα}(P) is decidable for a (0, α)PDA (i.e. a regular automaton outputting an αbranch tree) P.
For simplicity, we assume for all rules (p, γ) —^{b}→ (p_{1}, …, p_{m}, o) if m > 1 then o = rew_{γ} (i.e. the stack is unchanged). Additionally we have b = ε.
We also make analogous assumptions to the single character case. That is, we assume Σ = {a_{1}, …, a_{α}, ε} and use b to range over Σ. Moreover, all rules of the form (p, γ) —^{b}→ (p′, o) with o = push_{n} or o = pop_{n} have b = ε. Finally, we assume acceptance is by reaching a unique control state in F with an empty stack.
We briefly sketch the intuition behind the algorithm. We illustrate the reduction from (n, α)PDA to (n−1, α)PDA in Figure 4.
As before, we instrument our HOPDA with tests. Removing these tests requires a simple adaptation of Broadbent et al. [8].
We use the notation (p, γ, A) —^{b}→ (p_{1}, …, p_{m}, o) to denote a rule (p, γ, A, b, o, p_{1}, …, p_{m}) ∈ R.
From the initial configuration c_{0} = ⟨ p_{in}, [[ γ_{in} ]] ⟩ a run of an (n, α)PDA with tests is a tree T = (D, λ) and generates an output tree ρ = (D, λ′) where
The run is accepting if for all leaf nodes η we have λ(η) = ⟨ p, []_{n} ⟩ and p ∈ F. Let L(P) be the set of output trees of P.
Proof. This is a straightforward adaptation of Broadbent et al. [8]. Let the (n, α)PDA with tests be P = (P, Σ, Γ, R, F, p_{in}, γ_{in}, θ) with test automata A_{1}, …, A_{m}. We build an (n, α)PDA that mimics P almost directly. The only difference is that each character γ appearing in the stack is replaced by
⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠  . 
For each test A we have a vector of functions
 _{=}  ⎛ ⎝  τ_{1}, …, τ_{n}  ⎞ ⎠  . 
The function τ_{k} : Q → Q intuitively describes runs of A from the bottom of top_{k+1}(s) to the top of pop_{k}(top_{k+1}(s)). Thus, we can reconstruct an entire run over pop_{1}(s) from initial state q as
q′ = τ_{1}  ⎛ ⎝ 
 ⎞ ⎠ 
and then we can consult Δ to complete the run by adding the effect of reading top_{1}(s).
Thus, let A_{i}= (Q_{i}, Γ_{[]}, q_{in}^{i}, Δ_{i}, Q_{F}^{i}). We define
P^{T} =  ⎛ ⎝  P, Σ, Γ^{T}, R^{T}, F, p_{in}, γ_{in}^{T}, θ  ⎞ ⎠ 
where
Γ^{T} =  ⎧ ⎨ ⎩ 
 ⎪ ⎪ ⎪ 
 ⎫ ⎬ ⎭ 
and R^{T} is the smallest set of rules of the form
⎛ ⎝  p, γ^{T}  ⎞ ⎠  —^{b}→  ⎛ ⎝ 
 ⎞ ⎠ 
where γ^{T} = (γ, τ_{1}, …, τ_{m}) and (p, γ, A_{i}) —^{b}→ (p_{1}, …, p_{l}, o) ∈ R and Accepts(γ, τ_{i}, Δ_{i}, q_{in}^{i}, Q_{F}^{i}) and we define

where Δ(q, [_{n} ⋯ [_{1} γ) is shorthand for the repeated application of Δ on γ then [_{1}, back to [_{n}, and we define Update(o, γ^{T}) = o^{T} following the cases below. Let γ^{T} = (γ, τ_{1}, …, τ_{m}).
 _{i} =  ⎛ ⎝  τ_{1}, …, τ_{k−1}, τ_{k}′, τ_{k+1}, … τ_{n}  ⎞ ⎠ 
τ_{k}′  ⎛ ⎝  q  ⎞ ⎠  = τ_{k}  ⎛ ⎝ 
 ⎞ ⎠  . 
o^{T} = pop_{o}; 
 ?; rew 

 _{i}″ =  ⎛ ⎝  τ_{1}′, …, τ_{k−1}′, τ_{k}, … τ_{n}  ⎞ ⎠  . 
Finally, we set γ_{in}^{T} = (γ_{in}, τ_{1}, …, τ_{m}) where for each i we have τ_{i} = (τ_{1}, …, τ_{n}) such that for each k we have τ_{k}(q) = Δ(q, ]_{k} ⋯ ]_{n}).
Previously we built automata A_{p1, p2} to indicate that from p_{1}, the current top stack could be removed, arriving at p_{2}. This is fine for words, however, we now have αbranch trees. It is no longer enough to specify a single control state: the top stack may be popped once on each branch of the tree, hence for a control state p we need to recognise configurations with control state p from which there is a run tree where the leaves of the trees are labelled with configurations with control states p_{1}, …, p_{m} and empty stacks. Moreover we need to recognise the set O of characters output by the run tree. More precisely, for these automata we write
A_{p,p1,…,pm}^{O} 
where θ(p) ≥ θ(p_{1}) + ⋯ + θ(p_{m}) and O ⊆ {a_{1}, …, a_{α}}. We have s ∈ L(A_{p,p1,…,pm}^{O}) iff there is a run tree T with the root labelled ⟨ p, [s]_{n} ⟩ and m leaf nodes labelled ⟨ p_{1}, []_{n} ⟩, …, ⟨ p_{m}, []_{n} ⟩ respectively. Moreover, we have a ∈ O iff the corresponding output tree T′ has T′_{a} > 0.
To construct the required stack automata, we need to do reachability analysis of (n, α)PDA. We show that such analyses can be rephrased in terms of alternating higherorder pushdown systems (HOPDS), for which the required algorithms are already known [7]. Note, we refer to these machines as “systems” rather than “automata” because they do not output a language.
R ⊆  ⎛ ⎝  P × Γ × Ops_{n} × P  ⎞ ⎠  ⋃  ⎛ ⎝  P × Γ × 2^{P}  ⎞ ⎠ 
We write (p, γ) → (p, o) to denote (p, γ, o, p) ∈ R and (p, γ) → p_{1}, …, p_{m} to denote (p, γ, {p_{1}, …, p_{m}}) ∈ R.
An run of an alternating HOPDS may split into several configurations, each of which must reach a target state. Hence, the branching of the alternating HOPDS mimics the branching of the (n, α)PDA. Given a set C of configurations, we define Pre_{P}^{∗}(C) to be the smallest set C′ such that

In order to use standard results to obtain A_{p,p1,…,pm}^{O} we construct an alternating HOPDS P_{⋄} and automaton A such that checking c ∈ Pre_{P⋄}^{∗}(A) for a suitably constructed c allows us to check whether s ∈ L(A_{p,p1,…,pm}^{O}).
The alternating HOPDS P_{⋄} will mimic the branching of P with alternating transitions^{1} (p, γ) → p_{1}, …, p_{m} of P_{⋄}. It will maintain in its control states information about which characters have been output, as well as which control states should appear on the leaves of the branches. This final piece of information prevents all copies of the alternating HOPDS from verifying the same branch of P.
P_{⋄} =  ⎛ ⎝  P_{⋄}, Γ, R_{⋄}  ⎞ ⎠ 
P_{⋄} =  ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ 
 ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ 
 ⎫ ⎪ ⎪ ⎬ ⎪ ⎪ ⎭ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{b}→  ⎛ ⎝  p′, o  ⎞ ⎠  ∈ R 
⎛ ⎝ 
 ⎞ ⎠  →  ⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p_{1}, …, p_{m}, rew_{γ}  ⎞ ⎠  ∈ R 
⎛ ⎝ 
 ⎞ ⎠  → 

In the above definition, the permutation condition ensures that the target control states are properly distributed amongst the newly created branches.
⟨ 
 , 
 ⟩ ∈ Pre_{P⋄}^{∗}  ⎛ ⎝  A  ⎞ ⎠ 
L  ⎛ ⎝  A  ⎞ ⎠  =  ⎧ ⎨ ⎩ 
 ⎪ ⎪ ⎪ 
 ⎫ ⎬ ⎭  . 
Proof. First take s ∈ L(A_{p,p1,…,pm}^{O}) and the run tree witnessing this membership. We can move down the tree, maintaining a frontier c_{1}, …, c_{l} and building a tree witnessing that ⟨ (p, O, p_{1}, …, p_{m}), [s]_{n} ⟩ ∈ Pre_{P⋄}^{∗}(A). Initially we have the frontier ⟨ p, [s]_{n} ⟩ and the initial configuration ⟨ (p, O, p_{1}, …, p_{m}), [s]_{n} ⟩.
Hence, take a configuration c = ⟨ p′, s′ ⟩ from the frontier and corresponding configuration c′ = ⟨ (p′, O′, p′_{1}, …, p′_{i}), s′ ⟩. If the rule applied to c is not a branching rule, we simply take the matching rule of P_{⋄} and apply it to c′. Note, that if the rule output b we remove b from O′. Hence, O′ contains only characters that have not been output on the path from the initial configuration.
If the rule applied is branching, that is (p′, γ) —^{ε}→ (p″_{1}, …, p″_{j}, rew_{γ}) then we apply the rule
⎛ ⎝ 
 ⎞ ⎠  → 

where p′_{1}, …, p′_{i} is a permutation of p_{1}^{1}, …, p_{i1}^{1}, … p_{1}^{j}, …, p_{ij}^{m} and O = O_{1} ∪ ⋯ ∪ O_{m}. These partitions are made in accordance with the distribution of the leaves and outputs of the run tree of P. I.e. if a control state p″ appears on the i′th subtree, then it should appear in the i′th target state of P_{⋄}. Similarly, if the i′th subtree outputs an b ∈ O, then b should be placed in O_{i′}. Applying this alternating transition creates a matching configuration for each new branch in the frontier.
We continue in this way until we reach the leaf nodes of the frontier. Each leaf ⟨ p′, s ⟩ has a matching ⟨ (p′, ∅, p′), s ⟩ and hence is in L(A). Thus, we have witnessed ⟨ (p, O, p_{1}, …, p_{m}), [s]_{n} ⟩ ∈ Pre_{P⋄}^{∗}(A) as required.
To prove the other direction, we mirror the previous argument, showing that the witnessing tree for P_{⋄} can be used to build a run tree of P.
It is known that Pre_{P}^{∗}(A) is computable for alternating HOPDS.
Hence, we can now build A_{p,p1,…,pm}^{O} from the control state p and topdown automaton representation of Pre_{P⋄}^{∗}(A) since we can effectively translate from topdown to bottomup stack automata.
We generalise our reduction to (n, α)PDA. Let A_{tt} be the automata accepting all configurations. Note, in the following definition we allow all transitions (including branching) to be labelled by sets of output characters. To maintain our assumed normal form we have to replace these transitions using intermediate control states to ensure all branching transitions are labelled by ε and all transitions labelled O are replaced by a sequence of transitions outputting a single instance of each character in O.
The construction follows the intuition of the single character case, but with a lot more bookkeeping. Given an (n, α)PDA P we define an (n−1, α)PDA with tests P_{−1} such that P satisfies the diagonal problem iff P_{−1} also satisfies the diagonal problem. The main control states of P_{−1} take the form
⎛ ⎝  p, p_{1}, …, p_{m}, O, B  ⎞ ⎠ 
where p, p_{1}, …, p_{m} are control states of P and both O and B are sets of output characters. We explain the purpose of each of these components.
We will define P_{−1} to generate up to m branches of the tree decomposition of a run of P. In particular, for each of the characters a ∈ {a_{1}, …, a_{α}} there will be a branch of the run of P_{−1} responsible for outputting “enough” of the character a to satisfy the diagonal problem. Note that two characters a and a′ may share the same branch. When a control state of the above form appears on a node of the run tree, the final component B makes explicit which characters the subtree rooted at that node is responsible for generating in large numbers. Thus, the initial control state will have B = {a_{1}, …, a_{α}} since all characters must be generated from this node. However, when the output tree branches – i.e. a node has more than one child – the contents of B will be partitioned amongst the children. That is, the responsibility of the parent to output enough of the characters in B is divided amongst its children.
The remaining components play the role of a test A_{p,p1,…,pm}^{O}. That is, the current node is simulating the control state p of P, and is required to produce m branches, where the stack is emptied on each leaf and the control states appearing on these leaves are p_{1}, …, p_{m}. Moreover, the tree should output at least one of each character in O.
Note, P_{−1} also has (external) tests of the form A_{p,p1,…,pm}^{O} that it can use to make decisions, just like in the single character case. However, it also performs tests “online” in its control states. This is necessary because the tests were used to check what could have happened on branches not followed by P_{−1}. In the single character case, there was only one branch, hence P_{−1} would uses tests to check all the branches not followed, and then continue down a single branch of the tree. In the multicharacter case the situation is different. Suppose a subtree rooted at a given node was responsible for outputting enough of both a_{1} and a_{2}. Amongst the possible children of this node we may select two children: one for outputting enough a_{1} characters, and one for outputting enough a_{2} characters. The alternatives not taken will be checked using tests as before. However, the child responsible for outputting a_{1} may have also wanted to run a test on the child responsible for outputting a_{2}. Thus, as well as having to output enough a_{2} characters, this latter child will also have to run the test required by the former. Thus, we have to build these tests into the control state. As a sanity condition we enforce O ∩ B = ∅ since a branch outputting a should never ask itself if it is able to produce at least one a.
We explain the rules of P_{−1} intuitively. It will be beneficial to refer to the formal definition (below) while reading the explanations. The case for R_{push} is illustrated in Figure 5 since it covers most of the situations appearing in the other rules as well.
Similarly, in the current subtree we are obliged to pop to leaf nodes containing the control states p_{1}, …, p_{m}. We split these obligations between the branches we are exploring and those we are handling using tests. We use another permutation check to ensure the obligations have been distributed properly.
Finally, we are required to output characters in O. We may also, in choosing a particular branch for a character a, need to output a to account for instances appearing on a missed branch. Hence we also output O′ to account for these. We distribute the obligations O and O′ amongst the different branches using X_{1}, …, X_{i} and Y_{1}, …, Y_{j}.
In these rules, after the push we’re in control state p′ and we guess that we will pop to control states p′_{1}, …, p′_{l}. Hence we have a branch or a test to ensure that this happens. The remaining branches and tests are for what happens after the pops. The start from the states p′_{1}, …, p′_{l} and must, in total, pop to the original pop obligation p_{1}, …, p_{m}. Hence, we distribute these tasks in the same way as the R_{br}.
Before giving the formal definition, we summarise the discussion above by recalling the meaning of the various components. A control state (p, p_{1}, …, p_{m}, O, B) means we’re currently simulating a node at control state p that is required to produce m branches terminating in control states p_{1}, …, p_{m} respectively, that the produced tree should output at least one of each character in O and the entire subtree should output enough of each character in B to satisfy the diagonal problem. In the definition below, the set O′ is the set of new single character output obligations produced when the automaton decides which branches to follow faithfully and which to test (for the output of at least one of each character). The sets X_{1}, …, X_{i} and Y_{1}, …, Y_{j} represent the partitioning of the single character output obligations amongst the tests and new branches.
The correctness of the reduction is stated after the definition. A discussion of the proof appears in Section 7.
P_{−1} =  ⎛ ⎝  P_{−1}, Σ, Γ, R_{−1}, F_{−1}, p_{in}^{−1}, γ_{in}, θ_{−1}  ⎞ ⎠ 


⎛ ⎝  p_{in}^{−1}, γ_{in}  ⎞ ⎠  —^{ε}→  ⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠ 
⎛ ⎝ 
 ⎞ ⎠  —^{ε}→  ⎛ ⎝  f, rew_{γ}  ⎞ ⎠ 
⎛ ⎝ 
 ⎞ ⎠  — 
 →  ⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠ 
⎛ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎠ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p′_{1}, …, p′_{l}, rew_{γ}  ⎞ ⎠  ∈ R 
x_{1}, …, x_{i}, y_{1}, …, y_{j} 
x_{1}^{1}, …, x_{j1}^{1}, … x_{1}^{i}, …, x_{ji}^{i} y_{1}^{1}, …, y_{i1}^{1}, … y_{1}^{j}, …, y_{ij}^{j} 
O ⋃ O′ = X_{1} ⋃ ⋯ ⋃ X_{i}⋃ Y_{1} ⋃ ⋯ ⋃ Y_{j} 
⎛ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p′, push_{n}  ⎞ ⎠ 
x_{1}, …, x_{i}, y_{1}, …, y_{j} 
x_{1}^{1}, …, x_{j1}^{1}, … x_{1}^{i}, …, x_{ji}^{i} y_{1}^{1}, …, y_{i1}^{1}, … y_{1}^{j}, …, y_{ij}^{j} 
O ⋃ O′ = X ⋃ X_{1} ⋃ ⋯ ⋃ X_{i}⋃ Y_{1} ⋃ ⋯ ⋃ Y_{j} 
⎛ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎠ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p′, push_{n}  ⎞ ⎠ 
x_{1}, …, x_{i}, y_{1}, …, y_{j} 
x_{1}^{1}, …, x_{j1}^{1}, … x_{1}^{i}, …, x_{ji}^{i} y_{1}^{1}, …, y_{i1}^{1}, … y_{1}^{j}, …, y_{ij}^{j} 
O ⋃ O′ = Y ⋃ X_{1} ⋃ ⋯ ⋃ X_{i}⋃ Y_{1} ⋃ ⋯ ⋃ Y_{j} 
In Section 7 we show that the reduction is correct.
To complete the reduction, we convert the (n, α)PDA with tests into a (n, α)PDA without tests.
Diagonal_{a1, …, aα}  ⎛ ⎝  P  ⎞ ⎠  ⇐⇒ Diagonal_{a1, …, aα}  ⎛ ⎝  P′  ⎞ ⎠  . 
Proof. From Definition 4 (P_{−1}) and Lemma 2 (Correctness of P_{−1}), we obtain from P an (n−1, α)PDA with tests P_{−1} satisfying the conditions of the lemma. To complete the proof, we invoke Theorem 1 (Removing Tests) to find P′ as required.
We show correctness of the reduction in Section 7. First we show that we have decidability once we have reduced to order0.
We show that the problem becomes decidable for a 0PDA P. This is essentially a finite state machine and we can linearise the trees generated by saving the list of states that have been branched to in the control state. After one branch has completed, we run the next in the list, until all branches have completed. Hence, a tree of P becomes a run of the linearised 0PDA, and viceversa. Since each output tree has a bounded number of branches, the list length is bounded. Thus, we convert P into a finite state word automaton, for which the diagonal problem is decidable. Note, this result can also be obtained from the decidability of the diagonal problem for pushdown automata.
 =  ⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠ 
P =  ⎧ ⎪ ⎨ ⎪ ⎩ 
 ⎪ ⎪ ⎪ ⎪ 
 ⎫ ⎪ ⎬ ⎪ ⎭  ⋃  ⎧ ⎨ ⎩  f  ⎫ ⎬ ⎭ 
⎛ ⎝ 
 ⎞ ⎠  —^{b}→  ⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{b}→  ⎛ ⎝  p′_{1}, …, p′_{l}, rew_{σ}  ⎞ ⎠  ∈ R 
⎛ ⎝ 
 ⎞ ⎠  —^{ε}→  ⎛ ⎝ 
 ⎞ ⎠ 
Diagonal_{a1, …, aα}  ⎛ ⎝  P  ⎞ ⎠  ⇐⇒ Diagonal_{a1, …, aα}  ⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠ 
Proof. Take an accepting run tree ρ of P. If this tree contains no branching, then it is straightforward to construct an accepting run of P. Hence, assume all trees with fewer than α branches have a corresponding run of P. At a subtree c[T_{1}, …, T_{m}] we take the run trees ρ_{1}, …, ρ_{m} corresponding to the subtrees. Let c = ⟨ p, γ ⟩ and c_{1} = ⟨ p_{1}, γ ⟩, …, c_{m}= ⟨ p_{m}, γ ⟩ be the configurations at the roots of the subtrees. We build a run beginning at c and transitioning to ⟨ (p_{1}, p_{2}, γ, …, p_{m}, γ), γ ⟩. The run then follows ρ_{1} with the extra information in its control state. After ρ_{1} accepts, we transition to ⟨ (p_{2}, p_{3}, γ, …, p_{m}, γ), γ ⟩ and then replay ρ_{2}. We repeat until all subtrees have been dispatched. This gives an accepting run of P outputting the same number of each a.
In the other direction, we replay the accepting run ρ of P until we reach a configuration ⟨ (p_{1}, p_{2}, γ, …, p_{m}, γ), γ ⟩ via a rule
⎛ ⎝  p, σ  ⎞ ⎠  —^{ε}→  ⎛ ⎝ 
 ⎞ ⎠ 
At this point we apply
⎛ ⎝  p, σ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p_{1}, …, p_{m}, rew_{γ}  ⎞ ⎠ 
of P. We obtain runs for each of the new children as follows. We split the remainder of the run ρ′ into m parts ρ′_{1}, …, ρ′_{m} where the break points correspond to each application of a rule of the second kind. For each i we replay the transitions of ρ′_{1} from ⟨ p_{i}, γ ⟩ to obtain a new run of P with fewer applications of the second rule. Inductively, we obtain an accepting run of P that we plug into the ith child. This gives us an accepting run of P outputting the same number of each a.
We thus have the following theorem.
Proof. We first interpret P as an (n, α)PDA and then construct via Lemma 3 (Reduction to Lower Orders) an (n−1, α)PDA P′ such that Diagonal_{a1, …, aα}(P) iff Diagonal_{a1, …, aα}(P′). We repeat this step until we have an (0, α)PDA. Then, from Lemma 4 (Decidability at Order0) we obtain decidability as required.
In this section we prove Lemma 2 (Correctness of P_{−1}). The proof follows the same outline as the single character case. To show there is a run with at least m of each character, we take via Lemma 1 (Section 7.2), m′ = (α+1)^{m}, and a run of P outputting at least this many of each character. Then from Lemma 2 (Section 7.3) a run of P_{−1} outputting at least m of each character as required. The other direction is shown in Lemma 3 (Section 7.4).
We first generalise our tree decomposition and notion of scores. We then show that every αbranch subtree of a tree decomposition generates a run tree of P_{−1} matching the scores of the tree. Finally we prove the opposite direction.
Given an output tree T of P where each push_{n} operation has a matching pop_{n} on all branches, we can construct a decomposed tree representation of the run inductively as follows. We define Tree(T[ε]) = T[ε] and, when
T = b  ⎡ ⎣  T_{1}, …, T_{m}  ⎤ ⎦ 
where the rule applied at the root does not contain a push_{n} operation, we have
Tree  ⎛ ⎝  T  ⎞ ⎠  = b  ⎡ ⎣ 
 ⎤ ⎦  . 
In the final case, let
T = ε  ⎡ ⎣  T′  ⎤ ⎦ 
where the rule applied at the root contains a push_{n} operation and the corresponding pop_{n} operations occur at nodes η_{1}, …, η_{m}.
Note, if the output trees had an arbitrary number of branches, m may be unbounded. In our case, m ≤ α, without which our reduction would fail: P_{−1} would be unable to accurately count the number of pop_{n} nodes. In fact, our trees would have unbounded out degree and Lemma 1 (Minimum Scores) would not generalise.
Let T_{1}, …, T_{m} be the output trees rooted at η_{1}, …, η_{m} respectively and let T′ be T with these subtrees removed. Observe all branches of T are cut by this operation since the push_{n} must be matched on all branches. We define
Tree  ⎛ ⎝  T  ⎞ ⎠  = ε  ⎡ ⎣ 
 ⎤ ⎦  . 
An accepting run of P has an extra pop_{n} operation at the end of each branch leading to the empty stack. Let T′ be the tree obtained by removing the final pop_{n}induced edge leading to the leaves of each branch. The tree decomposition of an accepting run is
Tree  ⎛ ⎝  T  ⎞ ⎠  = ε  ⎡ ⎣ 
 ⎤ ⎦ 
where there are as many T[ε] as there are leaves of T.
Notice that our trees have outdegree at most (α + 1).
We score branches in the same way as the single character case. We simply define Score_{a}(ρ) to be Score(ρ) when a is considered as the only output character (all others are replaced with ε).
We have to slightly modify our minimum score lemma to accommodate the increased outdegree of the nodes in the trees.
Score_{a}  ⎛ ⎝  T  ⎞ ⎠  ≥ log_{(α+1)}  ⎛ ⎝  m  ⎞ ⎠ 
Proof. This is a simple extension of the proof of Lemma 1 (Minimum Scores). We simply replace the twochild case with a tree with up to (α+1) children. In this case, we have to use log_{(α+1)} rather than log to maintain the lemma.
Proof. We will construct a tree ρ_{−1} in L(P_{−1}) top down. At each step we will maintain a “frontier” of ρ_{−1} and extend one leaf of this frontier until the whole tree is constructed. The frontier is of the form
⎛ ⎝  c_{1}, η_{1}, O_{1}, B_{1}, …, c_{l}, η_{l}, O_{l}B_{l}  ⎞ ⎠ 
which means that there are l nodes in the frontier. We have B_{1} ⊎ ⋯ ⊎ B_{l}= {a_{1}, …, a_{α}} and each B_{i} indicates that the ith branch, ending in configuration c_{i}, is responsible for outputting enough of each of the characters in B_{i}. Each η_{i} is the corresponding node in Tree(ρ) that is being tracked by the ith branch of the output of P_{−1}.
Let p_{f} be the final (accepting) control state of P and let T = Tree(ρ). We begin at the root node of T, which corresponds to the initial configuration of ρ. Let ⟨ p, [s]_{n} ⟩ be this initial configuration and let c = ⟨ (p, p_{f}, …, p_{f}, ∅, {a_{1}, …, a_{α}}), s ⟩ be the configuration of P_{−1} after an application of a rule from R_{init}. The initial frontier is (c, ε, {a_{1}, …, a_{α}}).
Thus, assume we have a frontier
⎛ ⎝  c_{1}, η_{1}, O_{1}, B_{1}, …, c_{h}, η_{h}, O_{h}, B_{h}  ⎞ ⎠ 
and for each of the sequences c_{−1}, η, O, B of the frontier we have
Pick such a sequence c_{−1}, η, O, B. We replace this sequence using a transition of P_{−1} in a way that produces a new frontier with the above properties and moves us a step closer to reaching leaves of T. There are three cases when we are dealing with internal nodes.
In this case there is a transition c —^{b}→ c′ via a rule (p, γ) —^{b}→ (p′, o) where o ∉ {push_{n}, pop_{n}}. Hence, we have
⎛ ⎝ 
 ⎞ ⎠  — 
 →  ⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠ 
in P_{−1} and thus we can extend ρ_{−1} with a transition c_{−1} —^{b}→ c′_{−1} via this rule. The new frontier is obtained by replacing c_{−1}, η, O, B with c′_{−1}, η′, O ∖ {b}, B where η′ is the child of η. The properties on the frontier are easily seen to be retained.
We separate B = B′_{1} ⊎ ⋯ ⊎ B′_{i} such that B′_{j} is the set of characters a that have their score derived from T_{j} (i.e. the subtree with the higher score for a characters). Let O′ be the set of all a who had a +1 in their score derived from another subtree. Let ⟨ x_{1}, s ⟩, … ⟨ x_{i}, s ⟩ be the configurations labelling the root nodes η_{0}, η_{1}, …, η_{i} of these subtrees. Let ⟨ y_{1}, s ⟩, …, ⟨ y_{j}, s ⟩ be the configurations labelling the root nodes of the remaining subtrees. Since T′ includes m leaves that are followed in ρ by pops to p_{1}, …, p_{m} we can distribute these control states amongst the branches, obtaining
x_{1}^{1}, …, x_{j1}^{1}, … x_{1}^{i}, …, x_{ji}^{i} y_{1}^{1}, …, y_{i1}^{1}, … y_{1}^{j}, …, y_{ij}^{j} . 
Finally, we can distribute
O ⋃ O′ = X_{1} ⋃ ⋯ ⋃ X_{i}⋃ Y_{1} ⋃ ⋯ ⋃ Y_{j} 
amongst the subtrees T_{1}, …, T_{l} since O can be distributed by assumption and we chose O′ such that this can be done.
From the runs corresponding to T_{1}, …, T_{l} and our choices above we know that the tests will pass. That is, c_{−1} ∈ L(A_{p′1,y11,…,yi11}^{Y1}), …, c_{−1} ∈ L(A_{p′j,y1j,…,yijj}^{Yj}).
Hence, we apply to c_{−1} the rule
⎛ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎠ 
and obtain configurations c_{−1}^{1}, …, c_{−1}^{i} and a new frontier satisfying the required properties by replacing c_{−1}, η, O, B with the sequence
c_{−1}^{1}, η_{1}, X_{1}, B′_{1}, … c_{−1}^{i}, η_{i}, X_{i}, B′_{i} . 
In this case we have that T′ (subtree of the decomposition T) corresponds to a run tree ρ_{T′} that can be decomposed into
There are two cases depending on whether we send the HOPDA down the branch corresponding to the push.
x_{1}^{1}, …, x_{j1}^{1}, … x_{1}^{i}, …, x_{ji}^{i} y_{1}^{1}, …, y_{i1}^{1}, … y_{1}^{j}, …, y_{ij}^{j} . 
O ⋃ O′ = X ⋃ X_{1} ⋃ ⋯ ⋃ X_{i}⋃ Y_{1} ⋃ ⋯ ⋃ Y_{j} 
From the existence of the runs ρ_{1}, …, ρ_{l} we know c_{−1} ∈ L(A_{p′1,y11,…,yi11}^{Y1}), …, c_{−1} ∈ L(A_{p′j,y1j,…,yijj}^{Yj}).
Hence, we apply to c_{−1} the rule
⎛ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ 
and obtain configurations c_{−1}^{0}, c_{−1}^{1}, …, c_{−1}^{i} and a new frontier satisfying the required properties by replacing c_{−1}, η, O, B with the sequence
c_{−1}^{0}, η_{0}, X, B′_{0}, c_{−1}^{1}, η_{1}, X_{1}, B′_{1}, … c_{−1}^{i}, η_{i}, X_{i}, B′_{i} . 
x_{1}^{1}, …, x_{j1}^{1}, … x_{1}^{i}, …, x_{ji}^{i} y_{1}^{1}, …, y_{i1}^{1}, … y_{1}^{j}, …, y_{ij}^{j} . 
O ⋃ O′ = X_{1} ⋃ ⋯ ⋃ X_{i}⋃ Y ⋃ Y_{1} ⋃ ⋯ ⋃ Y_{j} 
From the existence of ρ′ we know that c_{−1} ∈ L(A_{p′,p′1,…,p′l}^{Y}) and from the existence of ρ_{1}, …, ρ_{l} we also know c_{−1} ∈ L(A_{p′1,y11,…,yi11}^{Y1}), …, c_{−1} ∈ L(A_{p′j,y1j,…,yijj}^{Yj}).
Hence, we apply to c_{−1} the rule
⎛ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎠ 
and obtain configurations c_{−1}^{1}, …, c_{−1}^{i} and a new frontier satisfying the required properties by replacing c_{−1}, η, O, B with the sequence
c_{−1}^{1}, η_{1}, X_{1}, B′_{1}, … c_{−1}^{i}, η_{i}, X_{i}, B′_{i} . 
Finally, we reach a leaf node η with a run outputting the required number of as. We need to show that the run constructed is accepting. From the tree decomposition, we know that the corresponding node of ρ is immediately followed by a pop_{n}. Thus, from our conditions on the frontier, we must have m = 1 and O = ∅. We also have a rule (p, γ) —^{ε}→ (p_{1}, pop_{n}) and therefore ((p, p_{1}, ∅, B), γ, A_{tt}) —^{ε}→ (f, rew_{γ}) with which we can complete the run of P_{−1} as required.
Finally, we need to show that each accepting run tree of P_{−1} gives rise to an accepting run tree of P containing at least as many of each output character a.
Proof. Take an accepting run tree ρ_{−1} of P_{−1}. We show that there exists a corresponding run tree ρ of P outputting at least as many as.
We maintain a frontier
c_{1}, …, c_{h} 
of ρ_{−1} and a run ρ of P “with holes” such that
Initially after a rule from R_{init} we have the frontier c = ⟨ (p, p_{f}, …, p_{f}, ∅, {a_{1}, …, a_{α}}), s ⟩ with corresponding run ρ of P being
 ⎡ ⎣ 
 ⎤ ⎦  . 
Pick a configuration c_{−1} = ⟨ (p, p_{1}, …, p_{m}, O, B), top_{n}(s) ⟩ of the frontier that is not a leaf of ρ_{−1} and its corresponding node in ρ with parent labelled c = ⟨ p, s ⟩. Let ρ′_{−1} be the subtree of P_{−1} rooted at this configuration.
We show how to extend the frontier closer to the leaves of ρ_{−1}. There are several cases depending on the transition of P_{−1} used to exit our chosen node.
⎛ ⎝ 
 ⎞ ⎠  — 
 →  ⎛ ⎜ ⎝ 
 ⎞ ⎟ ⎠  . 
⎛ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎠ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p′_{1}, …, p′_{l}, rew_{γ}  ⎞ ⎠  ∈ R . 
The new frontier replaces c_{−1} with

which satisfies all properties as needed.
⎛ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p′, push_{n}  ⎞ ⎠ 
⟨ 
 , 
 ⟩ . 
These nodes have configurations ⟨ p′_{1}, s ⟩, …, ⟨ p′_{l}, s ⟩ (since s = pop_{n}(push_{n}(s))). These control states are distributed between x_{1}, …, x_{i} and y_{1}, …, y_{j}. Consider y_{1} (the other y_{2}, …, y_{j} are identical). We have from the passed test that ⟨ y_{1}, s ⟩ has a run where the first popping of the top_{n} stack leads to configurations ⟨ y_{1}^{1}, pop_{n}(s) ⟩, …, ⟨ y_{i1}^{1}, pop_{n}(s) ⟩. We append this run tree as a child of the node corresponding to y_{1}. Since y_{1}^{1}, …, y_{i1}^{1} appear amongst p_{1}, …, p_{m} we append the relevant subtrees we had already constructed for these nodes to complete these branches with the required properties.
Now consider x_{1} (the other cases are symmetric). In this case we append a node labelled ⟨ (x_{1}, x_{1}^{1}, …, x_{j1}^{1}, X_{1}, B_{1}), top_{n}(s) ⟩ as a child of the node corresponding to x_{1}. Since x_{1}^{1}, …, x_{j1}^{1} appear amongst p_{1}, …, p_{m} we append the relevant subtrees we had already constructed for these nodes to complete these branches with the required properties.
The new frontier replaces c_{−1} with
⟨ 
 , 
 ⟩ 
and

which satisfies all the required properties.
⎛ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎠  —^{O′ ⋂ B}→  ⎛ ⎜ ⎜ ⎜ ⎜ ⎝ 
 ⎞ ⎟ ⎟ ⎟ ⎟ ⎠ 
⎛ ⎝  p, γ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p′, push_{n}  ⎞ ⎠ 
These leaf nodes are completed using the same argument as the previous case. That is, they are labelled with configurations ⟨ p′_{1}, s ⟩, …, ⟨ p′_{l}, s ⟩. These control states are distributed between x_{1}, …, x_{i} and y_{1}, …, y_{j}. Consider y_{1} (the other y_{2}, …, y_{j} are identical). We have from the passed test that ⟨ y_{1}, s ⟩ has a run where the first popping of the top_{n} stack leads to configurations ⟨ y_{1}^{1}, pop_{n}(s) ⟩, …, ⟨ y_{i1}^{1}, pop_{n}(s) ⟩. We append this run tree as a child of the node corresponding to y_{1}. Since y_{1}^{1}, …, y_{i1}^{1} appear amongst p_{1}, …, p_{m} we append the relevant subtrees we had already constructed for these nodes to complete these branches with the required properties.
Now consider x_{1} (the other cases are symmetric). In this case we append a node labelled ⟨ (x_{1}, x_{1}^{1}, …, x_{j1}^{1}, X_{1}, B_{1}), top_{n}(s) ⟩ as a child of the node corresponding to x_{1}. Since x_{1}^{1}, …, x_{j1}^{1} appear amongst p_{1}, …, p_{m} we append the relevant subtrees we had already constructed for these nodes to complete these branches with the required properties.
The new frontier replaces c_{−1} with
⟨ 
 , 
 ⟩ 
and

which satisfies all the required properties.
In this case c has the form
⟨ 
 , 
 ⟩ 
and there is a rule
⎛ ⎝  p, γ  ⎞ ⎠  —^{ε}→  ⎛ ⎝  p′, pop_{n}  ⎞ ⎠  . 
We can remove the hole from ρ by applying this rule. That is, we remove the hole node, setting its parent to have its (only) child as its child. This is possible since by our conditions the child has the label ⟨ p′, pop_{n}(s) ⟩. We remove c_{−1} from the frontier.
Thus, the frontier moves towards the leaves of the tree and finally is empty. At this point we have an accepting run of P as required. To see that the run outputs enough of each character, one needs to observe that at each stage the tests and O component of the control state ensured at least one character output for each that appeared in some O′ labelling a transition. Then, for characters output along branches followed were reproduced faithfully.
We have shown, using a recent result by Zetzsche, that the downward closures of languages defined by HOPDA are computable. We believe this to be a useful foundational result upon which new analyses may be based. Our result already has several immediate consequences, including separation by piecewise testability and asynchronous parameterised systems.
Regarding the complexity of the approach. We are unaware of any complexity bounds implied by Zetzsche’s techniques. Due to the complexity of the reachability problem for HOPDA, the test automata may be a tower of exponentials of height n for HOPDA of order n. These test automata are built into the system before proceeding to reduce to order (n−1). Thus, we may reach a tower of exponentials of height O(n^{2}).
A natural next step is to consider collapsible pushdown systems, which are equivalent to recursion schemes (without the safety constraint). However, it is not currently clear how to generalise our techniques due to the nonlocal behaviour introduced by collapse. We may also try to adapt our techniques to a higherorder version of BSautomata [3], which may be used, e.g., to check boundedness of resource usage for higherorder programs.
We thank Georg Zetzsche for keeping us up to date with his work, Jason Crampton for knowing about logarithms when they were most required, and Chris Broadbent for discussions. This work was supported by the Engineering and Physical Sciences Research Council [EP/K009907/1 and EP/M023974/1].
This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.