Rewriting Higher-Order Stack Trees

We briefly recall the notion of higher-order stacks (for details, see for instance [5]). In order to obtain a more straightforward extension from stacks to stack trees, we use a slightly tuned yet equivalent definition, whereby the hierarchy starts at order 0 and uses a different set of basic operations.

In the remainder, Γ will denote a fixed finite alphabet and n a positive integer. We first define stacks of order n (or n-stacks). Let S t a c k s ₀(Γ) = Γ denote the set of 0-stacks. For n > 0, the set of n-stacks is S t a c k s _n (Γ) = (S t a c k s _n−1(Γ))⁺, the set of non-empty sequences of (n − 1)-stacks. When Γ is understood, we simply write S t a c k s _n . For s ∈ S t a c k s _n , we write s = [s ₁…s _k ] _n , with k > 0 and n > 0, for an n-stack of size |s| = k whose topmost (n − 1)-stack is s _k . For example, [[[α β α]₁]₂[[α β α]₁[β]₁[α α]₁]₂]₃ is a 3-stack of size 2, whose topmost 2-stack [[α β α]₁[β]₁[α α]₁]₂ contains three 1-stacks, etc.

For the sake of simplicity, we will denote as [α] _n the n-stack containing only the symbol α, i.e. [[…[α]₁…] _n−1] _n .

We introduce the set \(ST_{n}(\Gamma ) = \mathcal {T}(Stacks_{n-1}(\Gamma ))\) (or simply S T _n when Γ is understood) of n-stack trees. Observe that an n-stack tree of degree 1 is isomorphic to an n-stack, and that \(ST_{1} = \mathcal {T}(\Gamma )\). Figure 1 shows an example of a 3-stack tree. The notion of stack trees therefore subsumes both higher-order stacks and ordinary trees.

In the previous definition, we consider that fr(t) = {u ₁,⋯ ,u _|fr(t)|}, and that the leaves are ordered in respect to the lexicographic order over {1,⋯ ,d}^∗. If i > |fr(t)|, there is no stack tree t ^′ such that \((t,t^{\prime }) \in r_{\theta }^{i}\). For simplicity, we will henceforth only consider the case where stack trees have arity at most 2 and k ≤ 2, but all results go through in the general case.

As already mentioned, S T ₁ is the set of trees labelled by Γ. In contrast with basic stack tree operations, a tree rewrite rule (ℓ,a,r) expresses the replacement of an arbitrarily large ground subtree ℓ of some tree s = c[ℓ] into r, yielding the tree c[r]. Contrarily to the case of order-1 stacks (which are simply words), composing basic stack tree operations does not allow us to directly express such an operation, because there is no guarantee that two successive operations will be applied to the same part of a tree. We thus need to find a way to consider compositions of basic operations acting on a single sub-tree. In our notations, the effect of a ground tree rewrite rule could thus be seen as the localised application of a sequence of rew and \(\overline {\text {copy}}_{1}^{2}\) operations followed by a sequence of rew and \(\text {copy}_{1}^{2}\) operations. The relative positions where these operations must be applied could be represented as a pair of trees with edge labels in O p s ₀.

From order 2 on, this is no longer possible. Indeed a localised sequence of operations may be used to perform introspection on the stack labelling a node without destroying it, by first performing a copy₂ operation followed by a sequence of order-1 operations and a \(\overline {\text {copy}}_{2}\) operation. It is thus impossible to directly represent such a transformation using pairs of trees labelled by stack tree operations. We therefore adopt a presentation of compound operations as DAGs, which allows us to specify the relative application positions of successive basic operations. However, not every DAG represents a valid compound operation, so we first need to define a suitable subclass of DAGs and associated concatenation operation. An example of the model we aim to define can be found in Fig. 2.

Additionally, the vertices of D are ordered inductively in such a way that every vertex of D _i in the above definition is smaller than the vertices of D _i+1, the order over □ being the trivial one. This induces in particular an order over the input vertices of D, and one over its output vertices.

Figure 2 shows an example of the application of a compound operation. Given a compound operation D, we define \(\overline {D}\) the operation obtained by reversing the edges of D and swapping the input and output vertices. Formally, for 𝜃 ∈ O p s _n−1(Γ), we define \(\overline {D_{\theta }} = D_{\overline {\theta }}\), \(\overline {D_{\text {copy}_{n}^{d}}} = D_{\overline {\text {copy}}_{n}^{d}}\), \(\overline {D_{\overline {\text {copy}}_{n}^{d}}} = D_{\text {copy}_{n}^{d}}\), and for every compound operations D ₁,D ₂, \(\overline {D_{1}\cdot _{i,j} D_{2}} = \overline {D_{2}} \cdot _{j,i} \overline {D_{1}}\). For every operation D, we have \(r_{\overline {D}} = r_{D}^{-1}\). Finally, given a k-tuple of operations D = (D ₁,…,D _k ) of respective in-degrees d ₁,…,d _k and a k-tuple of indices i = (i ₁,…,i _k ) with i _j+1 ≥ i _j + d _j for all j ∈{1,⋯ ,k}, we denote by \(r_{\mathbf {D}}^{\mathbf {i}}= r_{D_{k}}^{i_{k}}\circ \cdots \circ r_{D_{1}}^{i_{1}}\) the relation defined by the parallel application of each D _j to the position i _j , and by r _D the union of all these relations (we apply the rightmost DAGs first to not have to deal with the effect of the application of the leftmost DAGs to the numbering of the leaves).

