Unboundedness and Downward Closures of Higher-Order Pushdown Automata

Abstract: We show the diagonal problem for higher-order 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 higher-order programs expressed as HOPDA or safe higher-order recursion schemes.

1  Introduction

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 higher-order features – which are increasingly important given the popularity of event-based programs and asynchronous programs based on a continuation or callback style of programming. Hence, the modelling of higher-order function calls is becoming key to analysing modern day programs.

A popular approach to verifying higher-order 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 order-2 model called 2-PDA with links [1] or, equivalently, panic automata [22]. When these recursion schemes satisfy a syntactical condition called safety, a restriction of CPDA called higher-order pushdown automata (HOPDA or n-PDA for order-n 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 order-2 CPDA that cannot be generated by a deterministic HOPDA of any order [31].

It is well known that concurrency and first-order 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 2-PDA, 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.

Proof. The only-if direction follows from Theorem 1 since given a language L ⊆ a₁^∗… 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 2-PDA to the general case of n-PDA. 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:

1. decidability of separability by piecewise testable languages, which follows from from Czerwiński and Martens [11],
2. decidability of reachability for parameterised concurrent systems of HOPDA communicating asynchronously via a shared global register, from La Torre et al. [36],
3. decidability of finiteness of a language defined by a HOPDA, and
4. computability of the downward closure of the Parikh image of a HOPDA.

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 n-PDA are created and destroyed using push_n and pop_n operations. These push_n and pop_n operations along a run of an n-PDA are “well-bracketed” (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 well-bracketed 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 n-PDA could. Hence, by repeating this reduction, we obtain a 1-PDA, 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₁, …, 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).

2  Preliminaries

2.1  Downward Closures

Given two words w = γ₁ … γ_m∈ Σ^∗ and w′ = σ₁ … σ_l∈ Σ^∗ for some alphabet Σ, we write w ≤ w′ iff there exist i₁ < … < 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}.

2.2  Trees

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 prefix-closed, 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

to denote the tree whose root node is labelled a and has children T₁, …, T_m. That is, we define a[T₁, …, 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, η₁ ⋯ η_n, such that η₁ = є, η_n = δ₁   δ₂ ⋯ δ_n−1 is maximal in D, and η_j+1 = η_j   δ_j for each 1 ≤ j ≤ n−1.

2.3  HOPDA

HOPDA are a generalisation of pushdown systems to a stack-of-stacks structure. An order-n stack is a stack of order-(n−1) stacks. An order-n 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

to be the set of order-n stack operations.

For example

We write (p, γ) —^a→ (p′, o) for a rule (p, γ, a, o, p′) ∈ R.

A configuration of an n-PDA is a tuple ⟨ p, s ⟩ where p ∈ P and s is an order-n stack over Γ. We have a transition ⟨ p, s ⟩ —^a→ ⟨ p′, s′ ⟩ whenever we have (p, γ) —^a→ (p′, o), top₁(s) = γ, and s′ = o(s).

A run over a word w ∈ Σ^∗ is a sequence of configurations c₀ —^a₁→ ⋯ —^a_m→ c_m such that the word a₁…a_m is w. It is an accepting run if c₀ = ⟨ p_in, [[ γ_in ]] ⟩ — where we write [[ γ ]] for [⋯[γ]₁⋯]_n — and where c_m= ⟨ p, s ⟩ with p ∈ F. Furthermore, for a set of configurations C, we define

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₁; …; 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₁ character of the stack is γ. All of these extensions can be encoded by introducing intermediate control states.

2.3.1  Regular Sets of Stacks

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 bottom-up 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,…,[₁, ]₁,…,]_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 order-k stack is an edge labelled [_k and the end of an order-k stack is an edge labelled ]_k, a run of a bottom-up stack automaton is a labelling of the nodes of the graph with states in Q such that

