Bounded Automata Groups are co-ET0L

Abstract

Holt and Röver proved that finitely generated bounded automata groups have indexed co-word problem. Here we sharpen this result to show they are in fact co-ET0L.

Research supported by Australian Research Council grant DP160100486 and an Australian Government Research Training Program PhD Scholarship.

1 Introduction

A recurrent theme in group theory is to understand and classify group-theoretic problems in terms of their formal language complexity [1, 9,10,11, 20]. Many authors have considered the groups whose non-trivial elements, i.e. co-word problem, can be described as a context-free language [3, 14, 16, 18]. Holt and Röver went beyond context-free to show that a large class known as bounded automata groups have an indexed co-word problem [15]. This class includes important examples such as Grigorchuk’s group of intermediate growth, the Gupta-Sidki groups, and many more [12, 13, 21, 24]. For the specific case of the Grigorchuk group, Ciobanu et al. [5] showed that the co-word problem was in fact ET0L. ET0L is a class of languages coming from L-systems which lies strictly between context-free and indexed [19, 22, 23]. Ciobanu et al. rely on the grammar description of ET0L for their result. Here we are able to show that all finitely generated bounded automata groups have ET0L co-word problem by instead making use of an equivalent machine description: check-stack pushdown (cspd) automata.

ET0L languages, in particular their deterministic versions, have recently come to prominence in describing solution sets to equations in groups and monoids [4, 7, 8]. The present paper builds on the recent resurgence of interest, and demonstrates the usefulness of a previously overlooked machine description.

For a group G with finite generating set X, we denote by $\mathrm {coW}(G,X)$ the set of all words in the language $(X \cup X^{-1})^\star$ that represent non-trivial elements in G. We call $\mathrm {coW}(G,X)$ the co-word problem for G (with respect to X). Given a class $\mathcal {C}$ of formal languages that is closed under inverse homomorphism, if $\mathrm {coW}(G,X)$ is in $\mathcal {C}$ then so is $\mathrm {coW}(G,Y)$ for any finite generating set Y of G [14]. Thus, we say that a group is co-$\mathcal {C}$ if it has a co-word problem in the class $\mathcal {C}$. Note that ET0L is a full AFL [6] and so is closed under inverse homomorphism.

2 ET0L Languages and CSPD Automata

An alphabet is a finite set. Let $\varSigma$ and V be two alphabets which we will call the terminals and non-terminals, respectively. We will use lower case letters to represent terminals in $\varSigma$ and upper case letters for non-terminals in V. By $\varSigma ^\star$, we will denote the set of words over $\varSigma$ with $\varepsilon \in \varSigma ^\star$ denoting the empty word.

A table, $\tau$, is a finite set of context-free replacement rules where each non-terminal, $X \in V$, has at least one replacement in $\tau$. For example, with $\varSigma = \{a,b\}$ and $V = \{S,A,B\}$, the following are tables.