Since the (i,j)-concatenation of two operations as defined above is not necessarily a licit operation, we need to restrict ourselves to results which are well-formed according to Definition 2. Given D and D ^′, we let D ⋅ D ^′ = {D⋅ _i,j D ^′∣D⋅ _i,j D ^′ is an operation}. Given n > 1, we define² \(D^{n} = \bigcup _{i <n} D^{i} \cdot D^{n-i}\), and let \(D^{*} = \bigcup _{n\geq 0} D^{n}\) denote the set of iterations of D. These notations are naturally extended to sets of operations.

In this paragraph, we show that Rec is closed under union, intersection and contains the finite sets of operations.

It is possible to extend the notion of ground stack tree rewriting systems to recognisable sets of operations. Such a system is called recognisable.

As in the case of ground tree rewriting systems, recognisable ground stack tree rewriting systems do not capture the iteration of the transition relation of any ground stack tree rewriting system, as such a system impose to rewrite only a given subtree, while the iteration of the transition relation may rewrite several subtrees in one step. For ground tree rewriting systems, this problem is lifted by the introduction of ground tree transducers which precisely allow to rewrite in parallel any number of subtrees with a set of rules in a recognisable set of rules (but without control on the number of subtrees rewritten that way). Following that idea, we define the relation defined by an automaton A as \(\mathcal {R}(A)= \{(t,t^{\prime })\mid \exists \mathbf {D} \in \text {Op}(A), (t,t^{\prime }) \in r_{\mathbf {D}}\}\).

Operations may perform “unnecessary” actions on a given stack tree, for instance duplicating a leaf with a \(\text {copy}_{n}^{2}\) operation and later destroying both copies with \(\overline {\text {copy}}_{n}^{2}\). Such operations which leave the input tree unchanged are referred to as bubbles. There are thus in general infinitely many operations representing the same relation over stack trees. It is therefore desirable to look for a canonical representative (a canonical operation) for each considered relation. The intuitive idea is to simplify operations by removing occurrences of successive mutually inverse basic operations. This process is a very classical tool in the literature of pushdown automata and related models, and was applied to higher-order stacks in [5]. Our notion of reduced operations is inspired from this work.

To define such a notion for our operations, there are two main hurdles to overcome. First, as already mentioned, a compound operation D can perform introspection on the label of a leaf without destroying it. If D can be applied to a given stack tree t, such a sequence of operations does not change the resulting stack tree s. It does however forbid the application of D to other stack trees by inspecting their node labels, hence removing this part of the computation would lead to an operation with a possibly strictly larger domain. To adress this problem, and following [5], we use test operations ranging over regular sets of (n − 1)-stacks, which will allow us to handle non-destructive node-label introspection.

A second difficulty appears when an operation destroys a subtree and then reconstructs it identically, for instance a \(\overline {\text {copy}}_{n}^{2}\) operation followed by \(\text {copy}_{n}^{2}\). Trying to remove such a pattern would lead to a disconnected DAG, which does not describe a compound operation in our sense. We thus need to leave such occurrences intact. We can nevertheless bound the number of times a given position of the input stack tree is affected by the application of an operation by considering two phases: a destructive phase during which only \(\overline {\text {copy}}_{n}^{i}\) and order- (n − 1) basic operations (possibly including tests) are performed on the input stack tree, and a constructive phase only consisting of \(\text {copy}_{n}^{i}\) and order- (n − 1) basic operations. This idea is similar to the way ground tree rewriting is performed at order 1.

The goal of this section is to define a subset of operations called reduced operations analogously to the notion of reduced instructions with tests in [5], and prove that any recognisable relation can be defined by a recognisable set of reduced operations. However, as in [5], we won’t have a unique reduced operation representing a given relation, due to the presence of tests, but it limits the number of times the same stack tree can be obtained during its application to a stack tree, which is exactly what we need in the proof of the next section. To that end, we will first formally define tests, define the notion of reduced operations with tests, and prove that any relation accepted by an automaton can be accepted by an automaton accepting reduced operation with tests (with some technical restrictions), called a normalised automaton. A key point in the proof of that fact will be to use the notion of loop-free sets of instructions presented in [5], and we will explain why we can apply it to our case, as we don’t have the same set of basic operations as them.

Formally, a test T _L over S t a c k s _n is the restriction of the identity operation to L ∈ R e c(S t a c k s _n ).³ In other words, given s ∈ S t a c k s _n , \((s,s) \in r_{T_{L}}\) if and only if s ∈ L. We denote by \(\mathcal {T}_{n}\) the set of test operations over S t a c k s _n . We enrich our basic operations over S T _n with \(\mathcal {T}_{n-1}\). We also extend compound operations with edges labelled by tests. We denote by \(\mathcal {D}_{n}^{\mathcal {T}}\) the set of basic operations with tests.

We now define a notion of reduced sequences of stack operations that will be sufficient for limiting the number of time a given stack tree appears during the application of a reduced operation. Informally, we say that a sequence over \(Ops_{n-1}\cup \mathcal {T}_{n-1}\) is reduced if and only if the only subsequences that define a relation that can leave a stack unchanged are single test operations.

If a sequence 𝜃 = 𝜃 ₁⋯𝜃 _k is reduced, then for every stack s such that there is a stack s ^′ such that (s,s ^′) ∈ r _𝜃 , the sequence s ₁,⋯ ,s _k−1 with \((s,s_{1}) \in r_{\theta _{1}}, (s_{1},s_{2}) \in r_{\theta _{2}}, \cdots ,(s_{k-1},s^{\prime })\in r_{\theta _{k}}\) is such that for any s _i ,s _j , if s _i = s _j , then j = i + 1 and \(\theta _{i} \in \mathcal {T}_{n-1}\). Notice, that this definition also implies that there are no two consecutive test operations in a reduced sequence. Thus, in the application of a reduced sequence, any stack will appear at most twice. Furthermore, we also ask that there are no two rew_a,b operations which can apply successively on the same letter. This prevents useless rewriting (as rew_a,brew_b,c is equivalent to rew_a,c).