1. the rightmost (final) node is labelled by q_in, and
2. whenever we have for any γ ∈ Γ_[], and pair of labelled nodes with an edge q —^γ→ q′ then q = Δ(q′, γ).

The run is accepting if the leftmost (initial) node is labelled by q ∈ Q_F. An example run over the word graph representation of [ [ [γ   σ]₁[σ]₁ ]₂ [ [σ]₁ ]₂ ]₃ 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).

---

Figure 1: A run over [ [ [γ   σ]1[σ]1 ]2 [ [σ]1 ]2 ]3

---

3  The Single Character Case

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.

3.1  Outline of Proof

The approach is to take an n-PDA P and produce an (n−1)-PDA P₋₁ 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 out-degree 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 n-PDA. 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.

---

Figure 2: Tree decompositions of runs.

---

In more detail, we perform the following steps.

1. Instrument P to record whether an a character has been output. Then, using known reachability results, obtain regular sets of configurations from which the current top_n stack can be popped, and moreover, we can know whether an a is output on the way. These tests can be seen as a generalisation of pushdown systems with regular tests introduced by Esparza et al. [12].
2. From an n-PDA P, we define an (n−1)-PDA with tests P₋₁ and then an (n−1)-PDA P′ such that

   Diagonala

   ⎛ ⎝

   P

   ⎞ ⎠

   ⇐⇒ Diagonala

   ⎛ ⎝

   P′

   ⎞ ⎠

   .

   The tests will be used to check the branches of the tree decomposition not explored by P₋₁.
3. By repeated applications of the above reduction, we obtain an 1-PDA P for which Diagonal_a(P) is decidable since the downward closure of a context-free grammar (equivalent to 1-PDA) is computable [39, 9] and this is equivalent to the diagonal problem.

The (n−1)-PDA with tests P₋₁ will simulate the n-PDA P in the following way.

• All operations except for push_n and pop_n will be simulated directly.
• In lieu of performing a push_n, P₋₁ will choose to simulate the run of P between the push and its corresponding pop_n, or the run of P after the corresponding pop_n has taken place.
  • Tests will be used to determine which control state could appear after the corresponding pop_n.
  • If the part of the run not being simulated output some as, then P will output a single a in place of the omitted as.

Although P₋₁ 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 1-PDA. It is known that Diagonal_a(P) for an 1-PDA is decidable since it is possible to compute the downward closure [39, 9].

3.2  HOPDA with Tests

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].

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₁(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.

3.2.1  Marking Outputs

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,

• for a given p₁ and p₂, there is a run from ⟨ p₁, [s]_n ⟩ to ⟨ p₂, []_n ⟩ (that is, the HOPDA empties the stack), and
• whether, during the run, an a is output.

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.

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.

3.2.2  Building the Automata

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₁, p₂ ∈ 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.

1. A_{p1, p2} accepting all stacks s such that there is a run of P from ⟨ p₁, [s]_n ⟩ to ⟨ p₂, []_n ⟩,
2. A_{p1, p2}^a accepting all stacks s such that there is a run of P from ⟨ p₁, [s]_n ⟩ to ⟨ p₂, []_n ⟩ that outputs at least one a.

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 top-down automaton A and a control state p we can build a bottom-up 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 top-down automaton accepting configurations of the form ⟨ p, [s]_n ⟩ where top₁(s) = γ. Next, let

and

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 bottom-up automata since both

are regular from Theorem 3, and bottom-up and top-down automata are effectively equivalent. To enforce only stacks of the form [s]_n we intersect with an automaton A₁ accepting all stacks containing a single order-(n−1) stack (this is clearly regular).

3.3  Reduction to Lower Orders

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₁, p₂) means that we are currently in control state p₁ and are aiming to empty the stack on reaching p₂, 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.

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.

Proof. From Definition 4 (P₋₁) and Lemma 1 (Correctness of P₋₁), we obtain from P an (n−1)-PDA with tests P₋₁ satisfying the conditions of the lemma. To complete the proof, we invoke Theorem 2 (Removing Tests) to find P′ as required.

