This paper was converted on www.awesomepapers.org from LaTeX by an anonymous user.
Want to know more? Visit the Converter page.

\lmcsdoi

16311 \lmcsheadingLABEL:LastPageApr. 18, 2014Aug. 20, 2020

On the Expressive Power of
  Higher-Order Pushdown Systems

Paweł Parys University of Warsaw, ul. Banacha 2, 02-097 Warszawa, Poland [email protected]
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 schemes
1991 Mathematics Subject Classification:
F.1.1. Models of computation—Relations between models
Work supported by the National Science Center (decision DEC-2012/07/D/ST6/02443). The author holds a post-doctoral position supported by Warsaw Center of Mathematics and Computer Science.
\titlecomment

This 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 (nn-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 nn-PDA coincides with the class of trees generated by order-nn 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-nn recursion schemes (safety is a syntactic restriction on the recursion scheme), and Caucal [Caucal02] gave another characterization: trees of order n+1n+1 are obtained from trees of order nn 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 nn-PDA to order-nn collapsible pushdown automata (nn-CPDA) by introducing a new stack operation called collapse, and proved that the class of trees generated by nn-CPDA coincides with the class of trees generated by order-nn recursion schemes (earlier, Knapik, Niwiński, Urzyczyn, and Walukiewicz [panic] introduced panic automata, a model equivalent to 22-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 22-CPDA that is not generated by any 22-PDA. We prove the following stronger property.

Theorem 1.

There is a tree generated by a 22-CPDA (equivalently, by a recursion scheme of order 22) that is not generated by any nn-PDA, for any nn (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 22-CPDA that is not recognized by any deterministic nn-PDA, for any nn.

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 22 and is opposite: one can see that in 22-CPDA the collapse operation can be simulated by nondeterminism, hence 22-PDA and 22-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 nn-PDA and nn-CPDA, and their ε\varepsilon-closures. We know [collapsible] that there is a 22-CPDA whose configuration graph has undecidable MSO theory, hence which is not a configuration graph of an nn-PDA, nor an ε\varepsilon-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 nn there is a language recognized by an nn-PDA that is not recognized by any (n1)(n-1)-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 nn-CPDA is (n1)(n-1)-EXPTIME complete (which follows from Kobayashi and Ong [emptiness-n-1-exptime]).

2. Preliminaries

For natural numbers aa, bb, where ba1b\geq a-1, by [a,b][a,b] we denote the set {a,,b}\{a,\dots,b\} (which is empty if b=a1b=a-1).

In the whole paper, the letter nn 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 kk (kk-stacks for short). Traditionally, a 0-stack is just a single symbol, and a kk-stack for k1k\geq 1 is a (possibly empty) sequence of nonempty (k1)(k-1)-stacks. However, having a kk-stack that is a part of an rr-stack for k<rk<r, it is convenient to know where this kk-stack is located in the rr-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 Γ\Gamma (of stack symbols), a stack of order 0 is a pair (γ,x)(\gamma,x), where γΓ\gamma\in\Gamma and x=(xn,xn1,,x1)x=(x_{n},x_{n-1},\dots,x_{1}) is a vector of nn positive integers, called a position. Then, for k[1,n]k\in[1,n] we define kk-stacks by induction: a kk-stack is a list [s1,s2,,sm][s_{1},s_{2},\dots,s_{m}] of nonempty (k1)(k-1)-stacks (where, by convection, all 0-stacks are nonempty) for which there exist numbers xn,xn1,,xk+1x_{n},x_{n-1},\dots,x_{k+1} such that, for i[1,m]i\in[1,m], all positions in sis_{i} are of the form (xn,xn1,,xk+1,i,yk1,yk2,,y1)(x_{n},x_{n-1},\dots,x_{k+1},i,y_{k-1},y_{k-2},\dots,y_{1}). By Γk\Gamma^{k}_{*} and Γ+k\Gamma^{k}_{+} we denote the the set of order-kk stacks, and the set of nonempty order-kk stack, respectively, where k[0,n]k\in[0,n]. The top of a stack is on the right.

For example, when we have a 33-stack ss, and n=5n=5, then the second 0-stack of the third 11-stack (counting from the bottom) of the bottommost 22-stack of ss is of the form (γ,(x5,x4,1,3,2))(\gamma,(x_{5},x_{4},1,3,2)), where x5x_{5} and x4x_{4} say where ss is located in an imaginary 55-stack; the numbers x5x_{5} and x4x_{4} should be the same in the whole ss.

For a kk-stack sks^{k}, where k[0,n1]k\in[0,n-1], let 𝗉+1(sk)\mathsf{p}_{+1}(s^{k}) be the kk-stack obtained from sks^{k} by increasing the (nk)(n-k)-th coordinate of all its positions by 11. For example 𝗉+1((γ,(2,3)))=(γ,(2,4))\mathsf{p}_{+1}((\gamma,(2,3)))=(\gamma,(2,4)), and 𝗉+1([(γ,(2,1)),(γ,(2,2))])=[(γ,(3,1)),(γ,(3,2))]\mathsf{p}_{+1}([(\gamma,(2,1)),(\gamma,(2,2))])=[(\gamma,(3,1)),(\gamma,(3,2))].

Let us emphasize that when for two kk-stacks sks^{k}, tkt^{k} we write sk=tks^{k}=t^{k}, we mean that not only their contents are equal, but also positions contained in their 0-stacks are equal; thus, when sks^{k} and tkt^{k} come from the same nn-stack, this actually means that sks^{k} and tkt^{k} refer to the same kk-stack.

While comparing two stacks, we sometimes need to ignore positions contained in their 0-stacks, and compare only their contents. For a kk-stack sks^{k}, let positionless stack 𝗉𝗈𝗌(sk)\mathsf{pos}{\downarrow}(s^{k}) be the list of lists of … of lists of stack symbols obtained from sks^{k} by removing positions from all 0-stacks. We say that two kk-stacks sk,tks^{k},t^{k} are positionless-equal, denoted sktks^{k}\cong t^{k}, when 𝗉𝗈𝗌(sk)=𝗉𝗈𝗌(tk)\mathsf{pos}{\downarrow}(s^{k})=\mathsf{pos}{\downarrow}(t^{k}). When sns^{n}_{-} is a positionless nn-stack, there is a unique nn-stack sns^{n} such that sn=𝗉𝗈𝗌(sn)s^{n}_{-}=\mathsf{pos}{\downarrow}(s^{n}); we write 𝗉𝗈𝗌+(sn)\mathsf{pos}_{+}(s^{n}_{-}) for sns^{n}.

The size of a kk-stack sks^{k}, denoted |sk||s^{k}|, is the number of (k1)(k-1)-stacks it contains. When sk=[s1,s2,,sm]Γks^{k}=[s_{1},s_{2},\dots,s_{m}]\in\Gamma^{k}_{*}, and sk1Γ+k1s^{k-1}\in\Gamma^{k-1}_{+}, and [s1,s2,,sm,sk1][s_{1},s_{2},\dots,s_{m},s^{k-1}] is a valid kk-stack, we denote this kk-stack by sk:sk1s^{k}:s^{k-1}. The operator “::” is assumed to be right associative (i.e., e.g., s2:s1:s0=s2:(s1:s0)s^{2}:s^{1}:s^{0}=s^{2}:(s^{1}:s^{0})). When 0kr0\leq k\leq r, and sr=tr:tr1::tkΓ+rs^{r}=t^{r}:t^{r-1}:\dots:t^{k}\in\Gamma^{r}_{+}, by 𝗍𝗈𝗉k(sr)\mathsf{top}^{k}(s^{r}) we denote the topmost kk-stack of srs^{r}, that is, tkt^{k}. We use the name positionless topmost kk-stack for 𝗉𝗈𝗌(𝗍𝗈𝗉k())\mathsf{pos}{\downarrow}(\mathsf{top}^{k}(\cdot)).

When Γ\Gamma is fixed, the stack operations of order k1k\geq 1 are 𝗉𝗈𝗉k\mathsf{pop}^{k} and 𝗉𝗎𝗌𝗁γk\mathsf{push}^{k}_{\gamma} for each γΓ\gamma\in\Gamma. We can apply them to a nonempty rr-stack for rkr\geq k, which gives the following:

  • 𝗉𝗈𝗉k(sr:sr1::sk:sk1)=sr:sr1::sk\mathsf{pop}^{k}(s^{r}:s^{r-1}:\dots:s^{k}:s^{k-1})=s^{r}:s^{r-1}:\dots:s^{k}, that is, we remove the topmost (k1)(k-1)-stack; it is defined only when the topmost kk-stack contains at least two (k1)(k-1)-stacks;

  • 𝗉𝗎𝗌𝗁γk(sr:sr1::s0)=sr:sr1::sk+1:(sk:sk1::s0):𝗉+1(sk1:sk2::s1:(γ,x))\mathsf{push}^{k}_{\gamma}(s^{r}:s^{r-1}:\dots:s^{0})=s^{r}:s^{r-1}:\dots:s^{k+1}:(s^{k}:s^{k-1}:\dots:s^{0}):\mathsf{p}_{+1}(s^{k-1}:s^{k-2}:\dots:s^{1}:(\gamma,x)) for s0=(γ,x)s^{0}=(\gamma^{\prime},x), that is, we duplicate the topmost (k1)(k-1)-stack, and then we replace the topmost stack symbol by γ\gamma, adjusting appropriately all positions.111 In the classical definition the topmost symbol can be changed only when k=1k=1 (for k2k\geq 2 it required that γ=γ\gamma=\gamma^{\prime}). We make this (unimportant) extension to have a uniform definition of 𝗉𝗎𝗌𝗁k\mathsf{push}^{k} for all kk.

A deterministic word-recognizing pushdown automaton of order nn (nn-DPDA for short) is a tuple (A,Γ,γI,Q,qI,F,δ)(A,\Gamma,\gamma_{I},Q,q_{I},F,\delta) where AA is an input alphabet, Γ\Gamma is a stack alphabet, γIΓ\gamma_{I}\in\Gamma is an initial stack symbol, QQ is a set of states, qIQq_{I}\in Q is an initial state, FQF\subseteq Q is a set of accepting states, and δ\delta is a transition function that maps every element of Q×ΓQ\times\Gamma into one of the following objects:

  • 𝗋𝖾𝖺𝖽(q)\mathsf{read}(\vec{q}), where q:AQ\vec{q}:A\to Q is an injective function, or

  • (q,op)(q,op), where qQq\in Q and opop is a stack operation of order at most nn.

A configuration of 𝒜{\mathcal{A}} consists of a state and of a nonempty nn-stack, that is, it is an element of Q×Γ+nQ\times\Gamma_{+}^{n}. The initial configuration consists of the initial state qIq_{I} and of the nn-stack containing only one 0-stack, enclosing the initial stack symbol γI\gamma_{I}. We use the notation πi((p1,,pk))=pi\pi_{i}((p_{1},\dots,p_{k}))=p_{i}; in particular for a configuration cc, π1(c)\pi_{1}(c) denotes its state, and π2(c)\pi_{2}(c) its stack. Additionally, for a set XX of tuples we define πi(X)\pi_{i}(X) to be {πi(p):pX}\{\pi_{i}(p)\colon\,p\in X\}. In order to shorten the notation, for a configuration cc we sometimes write 𝗍𝗈𝗉k(c)\mathsf{top}^{k}(c) or 𝗉𝗈𝗉k(c)\mathsf{pop}^{k}(c) for 𝗍𝗈𝗉k(π2(c))\mathsf{top}^{k}(\pi_{2}(c)) or 𝗉𝗈𝗉k(π2(c))\mathsf{pop}^{k}(\pi_{2}(c)), respectively.

We use a shorthand δ(c)\delta(c) for a configuration cc to denote δ(π1(c),𝗉𝗈𝗌(𝗍𝗈𝗉0(c)))\delta(\pi_{1}(c),\mathsf{pos}{\downarrow}(\mathsf{top}^{0}(c))). A configuration dd is a successor of a configuration cc, if

  • δ(c)=𝗋𝖾𝖺𝖽(q)\delta(c)=\mathsf{read}(\vec{q}), and d=(q(a),π2(c))d=(\vec{q}(a),\pi_{2}(c)) for some aAa\in A, or

  • δ(c)=(q,op)\delta(c)=(q,op), and d=(q,op(π2(c)))d=(q,op(\pi_{2}(c))).

Notice that a configuration cc has

  • |A||A| successors, if the transition is 𝗋𝖾𝖺𝖽(q)\mathsf{read}(\vec{q});

  • no successors, if the operation is 𝗉𝗈𝗉k\mathsf{pop}^{k} but there is only one (k1)(k-1)-stack on the topmost kk-stack;

  • one successor, otherwise.

Next, we define a run of 𝒜{\mathcal{A}}. For 0im0\leq i\leq m, let cic_{i} be a configuration. A run RR from c0c_{0} to cmc_{m} is a sequence c0,c1,,cmc_{0},c_{1},\dots,c_{m} such that, for each i[1,m]i\in[1,m], cic_{i} is a successor of ci1c_{i-1}. We set R(i)=ciR(i)=c_{i} and call |R|=m\lvert R\rvert=m the length of RR. The subrun Ri,jR{\restriction}_{i,j} is ci,ci+1,,cjc_{i},c_{i+1},\dots,c_{j}. For runs R,SR,S with R(|R|)=S(0)R(\lvert R\rvert)=S(0), we write RSR\circ S for the composition of RR and SS that is defined as expected. Sometimes we also consider infinite runs, such that the sequence c0,c1,c2,c_{0},c_{1},c_{2},\dots is infinite. However, unless stated explicitly, a run is finite.

The word read by a run is a word over the input alphabet AA. For a run from a configuration cc to its successor dd, it is the empty word if the transition between them is of the form (q,op)(q,op). If the transition is 𝗋𝖾𝖺𝖽(q)\mathsf{read}(\vec{q}), this is the one-letter word consisting of the letter aa for which π1(d)=q(a)\pi_{1}(d)=\vec{q}(a) (this letter is determined uniquely, as q\vec{q} is injective). For a longer run RR this is defined as the concatenation of the words read by the subruns Ri1,iR{\restriction}_{i-1,i} for i[1,|R|]i\in[1,|R|]. A run is accepting if it ends in a configuration whose state is accepting. A word ww is accepted by 𝒜{\mathcal{A}} if it is read by some accepting run starting in the initial configuration. The language recognized by 𝒜{\mathcal{A}} is the set of words accepted by 𝒜{\mathcal{A}}.

2.1. Collapsible 22-DPDA

In Section 4 we also use deterministic collapsible pushdown automata of order 22 (22-DCPDA for short). Such automata are defined like 22-DPDA, with the following differences. A 0-stack contains now three parts: a symbol from Γ\Gamma, 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 𝗉𝗎𝗌𝗁γ1\mathsf{push}^{1}_{\gamma} operation sets the number in the topmost 0-stack to the current size of the 22-stack (while 𝗉𝗎𝗌𝗁γ2\mathsf{push}^{2}_{\gamma} does not modify these numbers). We have a new stack operation 𝖼𝗈𝗅𝗅𝖺𝗉𝗌𝖾\mathsf{collapse}. Its result 𝖼𝗈𝗅𝗅𝖺𝗉𝗌𝖾(s)\mathsf{collapse}(s) is obtained from ss by removing its topmost 11-stacks, so that only k1k-1 of them are left, where kk is the number stored in 𝗍𝗈𝗉0(s)\mathsf{top}^{0}(s) (intuitively, we remove all 11-stacks on which the topmost 0-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 nn-PDA are used to generate trees. We consider ranked, potentially infinite trees. Beside of the input alphabet AA we have a function 𝑟𝑎𝑛𝑘:A\mathit{rank}\colon A\to\mathbb{N}; a tree node labelled by some aAa\in A has always 𝑟𝑎𝑛𝑘(a)\mathit{rank}(a) 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 𝗋𝖾𝖺𝖽(q)\mathsf{read}(\vec{q}) transitions, there are 𝖻𝗋𝖺𝗇𝖼𝗁(a,q1,q2,,q𝑟𝑎𝑛𝑘(a))\mathsf{branch}(a,q_{1},q_{2},\dots,q_{\mathit{rank}(a)}) transitions, for aAa\in A, and for pairwise distinct states q1,q2,,q𝑟𝑎𝑛𝑘(a)Qq_{1},q_{2},\dots,q_{\mathit{rank}(a)}\in Q. If the transition from cc is δ(c)=𝖻𝗋𝖺𝗇𝖼𝗁(a,q1,q2,,q𝑟𝑎𝑛𝑘(a))\delta(c)=\mathsf{branch}(a,q_{1},q_{2},\dots,q_{\mathit{rank}(a)}), in a successor dd of cc we have π2(d)=π2(c)\pi_{2}(d)=\pi_{2}(c) and π1(d)=qi\pi_{1}(d)=q_{i} for some i[1,𝑟𝑎𝑛𝑘(a)]i\in[1,\mathit{rank}(a)] (in particular cc has no successors if 𝑟𝑎𝑛𝑘(a)=0\mathit{rank}(a)=0).

Let T(𝒜)T({\mathcal{A}}) be the set of all configurations cc of 𝒜{\mathcal{A}} reachable from the initial one, such that a 𝖻𝗋𝖺𝗇𝖼𝗁\mathsf{branch} transition should be performed from cc. If there is a configuration of 𝒜{\mathcal{A}} reachable from the initial one, from which there is no run to a configuration from T(𝒜)T({\mathcal{A}}), by definition 𝒜{\mathcal{A}} does not generate any tree. Otherwise, a tree generated by 𝒜{\mathcal{A}} has runs from the initial configuration to a configuration from T(𝒜)T({\mathcal{A}}) as its nodes. A node RR is labelled by aAa\in A such that δ(R(|R|))=𝖻𝗋𝖺𝗇𝖼𝗁(a,q1,q2,,q𝑟𝑎𝑛𝑘(a))\delta(R(|R|))=\mathsf{branch}(a,q_{1},q_{2},\dots,q_{\mathit{rank}(a)}). A node SS is its ii-th child (1i𝑟𝑎𝑛𝑘(a)1\leq i\leq\mathit{rank}(a)), if SS is the composition of RR and a run SS^{\prime} that uses a 𝖻𝗋𝖺𝗇𝖼𝗁\mathsf{branch} transition only in its first transition, and for which π1(S(1))=qi\pi_{1}(S^{\prime}(1))=q_{i}. Notice that the graph obtained this way is really an AA-labelled ranked tree.

We now see how Theorem 1 follows from Theorem 2. Let LAL\subseteq A^{*} be the language recognized by a 22-DCPDA 𝒜{\mathcal{A}} that is not recognized by any nn-DPDA, for any nn (LL exists by Theorem 2). First, we transform 𝒜{\mathcal{A}} into a 22-DCPDA {\mathcal{B}}, recognizing LL as well, such that each configuration of {\mathcal{B}} reachable from the initial one has a successor. Observe that the only reason why in 𝒜{\mathcal{A}} there may be configurations with no successors is that it wants to empty a stack using a 𝗉𝗈𝗉\mathsf{pop} operation. To avoid such situations, {\mathcal{B}} should have some bottom-of-stack marker \bot on the bottom of each 11-stack, and on the bottom of the 22-stack (a 11-stack containing only the \bot marker). Thus, {\mathcal{B}} starts with the \bot marker as the initial stack symbol, performs 𝗉𝗎𝗌𝗁2\mathsf{push}^{2}_{\bot} and 𝗉𝗎𝗌𝗁γI1\mathsf{push}^{1}_{\gamma_{I}}, placing the original initial stack symbol γI\gamma_{I}. Then, whenever 𝒜{\mathcal{A}} blocks because it wants to empty a stack, in {\mathcal{B}} the bottom-of-stack marker is uncovered; in such a situation {\mathcal{B}} starts some loop with no accepting state. There is also a technical detail, that a 𝗉𝗈𝗉\mathsf{pop} operation that would block 𝒜{\mathcal{A}}, in {\mathcal{B}} can enter an accepting state; to overcome this problem, every 𝗉𝗈𝗉\mathsf{pop} 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 22-CPDA 𝒞{\mathcal{C}}, which generates a tree over the alphabet B={X,Y,Z}B=\{{X},{Y},{Z}\}, where 𝑟𝑎𝑛𝑘(X)=|A|\mathit{rank}({X})=|A| and 𝑟𝑎𝑛𝑘(Y)=𝑟𝑎𝑛𝑘(Z)=1\mathit{rank}({Y})=\mathit{rank}({Z})=1. It is obtained from {\mathcal{B}} in two steps. First, we replace each transition 𝗋𝖾𝖺𝖽(q)\mathsf{read}(\vec{q}) of {\mathcal{B}} by the transition 𝖻𝗋𝖺𝗇𝖼𝗁(X,q(a1),q(a2),,q(a|A|))\mathsf{branch}({X},\vec{q}(a_{1}),\vec{q}(a_{2}),\dots,\vec{q}(a_{|A|})), where A={a1,,a|A|}A=\{a_{1},\dots,a_{|A|}\}. Then, in each transition we replace the resulting state qq by a fresh auxiliary state q¯\overline{q}, and from q¯\overline{q} (for any topmost stack symbol) we perform transition 𝖻𝗋𝖺𝗇𝖼𝗁(Y,q)\mathsf{branch}({Y},q) if qq was accepting, or transition 𝖻𝗋𝖺𝗇𝖼𝗁(Z,q)\mathsf{branch}({Z},q) if qq was not accepting (this way, after each step of the original automaton, we perform a transition 𝖻𝗋𝖺𝗇𝖼𝗁(Y,)\mathsf{branch}({Y},\cdot) or 𝖻𝗋𝖺𝗇𝖼𝗁(Z,)\mathsf{branch}({Z},\cdot)). Notice that from each configuration of 𝒞{\mathcal{C}} reachable from the initial one, there exists a run to a configuration from T(𝒞)T({\mathcal{C}}), as required by the definition of a tree-generating CPDA. Let t𝒞t_{\mathcal{C}} be the tree generated by 𝒞{\mathcal{C}}.

Finally, suppose that t𝒞t_{\mathcal{C}} can also be generated by some nn-PDA 𝒟{\mathcal{D}} (without collapse). From 𝒟{\mathcal{D}} we create a word-recognizing nn-DPDA {\mathcal{E}}. We replace each transition of the form 𝖻𝗋𝖺𝗇𝖼𝗁(X,q1,q2,,q|A|)\mathsf{branch}({X},q_{1},q_{2},\dots,q_{|A|}) of 𝒟{\mathcal{D}} by the transition 𝗋𝖾𝖺𝖽(q)\mathsf{read}(\vec{q}), where q(ai)=qi\vec{q}(a_{i})=q_{i}. We replace each transition 𝖻𝗋𝖺𝗇𝖼𝗁(Y,q)\mathsf{branch}({Y},q) of 𝒟{\mathcal{D}} by the transition (p,𝗉𝗎𝗌𝗁γ1)(p,\mathsf{push}^{1}_{\gamma}) for a fresh accepting state pp and some stack symbol γ\gamma; from (p,γ)(p,\gamma) we perform the transition (q,𝗉𝗈𝗉1)(q,\mathsf{pop}^{1}) (thus, we replace 𝖻𝗋𝖺𝗇𝖼𝗁(Y,q)\mathsf{branch}({Y},q) by a pass through an accepting state). The same for a 𝖻𝗋𝖺𝗇𝖼𝗁(Z,q)\mathsf{branch}({Z},q) transition, but the fresh state pp is not accepting.

Notice that {\mathcal{E}} recognizes LL; this contradicts our assumptions about LL, so t𝒞t_{\mathcal{C}} is not generated by any nn-PDA. Indeed, take any word wLw\in L. We have an accepting run of {\mathcal{B}} that reads ww and starts in the initial configuration. This run corresponds to a run of 𝒞{\mathcal{C}}, that is, to a path pp in t𝒞t_{\mathcal{C}} from the root to a Y{Y}-labelled node. Letters of ww tell us which child the path pp chooses in X{X}-labelled nodes: if ii-th letter of ww is aja_{j}, then from the ii-th X{X}-labelled node of pp, the path continues to the jj-th child. This path pp corresponds also to a run of 𝒟{\mathcal{D}}, so to a run of {\mathcal{E}}. This run starts in the initial configuration, ends with an accepting state, and reads ww; thus, {\mathcal{E}} accepts ww. Similarly, each word accepted by {\mathcal{E}} is also accepted by {\mathcal{B}}.

We also recall that a tree is generated by a recursion scheme of order 22 if and only if it is generated by a 22-CPDA [collapsible], and that a tree is generated by a safe recursion scheme of order nn if and only if it is generated by an nn-PDA [easy-trees]; this implies the “equivalently” parts of Theorem 1.

4. The Separating Language

In this section we define a language UU that can be recognized by a 22-DCPDA, but not by any nn-DPDA, for any nn. It is a language over the alphabet A={[,],,}A=\{[,],\star,\sharp\}. For a word w{[,],}w\in\{[,],\star\}^{*} we define 𝑠𝑡𝑎𝑟𝑠(w)\mathit{stars}(w). Whenever in some prefix of ww there are more closing brackets than opening brackets, 𝑠𝑡𝑎𝑟𝑠(w)=0\mathit{stars}(w)=0. Also when in the whole ww we have the same number of opening and closing brackets, 𝑠𝑡𝑎𝑟𝑠(w)=0\mathit{stars}(w)=0. Otherwise, let 𝑠𝑡𝑎𝑟𝑠(w)\mathit{stars}(w) be the number of stars in ww before the last opening bracket that is not closed. Let UU be the set of words w𝑠𝑡𝑎𝑟𝑠(w)+1w\sharp^{\mathit{stars}(w)+1}, for any w{[,],}w\in\{[,],\star\}^{*} (i.e., these are words ww consisting of brackets and stars, followed by 𝑠𝑡𝑎𝑟𝑠(w)+1\mathit{stars}(w)+1 sharp symbols).

It is known that languages similar to UU can be recognized by a 22-DCPDA (cf., e.g., Aehlig, de Miranda, and Ong [AehligMO05]), but for completeness we briefly show it below. The 22-DCPDA uses three stack symbols: XX (used to mark the bottom of 11-stacks), YY (used to count brackets), ZZ (used to mark the bottommost 11-stack). The initial symbol is XX. The automaton first pushes ZZ, makes a copy of the 11-stack (i.e., it performs 𝗉𝗎𝗌𝗁Z2\mathsf{push}^{2}_{Z}), and pops ZZ (hence the first 11-stack is marked with ZZ, unlike any other 11-stack used later). Then, for an opening bracket we push YY, for a closing bracket we pop YY, and for a star we perform 𝗉𝗎𝗌𝗁γ2\mathsf{push}^{2}_{\gamma} (where γ\gamma is the topmost stack symbol). Hence for each star we have a 11-stack and on the last 11-stack we have as many YY symbols as the number of currently open brackets. If for a closing bracket the topmost symbol is XX, 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 {[,],}\{[,],\star\}^{*}\sharp, which is easy.

Finally, the \sharp symbol is read. If the topmost symbol is XX, we have read as many opening brackets as closing brackets, hence we should accept one \sharp symbol. Otherwise, the topmost YY symbol corresponds to the last opening bracket that is not closed. We execute the 𝖼𝗈𝗅𝗅𝖺𝗉𝗌𝖾\mathsf{collapse} operation. It leaves the 11-stacks created by the stars read before this bracket, except one (plus the first 11-stack). Thus, the number of 11-stacks is precisely equal to 𝑠𝑡𝑎𝑟𝑠(w)\mathit{stars}(w). Now we should read as many \sharp symbols as we have 11-stacks, plus one (after each \sharp symbol we perform 𝗉𝗈𝗉2\mathsf{pop}^{2}), and then accept.

In the remaining part of the paper we prove that any nn-DPDA cannot recognize UU; 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 UU cannot be recognized by any 11-DPDA 𝒜{\mathcal{A}}. Consider the input word

w1=[n1[n2[nN[mN+1]mN]m1]m0[\displaystyle w_{1}=[\star^{n_{1}}[\star^{n_{2}}\dots[\star^{n_{N}}[\star^{m_{N+1}}]\star^{m_{N}}]\dots\star^{m_{1}}]\star^{m_{0}}[

(where each bracket is matched, except the last opening bracket). Notice that 𝑠𝑡𝑎𝑟𝑠(w1)\mathit{stars}(w_{1}) equals the sum of all nin_{i} and mim_{i}, so 𝒜{\mathcal{A}}, after reading w1w_{1}, has to store all these numbers in its stack. Thus, it first stores the number n1n_{1} on the stack (by repeating some stack symbol n1n_{1} times), then it can mark that there was an opening bracket, then it stores n2n_{2}, and so on (see Figure 1); none of these numbers can be removed later.

n1n_{1}
n2n_{2}
nNn_{N}
...
mN+1m_{N+1}
mNm_{N}
...
m0m_{0}
[[
[[
[[
[[
[[
]]
]]
]]
[[
Refer to caption
Figure 1. The stack of a 11-DPDA after reading the word w1w_{1}

Now consider the prefix w1,iw_{1,i} of w1w_{1} that ends just after the ii-th closing bracket. Since 𝒜{\mathcal{A}} is deterministic, the stack at the end of w1,iw_{1,i} 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 𝑠𝑡𝑎𝑟𝑠(w1,i)=n1++nNi\mathit{stars}(w_{1,i})=n_{1}+\dots+n_{N-i}. Thus, when 𝒜{\mathcal{A}} sees a \sharp after w1,iw_{1,i}, it has to remove (ignore) the numbers above nNin_{N-i}, and sum the rest. In particular it passes the vertical line in some state qiq_{i}. We see that for each ii, at the moment of crossing this line, the stack is the same (everything to the right of the line is removed), only the state qiq_{i} can differ. So in fact each qiq_{i} has to be different, since for each ii we expect a different behavior. This is a contradiction when NN is greater than the number of states.

It follows that 𝒜{\mathcal{A}} is of order at least 22, and while reading w1w_{1} at some moment a push of order 22 has to be performed, where in the topmost 11-stack we don’t remember some of the numbers nin_{i} or mim_{i} (for example, in order to recognize w1w_{1}, after each ]] we can copy the topmost 11-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

w2=w1n1w1n2w1nNw1mN+1]mN]m1]m0[,\displaystyle w_{2}=w_{1}\star^{n^{\prime}_{1}}w_{1}\star^{n^{\prime}_{2}}\dots w_{1}\star^{n^{\prime}_{N}}w_{1}\star^{m^{\prime}_{N+1}}]\star^{m^{\prime}_{N}}]\dots\star^{m^{\prime}_{1}}]\star^{m^{\prime}_{0}}[\,,

where the numbers ni,min_{i},m_{i} in each copy of w1w_{1} are independent (so in fact each w1w_{1} is a different word). Notice that each w1w_{1} ends by an unmatched opening bracket; they are matched by the closing brackets at the end of w2w_{2}. We can now almost repeat the previous reasoning. First, 𝑠𝑡𝑎𝑟𝑠(w2)\mathit{stars}(w_{2}) 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 w1w_{1} (that is, separating the 11-stacks created before that moment from those created later). By the order-11 argument, some number from each w1w_{1} is not present in the topmost 11-stack after reading this w1w_{1}, so it cannot be present above the line. Next, for each ii we try to end the word already after the ii-th closing bracket (among those at the end of w2w_{2}, not those inside words w1w_{1}). When we have a \sharp 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 NN is greater than the number of states. By induction we can continue like this, and nesting the words wnw_{n} 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. (1)

    Above we have argued why a 11-DPDA cannot deal correctly with the word w1w_{1}. But in fact we should consider any nn-DPDA, and prove that it is impossible that it stores all numbers from w1w_{1} inside one 11-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 11-stack has one fixed form, but we can cross the line in a copy of this 11-stack, with anything below this 11-stack. We can even cross the line multiple times, in several copies of the 11-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. (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. (3)

    Finally, why it would be wrong when, while reading the \sharp symbols, the automaton did not visit a place where there is stored a number that is a part of 𝑠𝑡𝑎𝑟𝑠()\mathit{stars}(\cdot)? 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 𝑠𝑡𝑎𝑟𝑠()\mathit{stars}(\cdot)) 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 \sharp symbols for two words with different 𝑠𝑡𝑎𝑟𝑠()\mathit{stars}(\cdot).

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 kk-upper runs and kk-returns.

For any run RR and any kk-stack sks^{k} of R(|R|)R(|R|), where k[0,n]k\in[0,n], we define a kk-stack 𝗁𝗂𝗌𝗍(R,sk)\mathsf{hist}(R,s^{k}). Intuitively, 𝗁𝗂𝗌𝗍(R,sk)\mathsf{hist}(R,s^{k}) is the (unique) kk-stack of R(0)R(0), which evolved to the kk-stack sks^{k} in R(|R|)R(|R|). Formally, we define 𝗁𝗂𝗌𝗍(R,sk)\mathsf{hist}(R,s^{k}) by induction on the length of RR, starting with the case of k=0k=0. When |R|=0|R|=0, we take 𝗁𝗂𝗌𝗍(R,s0)=s0\mathsf{hist}(R,s^{0})=s^{0}. Consider now a longer run R=STR=S\circ T with |T|=1|T|=1. We take 𝗁𝗂𝗌𝗍(R,s0)=𝗁𝗂𝗌𝗍(S,s0)\mathsf{hist}(R,s^{0})=\mathsf{hist}(S,s^{0}) if the last transition of RR is 𝗋𝖾𝖺𝖽\mathsf{read} or performs 𝗉𝗈𝗉\mathsf{pop}, as well as if the transition performs 𝗉𝗎𝗌𝗁γr\mathsf{push}^{r}_{\gamma} and s0s^{0} is not in the topmost (r1)(r-1)-stack of R(|R|)R(|R|). If the last transition of RR performs 𝗉𝗎𝗌𝗁γr\mathsf{push}^{r}_{\gamma} and s0s^{0} is in the topmost (r1)(r-1)-stack of R(|R|)R(|R|), then 𝗁𝗂𝗌𝗍(R,s0)=𝗁𝗂𝗌𝗍(S,t0)\mathsf{hist}(R,s^{0})=\mathsf{hist}(S,t^{0}), where t0t^{0} is equal to s0s^{0} with the (nr+1)(n-r+1)-th coordinate of its position decreased by 11 (i.e., t0t^{0} is the 0-stack of T(0)T(0) from which s0s^{0} was obtained as a copy). Notice that (for technical convenience) 𝗁𝗂𝗌𝗍\mathsf{hist} works in this way also for the topmost 0-stack, although the content of the topmost 0-stack changes during the 𝗉𝗎𝗌𝗁γr\mathsf{push}^{r}_{\gamma} operation. For k>0k>0, we define 𝗁𝗂𝗌𝗍(R,sk)\mathsf{hist}(R,s^{k}) to be the kk-stack of R(0)R(0) containing 𝗁𝗂𝗌𝗍(R,s0)\mathsf{hist}(R,s^{0}) for all 0-stacks s0s^{0} in sks^{k} (observe that when s0s^{0}, t0t^{0} are two 0-stacks in sks^{k}, the 0-stacks 𝗁𝗂𝗌𝗍(R,s0)\mathsf{hist}(R,s^{0}) and 𝗁𝗂𝗌𝗍(R,t0)\mathsf{hist}(R,t^{0}) are in the same kk-stack).

It is important to notice that whenever R=STR=S\circ T, then 𝗁𝗂𝗌𝗍(S,𝗁𝗂𝗌𝗍(T,sk))=𝗁𝗂𝗌𝗍(R,sk)\mathsf{hist}(S,\mathsf{hist}(T,s^{k}))=\mathsf{hist}(R,s^{k}). In the sequel we extensively use this property, which we call compositionality of histories.

For k[0,n]k\in[0,n], we say that a run RR is kk-upper if 𝗁𝗂𝗌𝗍(R,𝗍𝗈𝗉k(R(|R|)))=𝗍𝗈𝗉k(R(0))\mathsf{hist}(R,\mathsf{top}^{k}(R(|R|)))=\mathsf{top}^{k}(R(0)); let 𝗎𝗉k\mathsf{up}^{k} be the set of all such runs. Intuitively, a run RR is kk-upper when the topmost kk-stack of R(|R|)R(|R|) is a copy of the topmost kk-stack of R(0)R(0), but possibly some changes were made to it. Notice that 𝗎𝗉n\mathsf{up}^{n} contains all runs, 𝗎𝗉k𝗎𝗉l\mathsf{up}^{k}\subseteq\mathsf{up}^{l} for klk\leq l, and for a run RSR\circ S with S𝗎𝗉kS\in\mathsf{up}^{k} it holds R𝗎𝗉kRS𝗎𝗉kR\in\mathsf{up}^{k}\iff R\circ S\in\mathsf{up}^{k} (the last property is by compositionality of histories).

For k[1,n]k\in[1,n], a run RR is a kk-return if

  • 𝗁𝗂𝗌𝗍(R,𝗍𝗈𝗉k1(R(|R|)))=𝗍𝗈𝗉k1(𝗉𝗈𝗉k(R(0)))\mathsf{hist}(R,\mathsf{top}^{k-1}(R(|R|)))=\mathsf{top}^{k-1}(\mathsf{pop}^{k}(R(0))), and

  • Ri,|R|𝗎𝗉k1R{\restriction}_{i,|R|}\not\in\mathsf{up}^{k-1} for all i[0,|R|1]i\in[0,|R|-1].

Let 𝗋𝖾𝗍k\mathsf{ret}^{k} be the set of kk-returns. Observe that 𝗋𝖾𝗍k𝗎𝗉k\mathsf{ret}^{k}\subseteq\mathsf{up}^{k}. Intuitively, RR is a kk-return when the topmost kk-stack of R(|R|)R(|R|) is obtained from the topmost kk-stack of R(0)R(0) by removing its topmost (k1)(k-1)-stack (but not only in the sense of contents, but we require that really it was obtained this way).

{exa}

Consider a 22-DPDA, and its run RR of length 66 in which 𝗉𝗈𝗌(π2(R(0)))=[[a,b],[c,d]]\mathsf{pos}{\downarrow}(\pi_{2}(R(0)))=[[a,b],[c,d]], and in which the operations between consecutive configurations are

𝗉𝗎𝗌𝗁e2,𝗉𝗈𝗉1,𝗉𝗈𝗉2,𝗉𝗈𝗉1,𝗉𝗎𝗌𝗁d1,𝗉𝗈𝗉1.\displaystyle\mathsf{push}^{2}_{e}\,,\ \mathsf{pop}^{1}\,,\ \mathsf{pop}^{2}\,,\ \mathsf{pop}^{1}\,,\ \mathsf{push}^{1}_{d}\,,\ \mathsf{pop}^{1}\,.

Recall that our definition is that a 𝗉𝗎𝗌𝗁\mathsf{push} of any order can change the topmost stack symbol. The contents of the stacks of the configurations in the run, and subruns being kk-upper runs and kk-returns are presented in Table 1.

Table 1. Stack contents of the example run, and subruns being kk-upper runs and kk-returns
j𝗉𝗈𝗌(π2(R(j)))i:Ri,j𝗎𝗉0i:Ri,j𝗎𝗉1i:Ri,j𝗋𝖾𝗍1i:Ri,j𝗋𝖾𝗍20[[a,b],[c,d]]001[[a,b],[c,d],[c,e]]0,10,12[[a,b],[c,d],[c]]20,1,20,13[[a,b],[c,d]]0,30,31,24[[a,b],[c]]40,3,40,35[[a,b],[c,d]]4,50,3,4,56[[a,b],[c]]4,60,3,4,5,65\displaystyle\begin{array}[]{c|l|l|l|l|l}j&\mathsf{pos}{\downarrow}(\pi_{2}(R(j)))&i\colon\,R{\restriction}_{i,j}\in\mathsf{up}^{0}&i\colon\,R{\restriction}_{i,j}\in\mathsf{up}^{1}&i\colon\,R{\restriction}_{i,j}\in\mathsf{ret}^{1}&i\colon\,R{\restriction}_{i,j}\in\mathsf{ret}^{2}\\ \hline\cr 0&[[a,b],[c,d]]&0&0&-&-\\ 1&[[a,b],[c,d],[c,e]]&0,1&0,1&-&-\\ 2&[[a,b],[c,d],[c]]&2&0,1,2&0,1&-\\ 3&[[a,b],[c,d]]&0,3&0,3&-&1,2\\ 4&[[a,b],[c]]&4&0,3,4&0,3&-\\ 5&[[a,b],[c,d]]&4,5&0,3,4,5&-&-\\ 6&[[a,b],[c]]&4,6&0,3,4,5,6&5&-\end{array}

Notice that RR is not a 11-return. We have 𝗁𝗂𝗌𝗍(R0,5,(d,(2,2)))=(c,(2,1))\mathsf{hist}(R{\restriction}_{0,5},(d,(2,2)))=(c,(2,1)).

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 RR be a kk-upper run (where k[0,n]k\in[0,n]) such that Ri,|R|𝗎𝗉kR{\restriction}_{i,|R|}\not\in\mathsf{up}^{k} for each i[1,|R|1]i\in[1,|R|-1]. Then either

  • 𝗍𝗈𝗉k(R(0))𝗍𝗈𝗉k(R(|R|))\mathsf{top}^{k}(R(0))\cong\mathsf{top}^{k}(R(|R|)); additionally for every 0-stack s0s^{0} in 𝗍𝗈𝗉k(R(|R|))\mathsf{top}^{k}(R(|R|)), 𝗁𝗂𝗌𝗍(R,s0)\mathsf{hist}(R,s^{0}) is the corresponding 0-stack in 𝗍𝗈𝗉k(R(0))\mathsf{top}^{k}(R(0)), or

  • |R|=1|R|=1 and the only transition of RR performs 𝗉𝗈𝗉r\mathsf{pop}^{r} for rkr\leq k, or 𝗉𝗎𝗌𝗁γr\mathsf{push}^{r}_{\gamma} for rkr\leq k.

Proof 6.1.

For |R|1|R|\leq 1 we immediately fall into one of the possibilities. Otherwise, we look at the history of the topmost kk-stack of R(|R|)R(|R|). It is covered by the first operation of RR, and then it is not the topmost kk-stack until R(|R|)R(|R|). Thus, it remains unchanged (we have the first possibility). ∎

Next, we give four propositions about kk-upper runs and kk-returns.

Proposition 4.

Let RR be a kk-upper run, where k[1,n]k\in[1,n]. Then RR is (k1)(k-1)-upper if and only if |𝗍𝗈𝗉k(R(0))|𝗍𝗈𝗉k(R(i))||\mathsf{top}^{k}(R(0))|\leq\mathsf{top}^{k}(R(i))| for each i[0,|R|]i\in[0,|R|] such that Ri,|R|𝗎𝗉kR{\restriction}_{i,|R|}\in\mathsf{up}^{k}.

Proposition 5.

Let STS\circ T be a (k1)(k-1)-upper run in which TT is kk-upper, where k[1,n]k\in[1,n]. Then SS is (k1)(k-1)-upper.

Proposition 6.

Let RR be a run that is not (k1)(k-1)-upper, where k[1,n]k\in[1,n]. Suppose that R0,jR{\restriction}_{0,j} is (k1)(k-1)-upper for the greatest index j[0,|R|1]j\in[0,|R|-1] such that Rj,|R|R{\restriction}_{j,|R|} is kk-upper (in particular such an index jj exists). Then RR is a kk-return.

Proposition 7.

Let RR be a kk-return, where k[1,n]k\in[1,n]. Then 𝗉𝗈𝗉k(𝗍𝗈𝗉k(R(0)))𝗍𝗈𝗉k(R(|R|))\mathsf{pop}^{k}(\mathsf{top}^{k}(R(0)))\cong\mathsf{top}^{k}(R(|R|)). Additionally for every 0-stack s0s^{0} in 𝗍𝗈𝗉k(R(|R|))\mathsf{top}^{k}(R(|R|)), 𝗁𝗂𝗌𝗍(R,s0)\mathsf{hist}(R,s^{0}) is the corresponding 0-stack in 𝗉𝗈𝗉k(𝗍𝗈𝗉k(R(0)))\mathsf{pop}^{k}(\mathsf{top}^{k}(R(0))).