For example, the sequence rew_a,acopy₁rew_a,b is not reduced as rew_a,a is not a test but \(([\alpha ]{}_{1},[\alpha ]{}_{1})\in r_{\text {rew}_{\mathrm {a},\mathrm {a}}}\). Yet, copy₁rew_a,b is reduced. The sequence \(\theta = \overline {\text {copy}}_{2}\text {rew}_{\mathrm {a},\mathrm {b}}\) \(\text {copy}_{1}T_{L}\overline {\text {cop}}_{1}\text {rew}_{\mathrm {b},\mathrm {a}}\text {copy}_{2}\) is not reduced as ([[α]₁[α]₁]₂,[[α]₁[α]₁]₂) ∈ r _𝜃 . The sequence \(\theta = \overline {\text {copy}}_{2}\text {rew}_{\mathrm {a},\mathrm {b}}\text {copy}_{2}\) is reduced. \(T_{L_{1}}\text {rew}_{\mathrm {a},\mathrm {b}}T_{L_{2}}\text {copy}_{1}T_{L_{3}}\) is reduced, as even if it has three test operations, they are not consecutive, and rew_a,bcopy₁ is reduced.

We can now define our notion of reduced stack tree operations. Informally, a stack tree operation is reduced if there is no \(\overline {\text {copy}}_{n}^{d}\) operation “below” a \(\text {copy}_{n}^{d}\) operation, and if any suboperation containing only stack operations is reduced.

Intuitively, a reduced operation will have a destructive part, which contains all the operations \(\overline {\text {copy}}_{n}^{d}\) and thus “goes up (and only up)” in the stack tree it is applied to, followed by a constructive part, which contains all the operations \(\text {copy}_{n}^{d}\) and thus “constructs a stack tree from the leaf it is applied to”, and never removes a leaf. Moreover, any suboperation that does not contain tree operation is reduced, preventing it to “loop” on a stack tree if it is not a single test operation.

We are now ready to present the main result of this section: a notion of normalisation for operation automata. An automaton A is said to be distinguished if there is no transition ending in an initial state or starting in a final state.

The idea of the construction is to transform A in several steps, each modifying the set of accepted operations but not the recognised relation. The proof relies on the closure properties of regular sets of (n − 1)-stacks and an analysis of the structure of A. This transformation can be performed without altering the accepted relation over stack trees. The end of this section is devoted to explain this construction.

Before moving to the main proof, we first have to explain how we can derive that for every recognisable set of stack operations there is a recognisable set of reduced stack operations defining the same relation, from [5]. Indeed, we will need that fact in our construction. In [5], the set of O p s ₁ contains operations of the form push _α and pop _α , while we have the operations rew _α,β , copy₁ and \(\overline {\text {cop}}_{1}\). Notice as well that in [5], there is an empty stack that we don’t consider in our model. Yet it is possible to simulate our operations with sets of sequences of push _α and pop _α , and vice-versa. For example, \(\text {push}_{\alpha } \sim \bigcup _{\beta \in \Gamma } \text {copy}_{1} \text {rew}_{\beta }{\alpha }\) (observe that the relations defined by a sequence in this union are disjoint), or \(\text {copy}_{1} \sim \bigcup _{\alpha \in \Gamma } \text {pop}_{\alpha } \text {push}_{\alpha } \text {push}_{\alpha }\). The remaining equivalences are similar and thus left to the reader.

Thus, as these are local transformations, any relation defined by a recognisable set for our notion is also defined by a recognisable set for the notion of [5], and vice-versa.

In [5], there is a notion of loop-free operations, which are operations without factors of the form \(\text {copy}_{i}\overline {\text {copy}}_{i}\), \(\overline {\text {copy}}_{i}\text {copy}_{i}\), push _a pop _a or pop _a push _a . Observe that a loop-free operation (without test) cannot contain a suboperation 𝜃 such that r _𝜃 ∩id≠∅, as an operation defining a test necessarily contains one of these factors. They extend this notion to operations with tests (an operation with test is loop-free if the one obtained by removing the tests is loop-free). Observe that a loop-free operation with tests is reduced in our sense (except that there may be several tests in a row – but one can find easily an equivalent operation reduced in our sense by shrinking these tests). Proposition 2.2 from [5] thus states that any set recognised by an automaton A over operations defines the same relation as a set recognised by an automaton A ^′ over \(Ops_{k} \cup \{T_{L_{q,q^{\prime }}}\mid q,q^{\prime } \in Q\}\) accepting only loop-free operations, where \(L_{q,q^{\prime }}\) is the set of stacks s, such that there is an operation 𝜃 recognised by A between states q and q ^′ such that (s,s) ∈ r _𝜃 . Furthermore, they show that the sets \(L_{q,q^{\prime }}\) are regular, so it is possible to compute A ^′.

Finally, observe that for any loop-free operation with tests in the sense of [5], we can find a finite set of reduced operations in our sense recognising the same relation, by applying the transformation described earlier, replacing the rew _α α with a test operation and merging the possible \(T_{L} T_{L^{\prime }}\) factors introduced that way with \(T_{L\cap L^{\prime }}\). Observe that a factor rew_a,b T _L rew _c d cannot appear in this transformation. These transformations being local, we can compute the set corresponding to a loop-free operation. For the same reason, we can compute a reduced automaton with tests from a loop-free automaton with tests.