4  Correctness of Reduction

This section is dedicated to the proof of Lemma 1 (Correctness of P₋₁).

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₋₁. To prove that P₋₁ can output an unbounded number of as we prove that any tree containing m edges outputting a must have a branch along which P₋₁ would output log(m) a characters. Thus, if P can output an unbounded number of a characters, so can P₋₁.

4.1  Tree Decomposition of Runs

Given a run

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 single-configuration run c, and, when

where the first rule applied does not contain a push_n operation, we have

and, when

with c₁ being the first configuration of ρ₂ and where the first rule applied in ρ contains a push_n operation, c₀ = ⟨ p, s ⟩ and c₁ = ⟨ p′, s ⟩ for some p, p′, s and there is no configuration in ρ₁ of the form ⟨ p″, s ⟩, then

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

4.2  Scoring Trees

In the above tree decomposition of runs, the tree branches at each instance of a push_n operation. This mimics the behaviour of P₋₁, which performs such branching non-deterministically. Hence, given a run ρ of P, each branch of Tree(ρ) corresponds to a run of P₋₁.

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₋₁ 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 out-degree larger than 2. This is needed in the simultaneous unboundedness section. For the moment, we only have trees with out-degree at most 2.

Let

Then,

We then have the following lemma for trees with out-degree 2.

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

1. T′ = a[T₁], or
2. T′ = ε[T₁, T₂] where T₁ and T₂ each have at least one node each labelled a.

In case (1) we have by induction

In case (2) we have

We pick whichever of T₁ and T₂ 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 right-hand side of the addition is always 1. Hence, we need to show

which follows from

By our choice of T′ we thus have Score(T) = Score(T′) ≥ log(m) as required.

4.3  From Branches to Runs

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₋₁.

Thus, assume we have a node η of T, with a corresponding configuration c = ⟨ p, s ⟩ of P and configuration c₋₁ = ⟨ (p, p_pop), top_n(s) ⟩ of P₋₁ and a run ρ₋₁ of P₋₁ ending in c₋₁ and outputting (m − Score(T′)) a characters where T′ is the subtree of T rooted at η. The subtree T′ corresponds to a sub-run ρ′ 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.

• T′ = b[T₁].

  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₋₁ and thus we can extend ρ₋₁ with a transition c₋₁ —^b→ c′₋₁ via this rule where ρ₋₁, c′ and c′₋₁ maintain the assumptions above.