$$\begin{aligned} \alpha \, : \, \left\{ \begin{aligned} S&\rightarrow SS \ \vert \ S \ \vert \ AB\\ A&\rightarrow A\\ B&\rightarrow B \end{aligned} \right. \qquad \beta \, : \, \left\{ \begin{aligned} S&\rightarrow S\\ A&\rightarrow aA\\ B&\rightarrow bB \end{aligned} \right. \qquad \gamma \, : \, \left\{ \begin{aligned} S&\rightarrow S \\ A&\rightarrow \varepsilon \\ B&\rightarrow \varepsilon \end{aligned} \right. \end{aligned}$$

(1)

We apply a table, $\tau$, to the word $w \in (\varSigma \cup V)^\star$ to obtain a word $w'$, written $w \rightarrow ^\tau w'$, by performing a replacement in $\tau$ to each non-terminal in w. If a table includes more than one rule for some non-terminal, we nondeterministically apply any such rule to each occurrence. For example, with $w = SSSS$ and $\alpha$ as in (1), we can apply $\alpha$ to w to obtain $w' = SABSSAB$. Given a sequence of tables $\tau _1$, $\tau _2$, ..., $\tau _k$, we will write $w \rightarrow ^{\tau _1 \tau _2 \cdots \tau _k} w'$ if there is a sequence of words $w = w_1$, $w_2$, ..., $w_{k+1} = w'$ such that $w_{j} \rightarrow ^{\tau _j} w_{j+1}$ for each j.

Definition 1

(Asveld [2]). An ET0L grammar is a 5-tuple $G = (\varSigma , V, T, \mathcal {R}, S)$, where

• 1. $\varSigma$ and V are the alphabets of terminals and non-terminals, respectively;

• 2. $T = \{\tau _1, \tau _2 ,\dots , \tau _k\}$ is a finite set of tables;

• 3. $\mathcal {R} \subseteq T^\star$ is a regular language called the rational control; and

• 4. $S \in V$ is the start symbol.

The ET0L language produced by the grammar G, denoted L(G), is

$$\begin{aligned} L(G) := \left\{ w \in \varSigma ^\star \, :\, S \rightarrow ^{v} w \ \ \text {for some} \ \ v \in \mathcal {R} \right\} . \end{aligned}$$

For example, with $\alpha$, $\beta$ and $\gamma$ as in (1), the language produced by the above grammar with rational control $\mathcal {R} = \alpha ^\star \beta ^\star \gamma$ is $\{ ( a^n b^n )^m \, : \, n,m \in \mathbb {N}\}$.

2.1 CSPD Automata

A cspd automaton, introduced in [17], is a nondeterministic finite-state automaton with a one-way input tape, and access to both a check-stack (with stack alphabet $\varDelta$) and a pushdown stack (with stack alphabet $\varGamma$), where access to these two stacks is tied in a very particular way. The execution of a cspd machine can be separated into two stages.

In the first stage the machine is allowed to push to its check-stack but not its pushdown, and further, the machine will not be allowed to read from its input tape. Thus, the set of all possible check-stacks that can be constructed in this stage forms a regular language which we will denote as $\mathcal {R}$.

In the second stage, the machine can no longer alter its check-stack, but is allowed to access its pushdown and input tape. We restrict the machine’s access to its stacks so that it can only move along its check-stack by pushing and popping items to and from its pushdown. In particular, every time the machine pushes a value onto the pushdown it will move up the check-stack, and every time it pops a value off of the pushdown it will move down the check-stack; see Fig. 1 for an example of this behaviour.

Fig. 1.

An example of a cspd machine pushing $w = a_1 a_2$, where $a_1,a_2 \in \varDelta$, onto its pushdown stack, then popping $a_1$

We define a cspd machine formally as follows.

Definition 2

A cspd machine is a 9-tuple $\mathcal {M} = (Q, \varSigma , \varGamma , \varDelta , \mathfrak b, \mathcal {R}, \theta , q_0, F)$, where

• 1. Q is the set of states;

• 2. $\varSigma$ is the input alphabet;

• 3. $\varGamma$ is the alphabet for the pushdown;

• 4. $\varDelta$ is the alphabet for the check-stack;

• 5. $\mathfrak b \notin \varDelta \cup \varGamma$ is the bottom of stack symbol;

• 6. $\mathcal {R} \subseteq \varDelta ^\star$ is a regular language of allowed check-stack contents;

• 7. $\theta$ is a finite subset of

  $$ ( Q \times ( \varSigma \cup \{\varepsilon \} ) \times ( (\varDelta \times \varGamma ) \cup \{ (\varepsilon ,\varepsilon ), (\mathfrak {b},\mathfrak {b}) \} ) ) \times (Q \times ( \varGamma \cup \{\mathfrak {b}\})^\star ), $$

  and is called the transition relation (see below for allowable elements of $\theta$);

• 8. $q_0 \in Q$ is the start state; and

• 9. $F \subseteq Q$ is the set of accepting states.

In its initial configuration, the machine will be in state $q_0$, the check-stack will contain $\mathfrak {b}w$ for some nondeterministic choice of $w \in \mathcal {R}$, the pushdown will contain only the letter $\mathfrak {b}$, the read-head for the input tape will be at its first letter, and the read-head for the machine’s stacks will be pointing to the $\mathfrak {b}$ on both stacks. From here, the machine will follow transitions as specified by $\theta$, each such transition having one of the following three forms, where $a\in \varSigma \cup \{\varepsilon \}$, $p,q\in Q$ and $w \in \varGamma ^\star$.

• 1. $((p,a,(\mathfrak {b},\mathfrak {b})),(q, w\mathfrak {b})) \in \theta$ meaning that if the machine is in state p, sees $\mathfrak {b}$ on both stacks and is able to consume a from its input; then it can follow this transition to consume a, push w onto the pushdown and move to state q.

• 2. $((p,a,(d,g)),(q,w)) \in \theta$ where $(d,g) \in \varDelta \times \varGamma$, meaning that if the machine is in state p, sees d on its check-stack, g on its pushdown, and is able to consume a from its input; then it can follow this transition to consume a, pop g, then push w and move to state q.

• 3. $((p,a,(\varepsilon ,\varepsilon )),(q,w)) \in \theta$ meaning that if the machine is in state p and can consume a from its input; then it can follow this transition to consume a, push w and move to state q.

In the previous three cases, $a = \varepsilon$ corresponds to a transition in which the machine does not consume a letter from input. We use the convention that, if $w = w_1 w_2 \cdots w_k$ with each $w_j \in \varGamma$, then the machine will first push the $w_k$, followed by the $w_{k-1}$ and so forth. The machine accepts if it has consumed all its input and is in an accepting state $q \in F$.

In [17] van Leeuwen proved that the class of languages that are recognisable by cspd automata is precisely the class of ET0L languages.

3 Bounded Automata Groups

For $d \geqslant 2$, let $\mathcal {T}_d$ denote the d-regular rooted tree, that is, the infinite rooted tree where each vertex has exactly d children. We identify the vertices of $\mathcal {T}_d$ with words in $\varSigma ^\star$ where $\varSigma = \{ a_1, a_2, \ldots , a_d \}$. In particular, we will identify the root with the empty word $\varepsilon \in \varSigma ^\star$ and, for each vertex $v \in \mathrm {V}(\mathcal {T}_d)$, we will identify the k-th child of v with the word $v a_k$, see Fig. 2.

Fig. 2.

A labelling of the vertices of $\mathcal {T}_d$ with the root labelled $\varepsilon$

Recall that an automorphism of a graph is a bijective mapping of the vertex set that preserves adjacencies. Thus, an automorphism of $\mathcal {T}_d$ preserves the root and “levels” of the tree. The set of all automorphisms of $\mathcal {T}_d$ is a group, which we denote by $\mathrm {Aut}(\mathcal {T}_d)$. We denote the permutation group of $\varSigma$ as $\mathrm {Sym}(\varSigma )$. An important observation is that $\mathrm {Aut}(\mathcal {T}_d)$ can be seen as the wreath product $\mathrm {Aut}(\mathcal {T}_d) \wr \mathrm {Sym}(\varSigma )$, since any automorphism $\alpha \in \mathrm {Aut}(\mathcal {T}_d)$ can be written uniquely as $\alpha = (\alpha _1, \alpha _2, \ldots , \alpha _d) \cdot \sigma$ where $\alpha _i \in \mathrm {Aut}(\mathcal {T}_d)$ is an automorphism of the sub-tree with root $a_i$, and $\sigma \in \mathrm {Sym}(\varSigma )$ is a permutation of the first level. Let $\alpha \in \mathrm {Aut}(\mathcal {T}_d)$ where $\alpha = (\alpha _1, \alpha _2, \ldots , \alpha _d) \cdot \sigma \in \mathrm {Aut}(\mathcal {T}_d) \wr \mathrm {Sym}(\varSigma )$. For any $b = a_i \in \varSigma$, the restriction of $\alpha$ to b, denoted $\left. \alpha \right| _b := \alpha _i$, is the action of $\alpha$ on the sub-tree with root b. Given any vertex $w = w_1 w_2 \cdots w_k \in \varSigma ^\star$ of $\mathcal {T}_d$, we can define the restriction of $\alpha$ to w recursively as

$$ \left. \alpha \right| _w = \left. \left( \left. \alpha \right| _{w_1w_2\cdots w_{k-1}}\right) \right| _{w_k} $$

and thus describe the action of $\alpha$ on the sub-tree with root w.

A $\varSigma$-automaton, $(\varGamma ,v)$, is a finite directed graph with a distinguished vertex v, called the initial state, and a $(\varSigma \times \varSigma )$-labelling of its edges, such that each vertex has exactly $\left| \varSigma \right|$ outgoing edges: with one outgoing edge with a label of the form $(a, \cdot )$ and one with a label of the form $( \cdot , a)$ for each $a \in \varSigma$.

Given some $\varSigma$-automaton $(\varGamma ,v)$, where $\varSigma = \{a_1,\ldots ,a_d\}$, we can define an automorphism $\alpha _{(\varGamma ,v)} \in \mathrm {Aut}(\mathcal {T}_d)$ as follows. For any given vertex $b_1 b_2 \cdots b_k \in \varSigma ^\star = \mathrm {V}\!\left( \mathcal {T}_d\right)$, there exists a unique path in $\varGamma$ starting from the initial vertex, v, of the form $(b_1, b_1') \, (b_2, b_2') \, \cdots \, (b_k, b_k')$, thus we will now define $\alpha _{(\varGamma ,v)}$ such that $\alpha _{(\varGamma ,v)} (b_1 b_2 \cdots b_k) = b_1' b_2' \cdots b_k'$. Notice that it follows from the definition of a $\varSigma$-automaton that $\alpha _{(\varGamma ,v)}$ is a tree automorphism as required.

An automaton automorphism, $\alpha$, of the tree $\mathcal {T}_d$ is an automorphism for which there exists a $\varSigma$-automaton, $(\varGamma ,v)$, such that $\alpha = \alpha _{(\varGamma ,v)}$. The set of all automaton automorphisms of the tree $\mathcal {T}_d$ form a group which we will denote as $\mathcal {A}\!\left( \mathcal {T}_d\right)$. A subgroup of $\mathcal {A}(\mathcal {T}_d)$ is called an automata group.

An automorphism $\alpha \in \mathrm {Aut}(\mathcal {T}_d)$ will be called bounded (originally defined in [24]) if there exists a constant $N \in \mathbb {N}$ such that for each $k\in \mathbb {N}$, there are no more than N vertices $v\in \varSigma ^\star$ with $\left| v \right| = k$ (i.e. at level k) such that $\left. \alpha \right| _v \ne 1$. Thus, the action of such a bounded automorphism will, on each level, be trivial on all but (up to) N sub-trees. The set of all such automorphisms form a group which we will denote as $\mathcal {B}(\mathcal {T}_d)$. The group of all bounded automaton automorphisms is defined as the intersection $\mathcal {A}(\mathcal {T}_d) \cap \mathcal {B}(\mathcal {T}_d)$, which we will denote as $\mathcal {D}(\mathcal {T}_d)$. A subgroup of $\mathcal {D}(\mathcal {T}_d)$ is called a bounded automata group.

A finitary automorphism of $\mathcal {T}_d$ is an automorphism $\phi$ such that there exists a constant $k \in \mathbb {N}$ for which $\left. \phi \right| _v = 1$ for each $v \in \varSigma ^\star$ with $\left| v \right| = k$. Thus, a finitary automorphism is one that is trivial after some k levels of the tree. Given a finitary automorphism $\phi$, the smallest k for which this definition holds will be called its depth and will be denoted as $\mathrm {depth}(\phi )$. We will denote the group formed by all finitary automorphisms of $\mathcal {T}_d$ as $\mathrm {Fin}(\mathcal {T}_d)$. See Fig. 3 for examples of the actions of finitary automorphisms on their associated trees (where any unspecified sub-tree is fixed by the action).

Fig. 3.

Examples of finitary automorphisms $a,b\in \mathrm {Fin}\!\left( \mathcal {T}_2\right)$

Let $\delta \in \mathcal {A}\!\left( \mathcal {T}_d\right) \setminus \mathrm {Fin}\!\left( \mathcal {T}_d\right)$. We call $\delta$ a directed automaton automorphism if

$$\begin{aligned} \delta = (\phi _1, \phi _2, \ldots , \phi _{k-1}, \delta ', \phi _{k+1}, \ldots , \phi _d) \cdot \sigma \in \mathrm {Aut}\!\left( \mathcal {T}_d\right) \wr \mathrm {Sym}(\varSigma ) \end{aligned}$$

(2)

where each $\phi _j$ is finitary and $\delta '$ is also directed automaton (that is, not finitary and can also be written in this form). We call $\mathrm {dir}(\delta ) = b = a_k \in \varSigma$, where $\delta '=\delta \vert _{b}$ is directed automaton, the direction of $\delta$; and we define the spine of $\delta$, denoted $\mathrm {spine}(\delta ) \in \varSigma ^\omega$, recursively such that $\mathrm {spine}(\delta ) = \mathrm {dir}(\delta ) \, \mathrm {spine}(\delta ')$. We will denote the set of all directed automaton automorphisms as $\mathrm {Dir}(\mathcal {T}_d)$. See Fig. 4 for examples of directed automaton automorphisms (in which a and b are the finitary automorphisms in Fig. 3).

Fig. 4.

Examples of directed automata automorphisms $x,y,z \in \mathrm {Dir}(\mathcal {T}_2)$

The following lemma is essential to prove our main theorem.

Lemma 3

The spine, $\mathrm {spine}(\delta ) \in \varSigma ^\omega$, of a directed automaton automorphism, $\delta \in \mathrm {Dir}(\mathcal {T}_d)$, is eventually periodic, that is, there exists some $\iota = \iota _1 \iota _2 \cdots \iota _s \in \varSigma ^\star$, called the initial section, and $\pi = \pi _1 \pi _2 \cdots \pi _t \in \varSigma ^\star$, called the periodic section, such that $\mathrm {spine}(\delta ) = \iota \, \pi ^\omega$; and

$$\begin{aligned} \left. \delta \right| _{\iota \, \pi ^k \, \pi _1 \pi _2 \cdots \pi _j} = \left. \delta \right| _{\iota \, \pi _1 \pi _2 \cdots \pi _j} \end{aligned}$$

(3)

for each $k,j \in \mathbb {N}$ with $0\leqslant j <t$.

Proof

Let $(\varGamma ,v)$ be a $\varSigma$-automaton such that $\delta = \alpha _{(\varGamma ,v)}$. By the definition of $\varSigma$-automata, for any given vertex $w = w_1 w_2 \cdots w_k \in \varSigma ^\star$ of $\mathcal {T}_d$ there exists a vertex $v_w \in \mathrm {V}(\varGamma )$ such that $\delta \vert _w = \alpha _{(\varGamma ,v_w)}$. In particular, such a vertex $v_w$ can be obtained by following the path with edges labelled $(w_1, w_1') (w_2, w_2') \cdots (w_k, w_k')$. Then, since there are only finitely many vertices in $\varGamma$, the set of all restrictions of $\delta$ is finite, that is,

$$\begin{aligned} \left| \left\{ \left. \delta \right| _w = \alpha _{(\varGamma ,v_w)} \, : \, w \in \varSigma ^\star \right\} \right| < \infty . \end{aligned}$$

(4)

Let $b = b_1 b_2 b_3 \cdots = \mathrm {spine}(\delta ) \in \varSigma ^\omega$ denote the spine of $\delta$. Then, there exists some $n,m \in \mathbb {N}$ with $n < m$ such that

$$\begin{aligned} \delta \vert _{b_1 b_2 \cdots b_n} = \delta \vert _{b_1 b_2 \cdots b_n \cdots b_{m}} \end{aligned}$$

(5)

as otherwise there would be infinitely many distinct restrictions of the form $\delta \vert _{b_1 b_2 \cdots b_k}$ thus contradicting (4). By the definition spine, it follows that

$$ \mathrm {spine} \left( \delta \vert _{b_1 b_2 \cdots b_n} \right) = (b_{n+1}b_{n+2} \cdots b_m) \ \mathrm {spine} \left( \delta \vert _{b_1 b_2 \cdots b_n \cdots b_{m}} \right) . $$

and hence, by (5),

$$ \mathrm {spine} \left( \delta \vert _{b_1 b_2 \cdots b_n} \right) = (b_{n+1}b_{n+2} \cdots b_m)^\omega . $$

Thus,

$$ \mathrm {spine}(\delta ) = (b_1 b_2 \cdots b_n) \ \mathrm {spine} \left( \delta \vert _{b_1 b_2 \cdots b_n} \right) = (b_1 b_2 \cdots b_n) \ (b_{n+1}b_{n+2} \cdots b_m)^\omega . $$

Then, by taking $\iota = b_1 b_2 \cdots b_n$ and $\pi = b_{n+1} b_{n+2} \cdots b_m$, we have $\mathrm {spine}(\delta ) = \iota \,\pi ^\omega$. Moreover, from (5), we have Eq. (3) as required.    $\square$

Notice that each finitary and directed automata automorphism is also bounded, in fact, we have the following proposition which shows that the generators of any given bounded automata group can be written as words in $\mathrm {Fin}\!\left( \mathcal {T}_d\right)$ and $\mathrm {Dir}\!\left( \mathcal {T}_d\right)$.

Proposition 4

(Proposition 16 in [24]). The group $\mathcal {D}\!\left( \mathcal {T}_d\right)$ of bounded automata automorphisms is generated by $\mathrm {Fin}\!\left( \mathcal {T}_d\right)$ together with $\mathrm {Dir}\!\left( \mathcal {T}_d\right)$.

4 Main Theorem

Theorem 5

Every finitely generated bounded automata group is co-ET0L.

The idea of the proof is straightforward: we construct a cspd machine that chooses a vertex $v \in \mathrm {V}(\mathcal {T}_d)$, writing its label on the check-stack and a copy on its pushdown; as it reads letters from input, it uses the pushdown to keep track of where the chosen vertex is moved; and finally it checks that the pushdown and check-stack differ. The full details are as follows.

Proof

Let $G \subseteq \mathcal {D}(\mathcal {T}_d)$ be a bounded automata group with finite symmetric generating set X. By Proposition 4, we can define a map

$$ \varphi : X \rightarrow \left( \mathrm {Fin}(\mathcal {T}_d) \cup \mathrm {Dir}(\mathcal {T}_d) \right) ^\star $$

so that $x =_{\mathcal {D}(\mathcal {T}_d)} \varphi (x)$ for each $x \in X$. Let

$$ Y = \left\{ \alpha \in \mathrm {Fin}(\mathcal {T}_d) \cup \mathrm {Dir}(\mathcal {T}_d) \,:\, \alpha \text { or } \alpha ^{-1} \text { is a factor of } \varphi (x) \text { for some } x \in X \right\} $$

which is finite and symmetric. Consider the group $H \subseteq \mathcal {D}(\mathcal {T}_d)$ generated by Y. Since ET0L is closed under inverse word homomorphism, it suffices to prove that $\mathrm {coW}(H,Y)$ is ET0L, as $\mathrm {coW}(G,X)$ is its inverse image under the mapping $X^\star \rightarrow Y^\star$ induced by $\varphi$. We construct a cspd machine $\mathcal {M}$ that recognises $\mathrm {coW}(H,Y)$, thus proving that G is co-ET0L.

Let $\alpha = \alpha _1 \alpha _2 \cdots \alpha _n \in Y^\star$ denote an input word given to $\mathcal {M}$. The execution of the cspd will be separated into four stages; (1) choosing a vertex $v \in \varSigma ^\star$ of $\mathcal {T}_d$ which witnesses the non-triviality of $\alpha$ (and placing it on the stacks); (2a) reading a finitary automorphism from the input tape; (2b) reading a directed automaton automorphism from the input tape; and (3) checking that the action of $\alpha$ on v that it has computed is non-trivial.

After Stage 1, $\mathcal {M}$ will be in state $q_\mathrm {comp}$. From here, $\mathcal {M}$ nondeterministically decides to either read from its input tape, performing either Stage 2a or 2b and returning to state $q_\mathrm {comp}$; or to finish reading from input by performing Stage 3.

We set both the check-stack and pushdown alphabets to be $\varDelta =\varGamma =\varSigma \sqcup \{\mathfrak {t}\}$.

Stage 1: Choosing a Witness $v = v_1 v_2 \cdots v_m \in \varSigma ^\star$.

If $\alpha$ is non-trivial, then there must exist a vertex $v \in \varSigma ^\star$ such that $\alpha \cdot v \ne v$. Thus, we nondeterministically choose such a witness from $\mathcal {R} = \varSigma ^\star \mathfrak {t}$ and store it on the check-stack, where the letter $\mathfrak {t}$ represents the top of the check-stack.

From the start state, $q_0$, $\mathcal {M}$ will copy the contents of the check-stack onto the pushdown, then enter the state $q_\mathrm {comp} \in Q$. Formally, this will be achieved by adding the transitions (for each $a \in \varSigma$):

$$ ( (q_0,\varepsilon ,(\mathfrak {b},\mathfrak {b})), (q_0,\mathfrak {t}\mathfrak {b}) ),\, ( (q_0,\varepsilon ,(a,\mathfrak {t})), (q_0,\mathfrak {t}a) ),\, ( (q_0,\varepsilon ,(\mathfrak {t},\mathfrak {t})), (q_\mathrm {comp},\mathfrak {t}) ). $$

This stage concludes with $\mathcal {M}$ in state $q_{\mathrm {comp}}$, and the read-head pointing to $(\mathfrak t, \mathfrak t)$. Note that whenever the machine is in state $q_{\mathrm {comp}}$ and $\alpha _1 \alpha _2 \cdots \alpha _k$ has been read from input, then the contents of pushdown will represent the permuted vertex $(\alpha _1 \alpha _2 \cdots \alpha _k) \cdot v$. Thus, the two stacks are initially the same as no input has been read and thus no group action has been simulated. In Stages 2a and 2b, only the height of the check-stack is impotant, that is, the exact contents of the check-stack will become relevant in Stage 3.

Stage 2a: Reading a Finitary Automorphism $\phi \in Y\cap \mathrm {Fin}(\mathcal {T}_d)$.

By definition, there exists some $k_\phi = \mathrm {depth}(\phi ) \in \mathbb {N}$ such that $\left. \phi \right| _u = 1$ for each $u \in \varSigma ^\star$ for which $\vert u \vert \geqslant k_\phi$. Thus, given a vertex $v = v_1 v_2 \cdots v_m \in \varSigma ^\star$, we have

$$ \phi (v) = \phi (v_1 v_2 \cdots v_{k_\phi }) \ v_{(k_\phi +1)} \cdots v_m. $$

Given that $\mathcal {M}$ is in state $q_\mathrm {comp}$ with $\mathfrak {t} v_1 v_2 \cdots v_m \mathfrak {b}$ on its pushdown, we will read $\phi$ from input, move to state $q_{\phi ,\varepsilon }$ and pop the $\mathfrak {t}$; we will then pop the next $k_\phi$ (or fewer if $m < k_\phi$) letters off the pushdown, and as we are popping these letters we visit the sequence of states $q_{\phi ,v_1}$, $q_{\phi ,v_1 v_2}$, ..., $q_{\phi ,v_1 v_2 \cdots v_{k_\phi }}$. From the final state in this sequence, we then push $\mathfrak t\phi (v_1\cdots v_{k_\phi })$ onto the pushdown, and return to the state $q_{\mathrm {comp}}$.

Formally, for letters $a,b \in \varSigma$, $\phi \in Y\cap \mathrm {Fin}(\mathcal {T}_d)$, and vertices $u,w\in \varSigma ^\star$ where $|u|< k_\phi$ and $|w|=k_\phi$, we have the transitions

$$ ( (q_{\mathrm {comp}}, \phi , (\mathfrak {t},\mathfrak {t})), (q_{\phi ,\varepsilon }, \varepsilon ) ), \ ( (q_{\phi ,u}, \varepsilon , (a,b)), (q_{\phi , ub}, \varepsilon ) ), $$

$$ ( (q_{\phi , w}, \varepsilon , (\varepsilon ,\varepsilon )), (q_\mathrm {comp}, \mathfrak {t}\phi (w)) ) $$

for the case where $m > k_\phi$, and

$$ ( (q_{\phi , u}, \varepsilon , (\mathfrak {b},\mathfrak {b})), (q_\mathrm {comp}, \mathfrak {t}\phi (u)\mathfrak {b}) ) $$

for the case where $m \leqslant k_\phi$. Notice that we have finitely many states and transitions since Y,  $\varSigma$ and each $k_\phi$ is finite.

Stage 2b: Reading a Directed Automorphism $\delta \in Y\cap \mathrm {Dir}(\mathcal {T}_d)$.

By Lemma 3, there exists some $\iota = \iota _1 \iota _2 \cdots \iota _s \in \varSigma ^\star$ and $\pi = \pi _1 \pi _2 \cdots \pi _t \in \varSigma ^\star$ such that $\mathrm {spine}(\delta ) = \iota \, \pi ^\omega$ and

$$ \delta (\iota \pi ^\omega ) = I_1 I_2 \cdots I_s \, \left( \varPi _1 \varPi _2 \cdots \varPi _t \right) ^\omega $$

where

$$ I_i = \left. \delta \right| _{\iota _1 \iota _2 \cdots \iota _{i-1}} (\iota _i) \qquad \text {and} \qquad \varPi _j = \left. \delta \right| _{\iota \, \pi _1 \pi _2 \cdots \pi _{j-1}}\!(\pi _j). $$

Given some vertex $v = v_1 v_2 \cdots v_m \in \varSigma ^\star$, let $\ell \in \mathbb {N}$ be largest such that $p = v_1 v_2 \cdots v_\ell$ is a prefix of the sequence $\iota \pi ^\omega = \mathrm {spine}(\delta )$. Then by definition of directed automorphism, $\delta ' = \delta \vert _p$ is directed and $\phi = \delta \vert _a$, where $a = v_{\ell }$, is finitary. Then, either $p = \iota _1 \iota _2 \cdots \iota _\ell$ and

$$ \delta (u) = (I_1 I_2 \cdots I_\ell ) \ \delta '(a) \ \phi (v_{\ell +2} v_{\ell +3} \cdots v_m), $$

or $p = \iota \pi ^k\pi _1\pi _2\cdots \pi _j$, with $\ell = |\iota |+k\cdot |\pi | + j$, and

$$ \delta (u) = (I_1 I_2 \cdots I_s) \, (\varPi _1 \varPi _2 \cdots \varPi _t)^k \, (\varPi _1 \varPi _2 \cdots \varPi _j) \ \delta '(a) \ \phi ( v_{\ell +2} v_{\ell +3} \cdots v_m). $$

Hence, from state $q_\mathrm {comp}$ with $\mathfrak {t} v_1 v_2 \cdots v_m \mathfrak {b}$ on its pushdown, $\mathcal M$ reads $\delta$ from input, moves to state $q_{\delta ,\iota ,0}$ and pops the $\mathfrak {t}$; it then pops pa off the pushdown, using states to remember the letter a and the part of the prefix to which the final letter of p belongs (i.e. $\iota _i$ or $\pi _j$). From here, $\mathcal {M}$ performs the finitary automorphism $\phi$ on the remainder of the pushdown (using the same construction as Stage 2a), then, in a sequence of transitions, pushes $\mathfrak {t}\delta (p)\delta '(a)$ and returns to state $q_\mathrm {comp}$. The key idea here is that, using only the knowledge of the letter a, the part of $\iota$ or $\pi$ to which the final letter of p belongs, and the height of the check-stack, that $\mathcal M$ is able to recover $\delta (p)\delta '(a)$.

We now give the details of the states and transitions involved in this stage of the construction.

We have states $q_{\delta ,\iota ,i}$ and $q_{\delta ,\pi ,j}$ with $0 \leqslant i \leqslant \vert \iota \vert$, $1 \leqslant j \leqslant \vert \pi \vert$; where $q_{\delta ,\iota ,i}$ represents that the word $\iota _1 \iota _2 \cdots \iota _i$ has been popped off the pushdown, and $q_{\delta ,\pi ,j}$ represents that a word $\iota \pi ^k\pi _1\pi _2\cdots \pi _j$ for some $k \in \mathbb {N}$ has been popped of the pushdown. Thus, we begin with the transition

$$ ( (q_\mathrm {comp}, \delta , (\mathfrak {t},\mathfrak {t})), (q_{\delta ,\iota ,0},\varepsilon ) ), $$

then for each $i,j\in \mathbb {N}$, $a \in \varSigma$ with $0 \leqslant i < \vert \iota \vert$ and $1 \leqslant j < \vert \pi \vert$, we have transitions

$$\begin{aligned} ( (q_{\delta ,\iota ,i}, \varepsilon , (a,\iota _{i+1})), (q_{\delta ,\iota ,(i+1)},\varepsilon ) ),&\ \ ( (q_{\delta ,\iota ,|\iota |}, \varepsilon , (a,\pi _1)), (q_{\delta ,\pi ,1},\varepsilon ) ), \\ ( (q_{\delta ,\pi ,j}, \varepsilon , (a,\pi _{j+1})), (q_{\delta ,\pi ,(j+1)},\varepsilon ) ),&\ \ ( (q_{\delta ,\pi ,|\pi |}, \varepsilon , (a,\pi _1)), (q_{\delta ,\pi ,1},\varepsilon ) ) \end{aligned}$$

to consume the prefix p.

After this, $\mathcal {M}$ will either be at the bottom of its stacks, or its read-head will see a letter on the pushdown that is not the next letter in the spine of $\delta$. Thus, for each $i,j \in \mathbb {N}$ with $0 \leqslant i \leqslant \vert \iota \vert$ and $1 \leqslant j \leqslant |\pi |$ we have states $q_{\delta ,\iota ,i,a}$ and $q_{\delta ,\pi ,j,a}$; and for each $b \in \varSigma$ we have transitions

$$ ( (q_{\delta ,\iota ,i}, \varepsilon , (b,a)), (q_{\delta ,\iota ,i,a},\varepsilon ) ) $$

where $a \ne \iota _{i+1}$ when $i < |\iota |$ and $a \ne \pi _1$ otherwise, and

$$ ( (q_{\delta ,\pi ,j}, \varepsilon , (b,a)), (q_{\delta ,\pi ,j,a},\varepsilon ) ) $$

where $a \ne \pi _{j+1}$ when $j < |\pi |$ and $a \ne \pi _1$ otherwise.

Hence, after these transitions, $\mathcal {M}$ has consumed pa from its pushdown and will either be at the bottom of its stacks in some state $q_{\delta ,\iota ,i}$ or $q_{\delta ,\pi ,j}$; or will be in some state $q_{\delta ,\iota ,i,a}$ or $q_{\delta ,\pi ,j,a}$. Note here that, if $\mathcal {M}$ is in the state $q_{\delta ,\iota ,i,a}$ or $q_{\delta ,\pi ,j,a}$, then from Lemma 3 we know $\delta ' = \delta \vert _{p}$ is equivalent to $\delta \vert _{\iota _1 \iota _2\cdots \iota _i}$ or $\delta \vert _{\iota \pi _1 \pi _2 \cdots \pi _j}$, respectively; and further, we know the finitary automorphism $\phi = \delta \vert _{pa} = \delta '\vert _a$.

Thus, for each state $q_{\delta ,\iota ,i,a}$ and $q_{\delta ,\pi ,a}$ we will follow a similar construction to Stage 2a, to perform the finitary automorphism $\phi$ to the remaining letters on the pushdown, then push $\delta '(a)$ and return to the state $r_{\delta ,\iota ,i}$ or $r_{\delta ,\pi ,j}$, respectively. For the case where $\mathcal {M}$ is at the bottom of its stacks we have transitions

$$ ( (q_{\delta ,\iota ,i}, \varepsilon , (\mathfrak {b},\mathfrak {b})), (r_{\delta ,\iota ,i}, \mathfrak {b}) ),\ \ ( (q_{\delta ,\pi ,i}, \varepsilon , (\mathfrak {b},\mathfrak {b})), (r_{\delta ,\pi ,i}, \mathfrak {b}) ) $$

with $0 \leqslant i \leqslant |\iota |$, $1 \leqslant j \leqslant |\pi |$.

Thus, after following these transitions, $\mathcal {M}$ is in some state $r_{\delta ,\iota ,i}$ or $r_{\delta ,\pi ,j}$ and all that remains is for $\mathcal {M}$ to push $\delta (p)$ with $p = \iota _1 \iota _2\cdots \iota _i$ or $p = \iota \pi ^k\pi _1 \pi _2\cdots \pi _k$, respectively, onto its pushdown. Thus, for each $i,j\in \mathbb {N}$ with $0 \leqslant i \leqslant |\iota |$ and $1 \leqslant j \leqslant |\pi |$, we have transitions

$$ ( (r_{\delta ,\pi ,i}, \varepsilon ,(\varepsilon ,\varepsilon )), (q_\mathrm {comp}, \mathfrak {t} I_1 I_2 \cdots I_i) ), \ \ ( (r_{\delta ,\pi ,j}, \varepsilon ,(\varepsilon ,\varepsilon )), (r_{\delta ,\pi }, \varPi _1 \varPi _2 \cdots \varPi _j) ) $$

where from the state $r_{\delta ,\pi }$, through a sequence of transitions, $\mathcal {M}$ will push the remaining $I\varPi ^k$ onto the pushdown. In particular, we have transitions

$$ ( (r_{\delta ,\pi }, \varepsilon ,(\varepsilon ,\varepsilon )), (r_{\delta ,\pi },\varPi ) ), \ \ ( (r_{\delta ,\pi }, \varepsilon ,(\varepsilon ,\varepsilon )), (q_\mathrm {comp},\mathfrak {t}I) ), $$

so that $\mathcal {M}$ can nondeterministically push some number of $\varPi$’s followed by $\mathfrak {t}I$ before it finishes this stage of the computation. We can assume that the machine pushes the correct number of $\varPi$’s onto its pushdown as otherwise it will not see $\mathfrak {t}$ on its check-stack while in state $q_\mathrm {comp}$ and thus would not be able to continue with its computation, as every subsequent stage (2a, 2b, 3) of the computation begins with the read-head pointing to $\mathfrak {t}$ on both stacks.

Once again it is clear that this stage of the construction requires only finitely many states and transitions.

Stage 3: Checking that the Action is Non-trivial.

At the beginning of this stage, the contents of the check-stack represent the chosen witness, v, and the contents of the pushdown represent the action of the input word, $\alpha$, on the witness, i.e., $\alpha \cdot v$.

In this stage $\mathcal {M}$ checks if the contents of its check-stack and pushdown differ. Formally, we have states $q_\mathrm {accept}$ and $q_{\mathrm {check}}$, with $q_\mathrm {accept}$ accepting; for each $a \in \varSigma$, we have transitions

$$ ( (q_\mathrm {comp}, \varepsilon , (\mathfrak {t},\mathfrak {t})), (q_\mathrm {check}, \varepsilon ) ), \ \ ( (q_\mathrm {check}, \varepsilon , (a,a)), (q_\mathrm {check}, \varepsilon ) ) $$

to pop identical entries of the pushdown; and for each $(a,b) \in \varSigma \times \varSigma$ with $a \ne b$ we have a transition

$$ ( (q_\mathrm {check},\varepsilon ,(a,b)), (q_\mathrm {accept},\varepsilon ) ) $$

to accept if the stacks differ by a letter.

Observe that if the two stacks are identical, then there is no path to the accepting state, $q_\mathrm {accept}$, and thus $\mathcal {M}$ will reject. Notice also that by definition of cspd automata, if $\mathcal M$ moves into $q_{\mathrm {check}}$ before all input has been read, then $\mathcal {M}$ will not accept, i.e., an accepting state is only effective if all input is consumed.

Soundness and Completeness.

If $\alpha$ is non-trivial, then there is a vertex $v \in \varSigma ^\star$ such that $\alpha \cdot v \ne v$, which $\mathcal {M}$ can nondeterministically choose to write on its check-stack and thus accept $\alpha$. If $\alpha$ is trivial, then $\alpha \cdot v = v$ for each vertex $v \in \varSigma ^\star$, and there is no choice of checking stack for which $\mathcal {M}$ will accept, so $\mathcal {M}$ will reject.

Thus, $\mathcal {M}$ accepts a word if and only if it is in $\mathrm {coW}(H,Y)$. Hence, the co-word problem $\mathrm {coW}(H,Y)$ is ET0L, completing our proof.    $\square$