Thus, we deduce from [5] the following lemma:

We now give the proof of Theorem 1.

The other direction of the inclusions is false. Indeed, in B ₂ (resp. B ₄), some operation that can modify node upper than the one they are applied to may be recognised (e.g. some operation starting by \(\text {copy}_{n}^{d}\overline {\text {copy}}_{n}^{d}\overline {\text {copy}}_{n}^{d^{\prime }}\)). As such an operation cannot accept a tree with a single node, it will not be shortcut by the test operation introduced in B ₁. This will not be a problem in our construction, as we simply need that by adding the test operations, we do not modify the recognised relation.

We have the following corollary as a consequence of this lemma.

Indeed A ₁ is obtained from A by adding sub-automata of the form B ₁ between two states forming the initial and final states of the form B ₂. As the lemma shows that the relation recognised by an automaton of the form B ₁ is included in the one recognised by the corresponding automaton of the form B ₂, we do not add anything to the relation recognised by A ₁. As A is furthermore included in A ₁, we get that the two automata recognise the same relation.

We construct A ₂ = (Q ^′,Γ,I ^′,F ^′,Δ^′) with Q ^′ = {q _d ,q _c ∣q ∈ Q}, I ^′ = {q _d ,q _c ∣q ∈ I}, F ^′ = {q _d ,q _c ∣q ∈ F} and

We call the destructive part the restriction A _2,d of A ₂ to Q _d and the constructive part its restriction A _2,c to Q _c . Notice that the two parts are separated by constructive operations (i.e. \(\text {copy}_{n}^{d}\) operations), thus the automaton labels all the nodes before the first \(\text {copy}_{n}^{d}\) operation with Q _d , and all the nodes after it with Q _c .

We define A ₃ = (Q ^′,Γ,I ^′,F ^′,Δ^′) with:

Observe that in this automaton, states of Q _s are sources of all stack transitions and only them, and Q _t are sources of all tree transitions and only them.

We thus construct A ₄ = (Q ^′,Γ,I ^′,F ^′,Δ^′) with

Informally, A ₄ is simply A ₃ in which we removed all stack transitions and we added between q _s and \(q^{\prime }_{t}\) the normalised automaton accepting the same relation as \(A_{q_{s},q^{\prime }_{t}}\). Figure 6 shows the idea of this transformation.

Finally, we suppose that an automaton obtained by these steps is distinguished, i.e. initial states are target of no transition and final states are source of no transition. If not, we can distinguish it by a classical transformation (as in the case of word automata). Observe that A ₅ satisfies all the requirements of Theorem 1. Thus A ₅ is a normalised automaton with tests which recognises the same relation as the initial automaton A. In subsequent constructions, we will consider the subsets of states Q _T ,Q _C ,Q _d ,Q _c as defined in steps 5 and 2, and Q _u,v = Q _u ∩ Q _v with u ∈{T,C} and v ∈{d,c}. □

With normalised automata, we can now show that the iteration of any relation defined by a ground stack tree rewriting system or a ground stack tree transducer is defined by a ground stack tree transducer.

Thus, every D _i is an operation accepted by A, and therefore D ∈Op(A) ^k .

Finally, we get \(\text {Op}(A^{\prime }) = \bigcup _{k \geq 0}\text {Op}(A)^{k}\), and thus A ^′ recognises Op(A)^∗. □

A consequence of this proposition is that the set of stack trees reachable in a GSTRS or a GSTT from a recognisable set of stack trees is recognisable.

This property is obtained by appending the automaton recognising the transitive closure of the relation defined by the GSTRS (or the GSTT) to the automaton recognising the operation producing L from a given stack tree, as in the previous proof. It is then sufficient to observe that the resulting automaton recognises the set of operations producing L ^′ from a given stack tree.

We define technical formulæ over \(\Delta _{\Gamma \times \{\varepsilon ,11,21,22\}}^{n}\) which are useful to define the set of stacks used to represent stack trees as sets of vertices of \(\Delta _{\Gamma \times \{\varepsilon ,11,21,22\}}^{n}\). To avoid long notations, in this section, we will shortcut O p s _n−1(Γ ×{ε}) by O p s _n−1(Γ).

For α,β ∈ Γ ×{ε,11,21,22}, we define \(\psi _{\text {rew}_{\alpha ,\beta }}(x,y) = x \xrightarrow {\text {rew}_{\alpha ,\beta }} y\). For every k < n, we define \(\psi _{\text {copy}_{k}}(x,y) = x \xrightarrow {\text {copy}_{k}} y\) and \(\psi _{\overline {\text {copy}}_{k}}(x,y) = y \xrightarrow {\text {copy}_{k}} x\). Finally, for k ∈{1,2} and d ≤ k, we define \(\psi _{\text {copy}_{n}^{k},d}(x,y) = \exists z_{1},z_{2}, \bigvee _{\alpha \in \Gamma } \left (x \xrightarrow {\text {rew}_{\alpha }{(\alpha ,\mathit {kd})}} z_{1} \wedge z_{1} \xrightarrow {\text {copy}_{n}} z_{2} \wedge z_{2} \xrightarrow {\text {rew}_{(\alpha ,\mathit {kd})}{\alpha }} y\right )\). Finally, for \(T_{L} \in \mathcal {T}_{n-1}\), we define \(\psi _{T_{L}}(x,y) = (x = y) \wedge \psi ^{\prime }_{L}(x)\), where \(\psi ^{\prime }_{L}(x)\) is a MSO-formula such that \(\psi ^{\prime }_{L}(x)\) holds if and only if the topmost (n − 1)-stack of x is in L. From Proposition 2.6 of [5], such a formula exists for any regular set L of (n − 1)-stacks.