• T′ = ε[T₁, T₂].

  In this case we have that T′ corresponds to a sub-run

  c —ε→ ρ1 —ε→ ρ2

  of ρ. The transition from c to the beginning of ρ₁ is via a rule r₁ = (p, γ) —^ε→ (p₁, push_n) and the transition from the end of ρ₁ to the start of ρ₂ is via a rule r₂ = (p₂, γ₁) —^ε→ (p₃, pop_n). Moreover, from the definition of the decomposition, the final configuration in ρ₂ is followed in ρ by a pop rule r₃ = (p₄, γ₂) —^ε→ (p_pop, pop_n).

  There are two further cases depending on whether the score of T′ is derived from the score of T₁ or T₂.

  • In the case of T₁, then, first observe that ρ₂ followed by an application of r₃ is a run from ⟨ p₃, s ⟩ to ⟨ p_pop, pop_n(s) ⟩ where the stack pop_n(s) does not appear in ρ₂. Thus, there is a run of P from ⟨ p₃, [top_n(s)]_n ⟩ to ⟨ p_pop, []_n ⟩ and moreover, this run outputs an a whenever the original run does. Hence, there is also a corresponding run of P from which outputs an a whenever the original run does.

    If an a is output, we have c₋₁ ∈ L(A_{p3, ppop}^a) and Score(T′) − Score(T₁) = 1. We can extend ρ via an application of the rule ((p, p_pop), γ, A_{p3, ppop}^a) —^a→ ((p₁, p₃), rew_γ) that exists in P₋₁ since c₋₁ ∈ L(A_{p3, ppop}^a). This transition maintains the property on the stacks since the push_n copies the topmost stack, hence P₋₁ 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₂. Finally, the condition on control states is satisfied since the second component is set to p₂.

    If an a is not output, then the case is similar to the above, except T₂ does not contribute to the score, we have c₋₁ ∈ L(A_{p3, ppop}), and the transition of P₋₁ is labelled ε instead of a.

  • The case of T₂ is almost symmetric to T₁. Observe that ρ₁ followed by an application of r₂ is a run from ⟨ p₁, push_n(s) ⟩ to ⟨ p₃, s ⟩ where the stack s does not appear in ρ₁. Thus, there is a run of P from ⟨ p₁, [top_n(s)]_n ⟩ to ⟨ p₃, []_n ⟩ and moreover, this run outputs an a whenever the original run does. Hence, there is also a corresponding run of P from which outputs an a whenever the original run does.

    If an a is output, we have c₋₁ ∈ L(A_{p1, p3}^a) and Score(T′) − Score(T₂) = 1. We can extend ρ via an application of the rule ((p, p_pop), γ, A_{p1, p3}^a) —^a→ ((p₃, p_pop), rew_γ) that exists in P₋₁ since c₋₁ ∈ 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₋₁ 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₁. 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₁ does not contribute to the score, we have c₋₁ ∈ L(A_{p1, p3}) and the transition of P₋₁ 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 sub-run ρ′ 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₋₁ as required.

4.4  The Other Direction

Finally, we need to show that each accepting run of P₋₁ 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 ρ₋₁ of P₋₁. We show that there exists a corresponding run ρ of P outputting at least as many as.

Let

for some s be the accepting run of P₋₁. We define inductively for each 0 ≤ i ≤ m a pair of runs ρ₁ⁱ, ρ₂ⁱ of P such that

1. ρ₂ⁱ ends in a configuration ⟨ p_f, []_n ⟩ (i.e. is accepting), and
2. if c_i= ⟨ (p, p_pop), s ⟩ then
   1. the final configuration of ρ₁ⁱ is ⟨ p, [s s₁ … s_l]_n ⟩, for some s₁, …, s_l, and
   2. the first configuration of ρ₂ⁱ is ⟨ p_pop, [s₁ … s_l]_n ⟩, and
3. the sum of the number of a characters output by ρ₁ⁱ and ρ₂ⁱ is at least the number of a characters output by c₀ —^b₁→ ⋯ —^b_i→ c_i.

Initially we have c₀ = ⟨ (p_in, p_f), s ⟩ and s = [[ γ_in ]]. We define ρ₁⁰ = ⟨ p_in, [s]_n ⟩ and ρ₂⁰ = ⟨ p_f, []_n ⟩ which immediately satisfy the required conditions.

Assume we have ρ₁ⁱ and ρ₂ⁱ as required. We show how to obtain ρ₁ⁱ⁺¹ and ρ₂ⁱ⁺¹. There are several cases depending on the rule used on the transition c_i—^b_i+1→ c_i+1. Let c_i= ⟨ (p, p_pop), s ⟩, the final configuration of ρ₁ⁱ be ⟨ p, [s s₁ … s_l]_n ⟩ and the first configuration of ρ₂ⁱ be ⟨ p_pop, [s₁ … s_l]_n ⟩.

• If the rule was ((p, p_pop), γ, A_tt) —^b→ ((p′, p_pop), o) with o ∉push_n, pop_n then we have (p, γ) —^b→ (p′, o) ∈ R and we define ρ₁ⁱ⁺¹ to be ρ₁ⁱ extended by an application of this rule. We also define ρ₂ⁱ⁺¹ = ρ₂ⁱ.

  The required conditions are inherited from ρ₁ⁱ and ρ₂ⁱ since o only changes the top_n stack, the final configuration of ρ₂ⁱ⁺¹ is the same as ρ₂ⁱ, p_pop is not changed, and the rule of P outputs an a iff the rule of P₋₁ does.

