16311 \lmcsheadingLABEL:LastPageApr. 18, 2014Aug. 20, 2020
On the Expressive Power of
Higher-Order Pushdown Systems
Abstract.
We show that deterministic collapsible pushdown automata of second order can recognize a language that is not recognizable by any deterministic higher-order pushdown automaton (without collapse) of any order. This implies that there exists a tree generated by a second order collapsible pushdown system (equivalently, by a recursion scheme of second order) that is not generated by any deterministic higher-order pushdown system (without collapse) of any order (equivalently, by any safe recursion scheme of any order). As a side effect, we present a pumping lemma for deterministic higher-order pushdown automata, which potentially can be useful for other applications.
Key words and phrases:
Higher-order pushdown systems, collapse, higher-order recursion schemes1991 Mathematics Subject Classification:
F.1.1. Models of computation—Relations between modelsThis is a full version of our conference paper [ho-new]
1. Introduction
Already in the 70’s, Maslov [Mas74, Mas76] generalized the concept of pushdown automata to higher-order pushdown automata (-PDA) by allowing the stack to contain other stacks rather than just atomic elements. In the last decade, renewed interest in these automata has arisen. They are now studied not only as acceptors of string languages, but also as generators of graphs and trees. It was an interesting problem whether the class of trees generated by -PDA coincides with the class of trees generated by order- recursion schemes. Knapik, Niwiński, and Urzyczyn [easy-trees] showed something similar but different: that this class coincides with the class of trees generated by safe order- recursion schemes (safety is a syntactic restriction on the recursion scheme), and Caucal [Caucal02] gave another characterization: trees of order are obtained from trees of order by an MSO-interpretation of a graph, followed by application of unfolding.
Driven by the question whether safety implies a semantical restriction to recursion schemes Hague, Murawski, Ong, and Serre [collapsible] extended the model of -PDA to order- collapsible pushdown automata (-CPDA) by introducing a new stack operation called collapse, and proved that the class of trees generated by -CPDA coincides with the class of trees generated by order- recursion schemes (earlier, Knapik, Niwiński, Urzyczyn, and Walukiewicz [panic] introduced panic automata, a model equivalent to -CPDA). Let us mention that these trees have decidable MSO theory [ong-lics], and that higher-order recursion schemes have close connections with verification of some real life higher-order programs [Kobayashi09].
Nevertheless, it was still an open question whether these two hierarchies of trees are possibly the same hierarchy? This problem was stated in Knapik et al. [easy-trees] and repeated in other papers concerning higher-order pushdown automata [panic, AehligMO05, ong-lics, collapsible]. A partial answer to this question was given in our previous paper [parys-panic]: there is a tree generated by a -CPDA that is not generated by any -PDA. We prove the following stronger property.
Theorem 1.
There is a tree generated by a -CPDA (equivalently, by a recursion scheme of order ) that is not generated by any -PDA, for any (equivalently, by any safe recursion scheme of any order).
This confirms that the correspondence between higher-order recursion schemes and higher-order pushdown automata is not perfect. The tree used in Theorem 1 (after some adaptations) comes from Knapik et al. [easy-trees] and from that time was conjectured to be a good example.
In this paper we work with PDA that recognize words instead of generating trees. While in general PDA used to recognize word languages can be nondeterministic, trees generated by PDA closely correspond to word languages recognized by deterministic PDA. Technically, we prove the following theorem, from which Theorem 1 follows (it is shown in Section 3 how these theorems are related).
Theorem 2.
There is a language recognized by a deterministic -CPDA that is not recognized by any deterministic -PDA, for any .
As a side effect, in Section LABEL:sec:pumping we present a pumping lemma for higher-order pushdown automata. Although its formulation is not very natural, we believe it may be useful for some other applications. The lemma is similar to the pumping lemma from our another paper [parys-pumping]; see Section LABEL:sec:pumping for some comments. Earlier, several pumping lemmas related to the second order of the pushdown hierarchy were proposed [hayashi-pumping, gilman-pumping, kartzow-pumping].
This paper is an extended version of our conference paper [ho-new]. The proof of Theorem 1 goes along the same line, but with essential differences in details. The part about types (Section LABEL:sec:types) was simplified slightly, in the cost of complicating other parts (which was necessary since Theorem LABEL:thm:types is now proven in a weaker form than in the conference paper).
1.1. Related Work
One may ask a similar question for word languages instead of trees: is there a language recognized by a CPDA that is not recognized by any (nondeterministic) PDA? This is an independent problem. The answer is known only for order and is opposite: one can see that in -CPDA the collapse operation can be simulated by nondeterminism, hence -PDA and -CPDA recognize the same languages [AehligMO05]. It is also an open question whether all word languages recognized by CPDA are context-sensitive.
We have shown [collapse-data] that the collapse operation increases the expressive power of deterministic higher-order pushdown automata with data. In this model of automata each letter from the input word is equipped by a data value, which comes from an infinite set; these data values can be stored on the stack and compared with other data values. In such a setting the proof becomes easier than in the no-data case considered in this paper.
One can consider configuration graphs of -PDA and -CPDA, and their -closures. We know [collapsible] that there is a -CPDA whose configuration graph has undecidable MSO theory, hence which is not a configuration graph of an -PDA, nor an -closure of such, as they all have decidable MSO theories.
Engelfriet [Engelfriet91] showed that the hierarchies of word languages and of trees generated by PDA are strict (that is, for each there is a language recognized by an -PDA that is not recognized by any -PDA, and similarly for trees). As observed by Haußner and Kartzow [HeussnerKartzow], his proof works equally well for these hierarchies for CPDA, once we know that the reachability problem for -CPDA is -EXPTIME complete (which follows from Kobayashi and Ong [emptiness-n-1-exptime]).
2. Preliminaries
For natural numbers , , where , by we denote the set (which is empty if ).
In the whole paper, the letter is used exclusively for the order of pushdown automata, which is usually assumed to be fixed and known implicitly.
We now define stacks of order (-stacks for short). Traditionally, a -stack is just a single symbol, and a -stack for is a (possibly empty) sequence of nonempty -stacks. However, having a -stack that is a part of an -stack for , it is convenient to know where this -stack is located in the -stack. For this reason, we equip every element of a stack by its position, written as a vector of natural numbers. Thus, for a fixed alphabet (of stack symbols), a stack of order is a pair , where and is a vector of positive integers, called a position. Then, for we define -stacks by induction: a -stack is a list of nonempty -stacks (where, by convection, all -stacks are nonempty) for which there exist numbers such that, for , all positions in are of the form . By and we denote the the set of order- stacks, and the set of nonempty order- stack, respectively, where . The top of a stack is on the right.
For example, when we have a -stack , and , then the second -stack of the third -stack (counting from the bottom) of the bottommost -stack of is of the form , where and say where is located in an imaginary -stack; the numbers and should be the same in the whole .
For a -stack , where , let be the -stack obtained from by increasing the -th coordinate of all its positions by . For example , and .
Let us emphasize that when for two -stacks , we write , we mean that not only their contents are equal, but also positions contained in their -stacks are equal; thus, when and come from the same -stack, this actually means that and refer to the same -stack.
While comparing two stacks, we sometimes need to ignore positions contained in their -stacks, and compare only their contents. For a -stack , let positionless stack be the list of lists of … of lists of stack symbols obtained from by removing positions from all -stacks. We say that two -stacks are positionless-equal, denoted , when . When is a positionless -stack, there is a unique -stack such that ; we write for .
The size of a -stack , denoted , is the number of -stacks it contains. When , and , and is a valid -stack, we denote this -stack by . The operator “” is assumed to be right associative (i.e., e.g., ). When , and , by we denote the topmost -stack of , that is, . We use the name positionless topmost -stack for .
When is fixed, the stack operations of order are and for each . We can apply them to a nonempty -stack for , which gives the following:
-
•
, that is, we remove the topmost -stack; it is defined only when the topmost -stack contains at least two -stacks;
-
•
for , that is, we duplicate the topmost -stack, and then we replace the topmost stack symbol by , adjusting appropriately all positions.111 In the classical definition the topmost symbol can be changed only when (for it required that ). We make this (unimportant) extension to have a uniform definition of for all .
A deterministic word-recognizing pushdown automaton of order (-DPDA for short) is a tuple where is an input alphabet, is a stack alphabet, is an initial stack symbol, is a set of states, is an initial state, is a set of accepting states, and is a transition function that maps every element of into one of the following objects:
-
•
, where is an injective function, or
-
•
, where and is a stack operation of order at most .
A configuration of consists of a state and of a nonempty -stack, that is, it is an element of . The initial configuration consists of the initial state and of the -stack containing only one -stack, enclosing the initial stack symbol . We use the notation ; in particular for a configuration , denotes its state, and its stack. Additionally, for a set of tuples we define to be . In order to shorten the notation, for a configuration we sometimes write or for or , respectively.
We use a shorthand for a configuration to denote . A configuration is a successor of a configuration , if
-
•
, and for some , or
-
•
, and .
Notice that a configuration has
-
•
successors, if the transition is ;
-
•
no successors, if the operation is but there is only one -stack on the topmost -stack;
-
•
one successor, otherwise.
Next, we define a run of . For , let be a configuration. A run from to is a sequence such that, for each , is a successor of . We set and call the length of . The subrun is . For runs with , we write for the composition of and that is defined as expected. Sometimes we also consider infinite runs, such that the sequence is infinite. However, unless stated explicitly, a run is finite.
The word read by a run is a word over the input alphabet . For a run from a configuration to its successor , it is the empty word if the transition between them is of the form . If the transition is , this is the one-letter word consisting of the letter for which (this letter is determined uniquely, as is injective). For a longer run this is defined as the concatenation of the words read by the subruns for . A run is accepting if it ends in a configuration whose state is accepting. A word is accepted by if it is read by some accepting run starting in the initial configuration. The language recognized by is the set of words accepted by .
2.1. Collapsible -DPDA
In Section 4 we also use deterministic collapsible pushdown automata of order (-DCPDA for short). Such automata are defined like -DPDA, with the following differences. A -stack contains now three parts: a symbol from , a position, and a natural number, but still only the symbol (together with a state) is used to determine which transition is performed from a configuration. The operation sets the number in the topmost -stack to the current size of the -stack (while does not modify these numbers). We have a new stack operation . Its result is obtained from by removing its topmost -stacks, so that only of them are left, where is the number stored in (intuitively, we remove all -stacks on which the topmost -stack is present).
3. Relation between Word Languages and Trees
In this section we describe how word languages recognized by DPDA are related to trees generated by PDA. Before seeing how Theorem 2 implies Theorem 1, we need to define how -PDA are used to generate trees. We consider ranked, potentially infinite trees. Beside of the input alphabet we have a function ; a tree node labelled by some has always children.
Automata used to generate trees are defined like DPDA or DCPDA (in particular they are deterministic as well), with the difference that they do not have the set of accepting states, and that instead of the transitions, there are transitions, for , and for pairwise distinct states . If the transition from is , in a successor of we have and for some (in particular has no successors if ).
Let be the set of all configurations of reachable from the initial one, such that a transition should be performed from . If there is a configuration of reachable from the initial one, from which there is no run to a configuration from , by definition does not generate any tree. Otherwise, a tree generated by has runs from the initial configuration to a configuration from as its nodes. A node is labelled by such that . A node is its -th child (), if is the composition of and a run that uses a transition only in its first transition, and for which . Notice that the graph obtained this way is really an -labelled ranked tree.
We now see how Theorem 1 follows from Theorem 2. Let be the language recognized by a -DCPDA that is not recognized by any -DPDA, for any ( exists by Theorem 2). First, we transform into a -DCPDA , recognizing as well, such that each configuration of reachable from the initial one has a successor. Observe that the only reason why in there may be configurations with no successors is that it wants to empty a stack using a operation. To avoid such situations, should have some bottom-of-stack marker on the bottom of each -stack, and on the bottom of the -stack (a -stack containing only the marker). Thus, starts with the marker as the initial stack symbol, performs and , placing the original initial stack symbol . Then, whenever blocks because it wants to empty a stack, in the bottom-of-stack marker is uncovered; in such a situation starts some loop with no accepting state. There is also a technical detail, that a operation that would block , in can enter an accepting state; to overcome this problem, every operation ending in an accepting state should first end in some auxiliary, not accepting state, from which (if the bottom-of-stack marker is not seen) the accepting state is reached.
Next, we create a tree-generating -CPDA , which generates a tree over the alphabet , where and . It is obtained from in two steps. First, we replace each transition of by the transition , where . Then, in each transition we replace the resulting state by a fresh auxiliary state , and from (for any topmost stack symbol) we perform transition if was accepting, or transition if was not accepting (this way, after each step of the original automaton, we perform a transition or ). Notice that from each configuration of reachable from the initial one, there exists a run to a configuration from , as required by the definition of a tree-generating CPDA. Let be the tree generated by .
Finally, suppose that can also be generated by some -PDA (without collapse). From we create a word-recognizing -DPDA . We replace each transition of the form of by the transition , where . We replace each transition of by the transition for a fresh accepting state and some stack symbol ; from we perform the transition (thus, we replace by a pass through an accepting state). The same for a transition, but the fresh state is not accepting.
Notice that recognizes ; this contradicts our assumptions about , so is not generated by any -PDA. Indeed, take any word . We have an accepting run of that reads and starts in the initial configuration. This run corresponds to a run of , that is, to a path in from the root to a -labelled node. Letters of tell us which child the path chooses in -labelled nodes: if -th letter of is , then from the -th -labelled node of , the path continues to the -th child. This path corresponds also to a run of , so to a run of . This run starts in the initial configuration, ends with an accepting state, and reads ; thus, accepts . Similarly, each word accepted by is also accepted by .
We also recall that a tree is generated by a recursion scheme of order if and only if it is generated by a -CPDA [collapsible], and that a tree is generated by a safe recursion scheme of order if and only if it is generated by an -PDA [easy-trees]; this implies the “equivalently” parts of Theorem 1.
4. The Separating Language
In this section we define a language that can be recognized by a -DCPDA, but not by any -DPDA, for any . It is a language over the alphabet . For a word we define . Whenever in some prefix of there are more closing brackets than opening brackets, . Also when in the whole we have the same number of opening and closing brackets, . Otherwise, let be the number of stars in before the last opening bracket that is not closed. Let be the set of words , for any (i.e., these are words consisting of brackets and stars, followed by sharp symbols).
It is known that languages similar to can be recognized by a -DCPDA (cf., e.g., Aehlig, de Miranda, and Ong [AehligMO05]), but for completeness we briefly show it below. The -DCPDA uses three stack symbols: (used to mark the bottom of -stacks), (used to count brackets), (used to mark the bottommost -stack). The initial symbol is . The automaton first pushes , makes a copy of the -stack (i.e., it performs ), and pops (hence the first -stack is marked with , unlike any other -stack used later). Then, for an opening bracket we push , for a closing bracket we pop , and for a star we perform (where is the topmost stack symbol). Hence for each star we have a -stack and on the last -stack we have as many symbols as the number of currently open brackets. If for a closing bracket the topmost symbol is , it means that in the word read so far we have more closing brackets than opening brackets; in this case we should accept suffixes of the form , which is easy.
Finally, the symbol is read. If the topmost symbol is , we have read as many opening brackets as closing brackets, hence we should accept one symbol. Otherwise, the topmost symbol corresponds to the last opening bracket that is not closed. We execute the operation. It leaves the -stacks created by the stars read before this bracket, except one (plus the first -stack). Thus, the number of -stacks is precisely equal to . Now we should read as many symbols as we have -stacks, plus one (after each symbol we perform ), and then accept.
In the remaining part of the paper we prove that any -DPDA cannot recognize ; in particular all automata appearing in the following sections do not use collapse.
5. Overview of the Proof
Before we start the real proof, in this section we present its general structure, on the intuitive level. Let us first see why cannot be recognized by any -DPDA . Consider the input word
(where each bracket is matched, except the last opening bracket). Notice that equals the sum of all and , so , after reading , has to store all these numbers in its stack. Thus, it first stores the number on the stack (by repeating some stack symbol times), then it can mark that there was an opening bracket, then it stores , and so on (see Figure 1); none of these numbers can be removed later.
Now consider the prefix of that ends just after the -th closing bracket. Since is deterministic, the stack at the end of looks similar: it is just shorter, but for sure it ends to the right of the vertical line, which denotes the stack size after the last opening bracket. We see that . Thus, when sees a after , it has to remove (ignore) the numbers above , and sum the rest. In particular it passes the vertical line in some state . We see that for each , at the moment of crossing this line, the stack is the same (everything to the right of the line is removed), only the state can differ. So in fact each has to be different, since for each we expect a different behavior. This is a contradiction when is greater than the number of states.
It follows that is of order at least , and while reading at some moment a push of order has to be performed, where in the topmost -stack we don’t remember some of the numbers or (for example, in order to recognize , after each we can copy the topmost -stack, and remove a fragment of its copy, so that the matching opening bracket is on the top). But now we can consider the word
where the numbers in each copy of are independent (so in fact each is a different word). Notice that each ends by an unmatched opening bracket; they are matched by the closing brackets at the end of . We can now almost repeat the previous reasoning. First, equals the sum of all numbers, so they all have to be kept on the stack. Then, we draw a line after reading the last (that is, separating the -stacks created before that moment from those created later). By the order- argument, some number from each is not present in the topmost -stack after reading this , so it cannot be present above the line. Next, for each we try to end the word already after the -th closing bracket (among those at the end of , not those inside words ). When we have a after each of these prefixes, we have to go below the line and behave differently (include a different subset of those values which are not present above the line), so we have to cross the line in different states. This is again a contradiction when is greater than the number of states. By induction we can continue like this, and nesting the words again we can show that for each order of the DPDA there is a problem.
Although the above idea of the proof looks simple, formalizing it is not straightforward. We have to deal with the following issues:
-
(1)
Above we have argued why a -DPDA cannot deal correctly with the word . But in fact we should consider any -DPDA, and prove that it is impossible that it stores all numbers from inside one -stack. Then there arises a problem: when crossing “the line” it is no longer true that the stack can only be of one form. Indeed, the topmost -stack has one fixed form, but we can cross the line in a copy of this -stack, with anything below this -stack. We can even cross the line multiple times, in several copies of the -stack. Thus, it is no longer true that the number of states gives the number of ways in which we can visit a substack. The ways of visiting a substack are described by types of stacks and by types of sequences of configurations, defined in Section LABEL:sec:types. The key point is that there are finitely many types for a fixed DPDA.
-
(2)
Where exactly is a number stored in a stack? And, where exactly “the line” should be placed? This is not sharp, since a DPDA may delay some stack operations by keeping information in its state, as well as it may temporarily create some fancy redundant structures on the stack, which are removed later in the run. To deal with this issue, in Section LABEL:sec:milestone we define milestone configurations. Intuitively, these are configurations in which no additional garbage is present on the stack.
-
(3)
Finally, why it would be wrong when, while reading the symbols, the automaton did not visit a place where there is stored a number that is a part of ? Maybe, accidentally, this number is equal to some other amount in the stack. Or maybe it was propagated to some other region on the stack by some involved manipulations. To overcome this difficulty, in Section LABEL:sec:pumping we prove a pumping lemma. It allows to change any of the numbers in the input word, without altering too much the whole stack. If some number (included in ) is changed, the DPDA has to enter the part of the stack changed by the pumping lemma; otherwise it would incorrectly accept after the same number of the symbols for two words with different .
6. The History Function and Special Runs
We begin this section by defining the history function. Then we define two classes of runs that are particularly interesting for us, namely -upper runs and -returns.
For any run and any -stack of , where , we define a -stack . Intuitively, is the (unique) -stack of , which evolved to the -stack in . Formally, we define by induction on the length of , starting with the case of . When , we take . Consider now a longer run with . We take if the last transition of is or performs , as well as if the transition performs and is not in the topmost -stack of . If the last transition of performs and is in the topmost -stack of , then , where is equal to with the -th coordinate of its position decreased by (i.e., is the -stack of from which was obtained as a copy). Notice that (for technical convenience) works in this way also for the topmost -stack, although the content of the topmost -stack changes during the operation. For , we define to be the -stack of containing for all -stacks in (observe that when , are two -stacks in , the -stacks and are in the same -stack).
It is important to notice that whenever , then . In the sequel we extensively use this property, which we call compositionality of histories.
For , we say that a run is -upper if ; let be the set of all such runs. Intuitively, a run is -upper when the topmost -stack of is a copy of the topmost -stack of , but possibly some changes were made to it. Notice that contains all runs, for , and for a run with it holds (the last property is by compositionality of histories).
For , a run is a -return if
-
•
, and
-
•
for all .
Let be the set of -returns. Observe that . Intuitively, is a -return when the topmost -stack of is obtained from the topmost -stack of by removing its topmost -stack (but not only in the sense of contents, but we require that really it was obtained this way).
Consider a -DPDA, and its run of length in which , and in which the operations between consecutive configurations are
Recall that our definition is that a of any order can change the topmost stack symbol. The contents of the stacks of the configurations in the run, and subruns being -upper runs and -returns are presented in Table 1.
Notice that is not a -return. We have .
6.1. Basic Properties of Runs
We now state several easy propositions, which are useful later, and also give more intuition about the above definitions.
Proposition 3.
Let be a -upper run (where ) such that for each . Then either
-
•
; additionally for every -stack in , is the corresponding -stack in , or
-
•
and the only transition of performs for , or for .
Proof 6.1.
For we immediately fall into one of the possibilities. Otherwise, we look at the history of the topmost -stack of . It is covered by the first operation of , and then it is not the topmost -stack until . Thus, it remains unchanged (we have the first possibility). ∎
Next, we give four propositions about -upper runs and -returns.
Proposition 4.
Let be a -upper run, where . Then is -upper if and only if for each such that .
Proposition 5.
Let be a -upper run in which is -upper, where . Then is -upper.
Proposition 6.
Let be a run that is not -upper, where . Suppose that is -upper for the greatest index such that is -upper (in particular such an index exists). Then is a -return.
Proposition 7.
Let be a -return, where . Then . Additionally for every -stack in , is the corresponding -stack in .