For 𝜃 ∈ O p s _n−1(Γ), ψ _𝜃 (x,y) is satisfied if y is obtained by applying 𝜃 to x. \(\psi _{\text {copy}_{n}^{k},d}(x,y)\) is satisfied if y is obtained by adding kd to the topmost letter of x, then copying its topmost (n − 1)-stack, and finally removing kd of its topmost letter. \(\psi _{\overline {\text {copy}}_{n}^{k},d}(x,y)\) is satisfied if \(\psi _{\text {copy}_{n}^{k},d}(y,x)\) is satisfied. These formulæ allow us to simulate the application of a stack tree operation to a stack tree over the elements of their coding.

We now give a formula checking that a given n-stack y is obtained from an n-stack x by using only the previous formulæ,

This formula is true if for every set of n-stacks X, if x is in X and X is closed under the relations defined by ψ _𝜃 and \(\psi _{\text {copy}_{n}^{k},d}\), then y is in X.

We now define δ(X) = OnlyLeaves(X) ∧TreeDom(X) ∧UniqueLabel(X) with where α is a fixed letter of Γ.

Formula OnlyLeaves ensures that every element x in X encodes a node in some stack tree. TreeDom ensures that the prefix closure of the set of words u such that there exists a tree t such that Code(t,u) ∈ X is a tree domain, that the set of words k ₀⋯k _m−1, where for every j, k _j is the arity of the node u ₁⋯u _j of t is included in this domain, and that there is no j for which k ₁⋯k _j−1(k _j + 1) is included in this domain (in other words, that the arity announced by the k _j is respected). Finally UniqueLabel ensures that for any two elements x = Code(t,u) and y = Code(t ^′,v) of X, there exists an index j ∈{1,⋯ ,min(|u|,|v|)} such that for every i < j, u _i = v _i , t(u _i ) = t ^′(u _i ) and the node u _i has the same arity in t and t ^′, and u _j ≠v _j , i.e. for every pair of elements, the (n − 1)-stacks labelling their common ancestors are equal, and x and y cannot code the same leaf (because u≠v). Moreover, this prevents x to code a node on the path from the root to y.

Let us now explain ϕ _A (X,Y ), which can be written as We detail each of the subformulæ below: This formula is here to ensure that only leaves of X are labelled by initial states, only leaves of Y are labelled by final states and outside of their labelled leaves, X and Y are equal (i.e. not modified). where ρ _q is true if and only if q is a final state, q ∈left(K) means that q appears in the left member of K (as in the cases below), and This formula ensures that the labelling respects the rules of the automaton in the downward direction, and that for every stack s labelled by q, if there is a rule starting by q, there is a labelled stack s ^′ which is the result of s by at least one of those rules. And also that it is possible for a stack labelled by a final state to have no successor labelled by a state of the automaton (and as the automaton is distinguished, it cannot have a successor). where σ _q is true if and only if q is an initial state, q ∈right(K) means that q appears in the right member of K (as in the cases below), and This formula ensures that the labelling respects the rules of the automaton in the upward direction, and that for every stack s labelled by q, if there is a rule ending by q, there is a labelled stack s ^′ such that s is the result of s ^′ by at least one of those rules. And also that it is possible for a stack labelled by an initial state to have no predecessor labelled by a state of the automaton (and as the automaton is distinguished, it cannot have a predecessor). This formula ensures that you never use two different transitions to label stacks from a single stack labelled with a state q (in direct and reverse direction). This forces that whenever the automaton has a non-deterministic choice, it only takes one. It furthermore ensures that it is impossible to have two nodes linked by a \(\text {copy}_{n}^{2}\) or \(\overline {\text {copy}}_{n}^{2}\) transition labelled without having the third node linked with that transition labelled. This formula ensures that for any labelled stack, we can find a path of labelled stacks related by the transitions of the automaton which starts in an initial state, and another which ends in a final state.

For the sake of simplicity, let us consider for this proof that D is a unique reduced operation D (if it is a tuple of reduced operations, the proof is the same for every operation).

Init First, let us prove that Init is satisfied. From the previous lemma, all nodes of X _s are labelled with the labels of input nodes of D (or not labelled), thus they are labelled by initial states (as we considered an accepting labelling of D). Furthermore, as the automaton is distinguished, only these ones can be labelled by initial states. Similarly, the nodes of X _t , and only them are labelled by final states (or not labelled).

Trans and RTrans We show by induction on the size of the operation that Trans and RTrans are satisfied. For the sake of this proof, we will consider that ρ _q (resp. σ _q ) are replaced by predicates that are true if and only if the nodes considered are output (resp. input). As Init is satisfied, for an operation accepted by the automaton, ρ _q will only be true for output nodes and σ _q for input nodes.