• If the rule was ((p, p_pop), γ, A_{p′pop, ppop}) —^ε→ ((p′, p′_pop), rew_γ) then we have a rule r = (p, γ) —^ε→ (p′, push_n) ∈ R. Moreover, from the test A_{p′pop, ppop} we know there is a run of P from ⟨ p′_pop, [s]_n ⟩ to ⟨ p_pop, []_n ⟩ and hence there is also a run ρ from ⟨ p′_pop, [s s₁ … s_l]_n ⟩ to ⟨ p_pop, [s₁ … s_l]_n ⟩. We set ρ₂ⁱ⁺¹ = ρ ρ₂ⁱ and ρ₁ⁱ⁺¹ to be ρ₁ⁱ extended by an application of r.

  Since the final configuration of ρ₁ⁱ⁺¹ is ⟨ p′, [s s s₁ … s_l]_n ⟩ it is easy to check the required correspondence with the first configuration ⟨ p′_pop, [s s₁ … s_l]_n ⟩ of ρ₂ⁱ⁺¹.

  The remaining conditions are immediate since no a is output and the final configuration of ρ₂ⁱ⁺¹ is the same as ρ₂ⁱ.

• The case of ((p, p_pop), γ, A_{p′pop, ppop}^a) —^a→ ((p′, p′_pop), rew_γ) is almost identical to the previous case. To adapt the proof, one needs only observe that since c_i∈ L(A_{p′pop, ppop}^a) the run ρ used to extend ρ₂ⁱ also outputs at least one a character.
• If the rule was ((p, p_pop), γ, A_{p1, p2}) —^ε→ ((p₂, p_pop), rew_γ) then there is also a rule r = (p, γ) —^ε→ (p₁, push_n) ∈ R and from the test A_{p1, p2} we know there is a run of P from ⟨ p₁, [s]_n ⟩ to ⟨ p₂, []_n ⟩ and therefore there is also a run ρ that goes from ⟨ p₁, [s s s₁ … s_l]_n ⟩ to ⟨ p₂, [s s₁ … s_l]_n ⟩. We set ρ₁ⁱ⁺¹ to be ρ₁ⁱ extended with an application of r and then the run ρ. We also set ρ₂ⁱ⁺¹ = ρ₂ⁱ.

  To verify that the properties hold, we observe that c_i+1 = ⟨ (p₂, p_pop), s ⟩, and ρ₁ⁱ⁺¹ ends with ⟨ p₂, [s s₁ … s_l]_n ⟩ and ρ₂ⁱ⁺¹ still begins with ⟨ p_pop, [s₁ … s_l]_n ⟩ and has the required final configuration. The property on the number of as holds since the rule of P₋₁ did not output an a.

• The case of ((p, p_pop), γ, A_{p1, p2}^a) —^a→ ((p₂, p_pop), rew_γ) is almost identical to the previous case. To adapt the proof, one needs only observe that since c_i∈ L(A_{p1, p2}^a) the run ρ used to extend ρ₁ⁱ also outputs at least one a character.

Finally, when we reach i = m we have from the final transition of the run of P₋₁ that there is a rule (p, γ) —^ε→ (p_pop, pop_n). We combine ρ₁^m and ρ₂^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₋₁.

5  Multiple Characters

We generalise the previous result to the full diagonal problem. Naïvely, the previous approach cannot work. Consider the HOPDA executing

where the first sequence of pop₁ operations output a₁ and the second sequence output a₂.