Suppose now that the formulæ are true for any operation of at most n nodes. Consider D with n + 1 nodes and suppose D = D ₁⋅_1,1 D _𝜃 ⋅_1,1 D ₂. We call x the output node of D ₁ and y the input node of D ₂. We take an integer i and a stack tree t and consider the (D,i,t) labelling. By definition it is the (D ₁,i,t)(D ₂,i,t ^′) labelling with t ^′ is a stack tree such that \((t,t^{\prime }) \in r_{D_{1}}^{i} \circ r_{D_{\theta }}^{i}\). We call t ^″ a stack tree such that \((t,t^{\prime \prime }) \in r_{D_{1}}^{i}\). By definition, we thus have \((t^{\prime \prime },t^{\prime }) \in r_{D_{\theta }}^{i}\). By Lemma 11, we have s ₁ = Code(t ^″,u _i ) labelled by ρ(x) and s ₂ = Code(t ^′,u _i ) labelled by ρ(y). As furthermore, we have (s ₁,s ₂) ∈ r _𝜃 , Trans_{(ρ(x),𝜃,ρ(y))}(s ₁,s ₂,s ₂,Z) and RTrans_{(ρ(x),𝜃,ρ(y))}(s ₂,s ₁,s ₁) are true. Thus Trans and RTrans are true for the (D,i,t) labelling, as by hypothesis of induction they hold for all the nodes of the (D ₁,i,t) and (D ₂,i,t ^′) labellings, x is the only output node of D ₁ and y the only input node of D ₂.

The other cases for the decomposition of D are similar, and thus omitted. Thus, Trans and RTrans are satisfied for any (D,i,t) labelling.

WellFormed Let us now show that the labelling satisfies WellFormed. We show it by induction. We furthermore show that if a stack s is labelled by an input node x, there is no K ∈ Δ with ρ(x) ∈right(K) and no t,t ^′ such that RTrans _K (s,t,t ^′,Z), and that if a stack s is labelled by an output node x, there is no K ∈ Δ with ρ(x) ∈left(K) and no t,t ^′ such that Trans _K (s,t,t ^′,Z).

If D = □ or \(D = D_{T_{L}}\), the result is immediate.

Suppose that \(D = (D_{1} \cdot _{1,1} (D_{\text {copy}_{n}^{2}} \cdot _{2,1} D_{3})) \cdot _{1,1} D_{2}\). By induction, WellFormed holds for the (D ₁,i,t), (D ₂,i,t ^′) and (D ₃,i + 1,t ^′) labellings with \((t,t^{\prime }) \in r_{D_{1}}^{i} \circ r_{\text {copy}_{n}^{2}}^{i}\), and we consider t ^″ such that \((t^{\prime \prime },t^{\prime }) \in r_{\text {copy}_{n}^{2}}^{i}\). We call x the only output node of D ₁, y and z the only input nodes of D ₂ and D ₃, s ₁ = Code(t ^″,u _i ), s ₂ = Code(t ^′,u _i ) and s ₃ = Code(t ^′,u _i+1). First, observe that we have Trans_{(ρ(x),(ρ(y),ρ(z)))}(s ₁,s ₂,s ₃,Z), RTrans_{(ρ(x),(ρ(y),ρ(z))}(s ₂,s ₁,s ₁,Z) and RTrans_{(ρ(x),(ρ(y),ρ(z))}(s ₃,s ₁,s ₁,Z), by definition of the labelling. By hypothesis of induction, there are no stacks s,s ^′ and no transition K with ρ(x) ∈left(K) (resp. ρ(y) ∈right(K), ρ(z) ∈right(K)) such that Trans _K (s ₁,s,s ^′,Z) (resp. RTrans _K (s ₂,s,s ^′,Z), RTrans _K (s ₃,s,s ^′)) holds in the (D ₁,i,t) labelling (resp. the (D ₂,i,t ^′) or (D ₃,i + 1,t ^′) labellings). Suppose there are stacks s,s ^′,s ^″ labelled in the (D,i,t) labelling such that Trans _K (s,s ^′,s ^″,Z) holds, such that s,s ^′,s ^″ are not all labelled in the same D _i . As A is normalised, all stacks labelled in D ₂ and D ₃ are labelled with states of Q _c , and have at least 1 (n − 1)-stack more than stack labelled with states of Q _c in D ₁. Moreover, as s ₂ is obtained as the left copy of s ₁ and s ₂ as the right copy of s ₁, it is not possible to produce stacks labelled in D ₂ from stacks labelled in D ₃ without producing first s ₁ (and vice-versa), and as A is normalised, this is impossible. Thus, if all three s,s ^′,s ^″ are labelled in Q _c , then s is labelled in D ₁ and K is a \(\text {copy}_{n}^{d}\) transition. If s is labelled in Q _d , then the only possibility for K is also to be a \(\text {copy}_{n}^{d}\) transition. Suppose it is a \(\text {copy}_{n}^{1}\) transition, then s ^′ = s ^″. Suppose s ^′ is labelled in D ₂ (the case for D ₃ being symmetric). It is thus obtained from s by a \(\text {copy}_{n}^{1}\) operation. But it is also obtained from s ₂ which has more (n − 1)-stacks than s and is obtained from s ₁ as the left copy of a \(\text {copy}_{n}^{2}\). Thus s ₂ have at least as many (n − 1)-stacks as s ^′, and to obtain s ^′ from s ₂ we must first annul that binary copy with a \(\overline {\text {copy}}_{n}^{2}\), which is impossible as A is normalised. Thus we have K is a \(\text {copy}_{n}^{2}\) transition, s is labelled in D ₁, s ^′ in D ₂ and s ^″ in D ₃. They are thus 𝜃 ₁, 𝜃 ₂, 𝜃 ₃ such that \((s,s_{1}) \in r_{\theta _{1}}\), \((s_{2},s^{\prime }) \in r_{\theta _{2}}\) and \((s_{3},s^{\prime \prime }) \in r_{\theta _{3}}\). Thus we have \(D_{\theta _{1}} \cdot _{1,1} ((D_{\text {copy}_{n}^{2}} \cdot _{2,1} D_{\theta _{3}}) \cdot _{1,1} D_{\theta _{2}})\) equivalent to \(D_{\text {copy}_{n}^{2}}\). Thus as A is normalised, 𝜃 ₁, 𝜃 ₂ and 𝜃 ₃ can only be single tests or empty operations, but as there are no state that can be at the left (resp. right) of both a test and a non-test transition, we get that 𝜃 ₁, 𝜃 ₂ and 𝜃 ₃ are empty operation, and thus that s = s ₁, s ^′ = s ₂, s ^″ = s ₃ and K = (ρ(x),(ρ(y),ρ(z))). Similarly, if RTrans _K (s,s ^′,s ^″) for s,s ^′,s ^″ not labelled in the same DAG, then K = (ρ(x),(ρ(y),ρ(z))) and s = s ₂ or s = s ₃ and s ^′ = s ^″ = s ₁. Observe as well that as we added a full transition, we did not add any x,y such that there is a K with RTrans _K (x,y,y,Z) but no z such that Trans _K (y,z,x) or Trans _K (y,x,z) (or the converse). Thus WellFormed holds for the (D,i,t) labelling. Finally, as input nodes of D were input nodes of D ₁ (resp. output nodes of D were output nodes of D ₂ and D ₃), and we did not add them any incoming edge (resp. output edge), the same reasoning apply to show there is no RTrans _K (resp. Trans _K )) true with them as first variable, and thus the induction hypothesis holds.

For \(D = D_{2} \cdot _{1,2}(D_{1} \cdot _{1,1} D_{\overline {\text {copy}}_{n}^{2}}))\cdot _{1,1} D_{3}\), the case is similar (by exchanging roles of \(\text {copy}_{n}^{d}\) and \(\overline {\text {copy}}_{n}^{d}\) and so on).

Suppose that D = D ₁⋅_1,1 D _𝜃 ⋅_1,1 D ₂, and call x the output node of D ₁ and y the input node of D ₂. We take t ^″ such that \((t,t^{\prime \prime }) \in r_{D_{1}}^{i}\) and t ^′ such that \((t^{\prime \prime },t^{\prime }) \in r_{\theta }^{i}\), and call s ₁ = Code(t ^″,u _i ) and s ₂ = Code(t ^′,u _i ). By definition of the labelling, Trans_{(ρ(x),𝜃,ρ(y))}(s ₁,s ₂,s ₂,Z) and RTrans_{(ρ(x),𝜃,ρ(y))}(s ₂,s ₁,s ₁,Z) hold. By hypothesis of induction, WellFormed holds for the (D ₁,i,t) and (D ₂,i,t ^′) labellings, and there are no K, and no s,s ^′ labelled in the (D ₁,i,t) labelling (resp. the (D ₂,i,t ^′) labelling) such that Trans _K (s ₁,s,s ^′,Z) holds (resp. RTrans _K (s ₂,s,s ^′,Z)). Suppose there are stacks s,s ^′,s ^″ labelled in the (D,i,t) labelling such that Trans _K (s,s ^′,s ^″,Z) holds and s,s ^′,s ^″ are not all labelled in the same D _i . Suppose that s is labelled by z ₂ in D ₂ and s ^′ by z ₁ in D ₁. Then, there is a path from z ₁ to z ₂ labelled by w which contains 𝜃. But as from ρ(z ₂) it is possible to take K, it is thus possible to label a DAG containing w followed by K, which is a non-single test word that can leave s ^′ unchanged. As A is normalised, this is impossible. Thus, s is labelled by z ₁ in D ₁ and s ^′,s ^″ by z ₂ and z ₃ in D ₂. Call 𝜃 ^′ the operation of K. There is a path from z ₁ to z ₂ labelled by an operation w that contains 𝜃, and such that \(r_{w} = r_{\theta ^{\prime }}\). We thus have w = w ₁ ⋅ 𝜃 ⋅ w ₂ for some operation words w ₁,w ₂. Suppose 𝜃 ^′ is a \(\text {copy}_{n}^{d}\) operation. Then s ^′ has exactly one (n − 1)-stack more than s and their topmost are equal. As 𝜃 is a non-test and non-tree operation, it must be inverted in w to get s ^′ from s. Thus w contains a non-single test operation containing the identity, which is impossible as A is normalised. If 𝜃 ^′ is a \(\overline {\text {copy}}_{n}^{d}\) operation we get a similar contradiction. Thus 𝜃 ^′ is a stack operation. Suppose w contains tree operations. As A is normalised, you only can have \(\overline {\text {copy}}_{n}^{d}\) followed by the same number of \(\text {copy}_{n}^{d}\), as 𝜃 ^′ does not modify the number of (n − 1)-stacks. Thus ρ(z ₁) is in Q _d and ρ(z ₂) is in Q _c . But the only transition between Q _d and Q _c are labelled with \(\text {copy}_{n}^{d}\) operations, so this is impossible. Thus w does not contain any tree operation and is thus in Red (as A is normalised). If 𝜃≠𝜃 ^′ and 𝜃 =copy _i (resp. \(\overline {\text {copy}}_{j}\)) or 𝜃 ^′ =copy _j (resp. \(\overline {\text {copy}}_{j}\)), we get a similar contradiction than for the \(\text {copy}_{n}^{d}\) case. If 𝜃 = 𝜃 ^′ =copy _i , similarly to the above case for D, we get that w ₁ and w ₂ can only be empty operations, thus z ₁ = x, z ₂ = y, and K = (ρ(x),𝜃,ρ(y)). Suppose 𝜃 =rew _α,β and 𝜃 ^′ =rew _γ δ. As w is in Red, it cannot contain non-single test factors containing the identity, thus it only contains tests and \(\text {rew}_{\alpha ^{\prime }}{\beta ^{\prime }}\) operations. But in a word of Red, there cannot be two \(\text {rew}_{\alpha ^{\prime }}{\beta ^{\prime }}\) operations not separated by a copy _i or a \(\overline {\text {copy}}_{i}\). Moreover as no state can be at the left of the right of both a test and a non-test transition, we get that w =rew _α,β and is equivalent to rew _γ δ. Thus z ₁ = x, z ₂ = y, and K = (ρ(x),𝜃,ρ(y)). Thus in every case, we have that if Trans _K (s,s ^′,s ^″) with s,s ^′,s ^″ labelled in different D _i , s = s ₁, s ^′ = s ^″ = s ₂ and K = (ρ(x),𝜃,ρ(y)). Similarly, if RTrans _K (s,s ^′,s ^″) with s,s ^′,s ^″ labelled in different D _i , we get s = s ₂, s ^′ = s ^″ = s ₁ and K = (ρ(x),𝜃,ρ(y)). Observe as well that as we added a full transition, we did not add any x,y such that there is a K with RTrans _K (x,y,y,Z) but no z such that Trans _K (y,z,x) or Trans _K (y,x,z) (or the converse). Thus WellFormed holds for the (D,i,t) labelling. Finally, as input nodes of D were input nodes of D ₁ (resp. output nodes of D were output nodes of D ₂ and D ₃), and we did not add them any incoming edge (resp. output edge), the same reasoning apply to show there is no RTrans _K (resp. Trans _K )) true with them as first variable, and thus the induction hypothesis holds.