The corresponding run trees are of the form given in Figure 3. In particular, P₋₁ can only choose one branch, hence all runs of P₋₁ produce a bounded number of a₁s or a bounded number of a₂s. They cannot be simultaneously unbounded.

---

Figure 3: An example showing that following a single branch does not work for simultaneous unboundedness.

---

For P₋₁ to be able to output both an unbounded number of a₁ and a₂ 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 n-PDA to (n−1)-PDA can be generalised to α-branch HOPDA.

5.1  Branching HOPDA

We define n-PDA outputting trees with at most α branches, denoted (n, α)-PDA. Note, an n-PDA 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₁, …, p_m, o) to denote a rule (p, γ, b, o, p₁, …, 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₀ = ⟨ p_in, [[ γ_in ]] ⟩ a run of an (n, α)-PDA is a tree T = (D, λ) whose nodes are labelled with n-PDA configurations, and generates an output tree T′ = (D, λ′) whose nodes are labelled with symbols from the output alphabet. Precisely

• λ(ε) = c₀, and
• for a node η with children η₁, …, η_m and λ(η) = ⟨ p, s ⟩ there is a rule (p, γ) —^b→ (p₁, …, p_m, o) such that for all 1 ≤ i ≤ m we have λ(η_i) = ⟨ p_i, s′ ⟩ where top₁(s) = γ, s′ = o(s). Moreover we have λ′(η) = b.
• For all leaf nodes η we have λ′(η) = ε.

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

6  Reduction For Simultaneous Unboundedness

Given an (n, α)-PDA P we construct an (n−1, α)-PDA P₋₁ such that

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₁, …, 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₁, …, 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.

6.1  Some Intuition

We briefly sketch the intuition behind the algorithm. We illustrate the reduction from (n, α)-PDA to (n−1, α)-PDA in Figure 4.

• We begin with an n-PDA which we first interpret as an (n, α)-PDA. This is possible because an (n, α)-PDA can produce at most α branches. Thus, an n-PDA — which produces a single branch — is also a (n, α)-PDA. We work with HOPDA producing α branches because, after each reduction step, we will need to output one branch for each character in a₁, …, a_α.
• We have an (n, α)-PDA P that outputs a tree with at most α branches. In Figure 4 we show part of a run tree with 2 branches. The push_n and pop_n operations are shown on the edges of the tree. Nodes are numbered to help identify them during the different transformations.
• We “decompose” this tree into another tree where the branches appearing after the pop_n operations are hung from the same parent as their matching push_n. This is shown in the middle of Figure 4. Notice that this tree has an unbounded number of branches (it branches at each push_n). However, we know that the maximum out-degree of any of its nodes is (α + 1) since the source of a push_n-labelled edge has one child, and we add at most α extra children corresponding to the pop_n on each of its at most α branches.
• We prove a generalisation of Lemma 1 (Minimum Scores) that shows a run tree with at least m instances of a character a has a branch with a score of at least log_(α+1)(m). Thus, we need to select one branch for each a we wish to output.
• We build an (n−1, α)-PDA P₋₁ that non-deterministically picks out the highest scoring branches for each a. This is shown on the right of Figure 4.

---

Figure 4: Illustrating the reduction steps.

---

6.2  Branching HOPDA with Regular Tests

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₁, …, p_m, o) to denote a rule (p, γ, A, b, o, p₁, …, p_m) ∈ R.

From the initial configuration c₀ = ⟨ p_in, [[ γ_in ]] ⟩ a run of an (n, α)-PDA with tests is a tree T = (D, λ) and generates an output tree ρ = (D, λ′) where

• λ(ε) = c₀, and
• for a node η with children η₁, …, η_m and λ(η) = ⟨ p, s ⟩ there is a rule (p, γ, A) —^b→ (p₁, …, p_m, o) such that s ∈ L(A) and for all 1 ≤ i ≤ m we have λ(η_i) = ⟨ p_i, s′ ⟩ where top₁(s) = γ, and s′ = o(s). Moreover we have λ′(η) = b.
• For all leaf nodes η we have λ′(η) = ε.

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₁, …, 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

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₁(s) from initial state q as

and then we can consult Δ to complete the run by adding the effect of reading top₁(s).

Thus, let A_i= (Q_i, Γ_[], q_inⁱ, Δ_i, Q_Fⁱ). We define

where

and R^T is the smallest set of rules of the form

where γ^T = (γ, τ₁, …, τ_m) and (p, γ, A_i) —^b→ (p₁, …, p_l, o) ∈ R and Accepts(γ, τ_i, Δ_i, q_inⁱ, Q_Fⁱ) and we define

where Δ(q, [_n ⋯ [₁ γ) is shorthand for the repeated application of Δ on γ then [₁, back to [_n, and we define Update(o, γ^T) = o^T following the cases below. Let γ^T = (γ, τ₁, …, τ_m).

• When o = rew_σ then o^T = (σ, τ₁, …, τ_m).
• When o = push_k then o^T = push_o; rew_{(γ, τ1′, …, τm′)} where for all i we have

  τ

  i =

  ⎛ ⎝

  τ1, …, τk−1, τk′, τk+1, … τn

  ⎞ ⎠

  and

  τk′

  ⎛ ⎝

  q

  ⎞ ⎠

  = τk

  ⎛ ⎝

  Δi ⎛ ⎝ τ1 ⎛ ⎝ ⋯ τk ⎛ ⎝ q ⎞ ⎠ ⎞ ⎠ , ]k−1 [k−1 ⋯ [1 γ ⎞ ⎠

  ⎞ ⎠

  .

  I.e., we apply the functions to read the whole stack once, and then the correct part of the copy created by the push_k.
• When o = pop_k then

  oT = popo;

  ⎛ ⎜ ⎝ σ,  τ 1′, …,  τ m′ ⎞ ⎟ ⎠

  ?; rew

  ⎛ ⎜ ⎝ σ,  τ 1″, …,  τ m″ ⎞ ⎟ ⎠

  where for all i we have τ_i = (τ₁, …, τ_n) and τ_i′ = (τ₁′, …, τ_n′) and

  τ

  i″ =

  ⎛ ⎝

  τ1′, …, τk−1′, τk, … τn

  ⎞ ⎠

  .

  We can see that this is correct since we do not update the functions that read parts of the stack unchanged (i.e., stacks outside of those changed by the pop_k), and we take the functions that are correct for the newly exposed top parts of the stack for the remaining functions.

Finally, we set γ_in^T = (γ_in, τ₁, …, τ_m) where for each i we have τ_i = (τ₁, …, τ_n) such that for each k we have τ_k(q) = Δ(q, ]_k ⋯ ]_n).

6.3  Building The Automata

Previously we built automata A_{p1, p2} to indicate that from p₁, the current top stack could be removed, arriving at p₂. 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₁, …, 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

where θ(p) ≥ θ(p₁) + ⋯ + θ(p_m) and O ⊆ {a₁, …, 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₁, []_n ⟩, …, ⟨ p_m, []_n ⟩ respectively. Moreover, we have a ∈ O iff the corresponding output tree T′ has |T′|_a > 0.

6.3.1  Alternating HOPDA

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 higher-order 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.

We write (p, γ) → (p, o) to denote (p, γ, o, p) ∈ R and (p, γ) → p₁, …, p_m to denote (p, γ, {p₁, …, 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

6.3.2  Constructing the Tests

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¹ (p, γ) → p₁, …, 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.

In the above definition, the permutation condition ensures that the target control states are properly distributed amongst the newly created branches.

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₁, …, c_l and building a tree witnessing that ⟨ (p, O, p₁, …, p_m), [s]_n ⟩ ∈ Pre_P⋄^∗(A). Initially we have the frontier ⟨ p, [s]_n ⟩ and the initial configuration ⟨ (p, O, p₁, …, p_m), [s]_n ⟩.

Hence, take a configuration c = ⟨ p′, s′ ⟩ from the frontier and corresponding configuration c′ = ⟨ (p′, O′, p′₁, …, 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″₁, …, p″_j, rew_γ) then we apply the rule

where p′₁, …, p′_i is a permutation of p₁¹, …, p_i1¹, … p₁^j, …, p_ij^m and O = O₁ ∪ ⋯ ∪ 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₁, …, 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 top-down automaton representation of Pre_P⋄^∗(A) since we can effectively translate from top-down to bottom-up stack automata.

6.4  Reduction to Lower Orders

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₋₁ such that P satisfies the diagonal problem iff P₋₁ also satisfies the diagonal problem. The main control states of P₋₁ take the form

where p, p₁, …, 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₋₁ to generate up to m branches of the tree decomposition of a run of P. In particular, for each of the characters a ∈ {a₁, …, a_α} there will be a branch of the run of P₋₁ 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₁, …, 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₁, …, p_m. Moreover, the tree should output at least one of each character in O.

Note, P₋₁ 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₋₁. In the single character case, there was only one branch, hence P₋₁ would uses tests to check all the branches not followed, and then continue down a single branch of the tree. In the multi-character case the situation is different. Suppose a subtree rooted at a given node was responsible for outputting enough of both a₁ and a₂. Amongst the possible children of this node we may select two children: one for outputting enough a₁ characters, and one for outputting enough a₂ characters. The alternatives not taken will be checked using tests as before. However, the child responsible for outputting a₁ may have also wanted to run a test on the child responsible for outputting a₂. Thus, as well as having to output enough a₂ 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₋₁ 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.

• The rules in R_init guess how many branches will be needed to output enough of each a. (This might be less than α since one branch might account for several characters.)
• The rules in R_fin check whether the run can be finished (always via a pop_n since we are aiming for the empty stack). This is true if we only have one branch to complete (just reach p′) and we have no more characters that we’re obliged to output.
• The rules in R_sim simulate a non-branching operation. They do this faithfully, simply passing along all information (updating O if a character is output by the simulated transition).
• The rules in R_br are the first of the complicated rules. This is mainly a matter of notation. The reasoning behind the rules is that we’re at a point where the tree splits into l different branches. These have control states p′₁, …, p′_l respectively. We non-deterministically guess which of these branches should output which of the characters in B. Thus, we split B into B₁, …, B_i. This means we are exploring i branches. Let x₁, …, x_i be the control states on these branches. The remaining branches we handle using tests on the stack. Let y₁, …, y_j be the control states appearing on these branches. We require that all of p′₁, …, p′_l are accounted for, so we assert that p′₁, …, p′_l is a permutation of x₁, …, x_i, y₁, …, y_j.

  Similarly, in the current subtree we are obliged to pop to leaf nodes containing the control states p₁, …, 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₁, …, X_i and Y₁, …, Y_j.

• The rules in R_push and R_pop follow the same intuition as in the single character case, except we have the branching to deal with. In particular, at a push we have one branch corresponding to exploring what happens between the push and the corresponding pops, and a branch for each of the corresponding pops. We choose a selection of these branches to track with the HOPDA and a selection to handle using tests. The difference between R_push and R_pop is that the former explores the branch of the push using the HOPDA and the latter uses a test.

  In these rules, after the push we’re in control state p′ and we guess that we will pop to control states p′₁, …, 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′₁, …, p′_l and must, in total, pop to the original pop obligation p₁, …, p_m. Hence, we distribute these tasks in the same way as the R_br.

---

Figure 5: Illustrating the rules in Rpush.

---

Before giving the formal definition, we summarise the discussion above by recalling the meaning of the various components. A control state (p, p₁, …, 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₁, …, 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₁, …, X_i and Y₁, …, 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.