Thus WellFormed holds for the (D,i,t) labelling.

NoCycle Finally, let us show that the labelling satisfies NoCycle. Take s a stack labelled in the (D,i,t) labelling of S t a c k s _n−1 with the label of a node x. We show by induction on the size of D that there exists a path of stacks related by basic operations from a stack s ^′ labelled with a state labelling an input node of D to s and a path of stacks related by basic operations from s to a stack s ^″ labelled with a state labelling an output node of D.

Suppose D = D ₁⋅_1,1 D _𝜃 ⋅_1,1 D ₂, and x is a node of D ₁ (the case x is a node of D ₂ is symmetric and thus omitted). By hypothesis of induction, there exists s ^′ labelled by an input node of D ₁ such that there is a path from s ^′ to s, and s ^″ labelled by the only output node of D ₁ such that there is a path from s to s ^″. By hypothesis of induction, for s ₁ labelled by the only input node of D ₂, there exists s ₂ labelled by an output node of D ₂ such that there is a path from s ₁ to s ₂. Furthermore, by definition of the labelling, we have (s ^″,s ₁) ∈ r _𝜃 , and thus, there is a path from s to s ₂.

Thus, as all its sub-formulæ are true, \(\phi _{A}^{\prime }(X_{s},X_{t},\mathbf {Z})\) is true with the described labelling Z. And thus ϕ _A (X _s ,X _t ) is true. □

Suppose now that ϕ _A (X _s ,X _t ) is satisfied. We take a labelling Z that satisfies the formula \(\phi _{A}^{\prime }(X_{s},X_{t},\mathbf {Z})\), minimal in the number of nodes labelled. We construct the following graph D:

We recall that a well-formed DAG is a DAG where for every nodes x,y, if there is an edge between x and y, then the subDAG obtained by restricting the DAG to x, y, the successors of x and the predecessors of y is a DAG representing a basic operation.

Thus, every D _i is a well-formed DAG accepted by A. From Lemma 7, we get that D _i is an operation.

We have proved both directions: for every n-stack trees s and t, there exists a tuple of operations D recognised by A and a tuple of positions i such that \((s,t)\in r_{\mathbf {D}}^{\mathbf {i}}\) if and only if ϕ _A (X _s ,X _t ). □

Given two stack trees s,t, the formula ψ _A (X _s ,X _t ) holds if there exists an operation D recognised by A such that (s,t) ∈ r _D . Thus, it differs from ϕ _A only by the fact that D is a unique operation, as ϕ _A (X _s ,X _t ) holds if there exists a tuple of operations D recognised by A such that (s,t) ∈ r _D . The formula is defined as follows:

Informally, this formula states that between any two nodes labelled, one can find a path of labelled nodes related by transitions of the automaton.

Suppose now that ψ _A (X _s ,X _t ) holds. As previously, we construct the graph D from a minimal labelling satisfying the formula. Lemmas 12, 13 and 14 hold. It is sufficient to modify the proof of Lemma 12 to show that D is furthermore a connected DAG. We chose the vertices (x,q) and (y,q ^′) in D. By definition of D, we have x ∈ Z _q and \(y \in Z_{q^{\prime }}\). As Connected(Z) holds, there is a sequence x = x ₁,x ₂,⋯ ,x _k = y such that for any i, x _i is labelled with a state q _i , with q ₁ = q and q _k = q ^′, and there is a transition K and a node z _i such that Trans _K (x _i ,x _i+1,z _i ,Z) or RTrans _K (x _i ,x _i+1,z _i ,Z) holds. In the first case, by construction of D, we have an edge (x _i ,𝜃,x _i+1) (or (x _i ,1,x _i+1) or other similar cases depending on the transition K), and in the second case we have an edge (x _i+1,𝜃,x _i ). Thus, there is an undirected path between (x,q) and (x,q ^′). Therefore D is a connected DAG. □

The three formulæ defined in this section allow to define the finite set interpretations announced at the beginning of the section, which proves Theorem 2.