# Tree stack automaton

A tree stack automaton (plural: tree stack automata) is a formalism considered in automata theory. It is a finite-state automaton with the additional ability to manipulate a tree-shaped stack. It is an automaton with storage whose storage roughly resembles the configurations of a thread automaton. A restricted class of tree stack automata recognises exactly the languages generated by multiple context-free grammars (or linear context-free rewriting systems).

## Definition
### Tree stack

For a finite and non-empty set Γ, a tree stack over Γ is a tuple (t, p) where
* t is a partial function from strings of positive integers to the set Γ ∪ {@} with prefix-closed domain (called tree),
* @ (called bottom symbol) is not in Γ and appears exactly at the root of t, and
* p is an element of the domain of t (called stack pointer).
The set of all tree stacks over Γ is denoted by TS(Γ).
The set of predicates on TS(Γ), denoted by Pred(Γ), contains the following unary predicates:
* true which is true for any tree stack over Γ,
* bottom which is true for tree stacks whose stack pointer points to the bottom symbol, and
* equals(γ) which is true for some tree stack (t, p) if t(p) = γ,
for every γ ∈ Γ.
The set of instructions on TS(Γ), denoted by Instr(Γ), contains the following partial functions:
* id: TS(Γ) → TS(Γ) which is the identity function on TS(Γ),
* push$_{n,γ}$: TS(Γ) → TS(Γ) which adds for a given tree stack (t,p) a pair (pn ↦ γ) to the tree t and sets the stack pointer to pn (i.e. it pushes γ to the n-th child position) if pn is not yet in the domain of t,
* up$_n$: TS(Γ) → TS(Γ) which replaces the current stack pointer p by pn (i.e. it moves the stack pointer to the n-th child position) if pn is in the domain of t,
* down: TS(Γ) → TS(Γ) which removes the last symbol from the stack pointer (i.e. it moves the stack pointer to the parent position), and
* set$_γ$: TS(Γ) → TS(Γ) which replaces the symbol currently under the stack pointer by γ,
for every positive integer n and every γ ∈ Γ.
| Illustration of the instruction id on a tree stack | Illustration of the instruction push on a tree stack | Illustration of the instructions up and down on a tree stack | Illustration of the instruction set on a tree stack |

### Tree stack automata

A tree stack automaton is a 6-tuple A = (Q, Γ, Σ, q$_i$, δ, Q$_f$) where
* Q, Γ, and Σ are finite sets (whose elements are called states, stack symbols, and input symbols, respectively),
* q$_i$ ∈ Q (the initial state),
* δ ⊆$_{fin.}$ Q × (Σ ∪ {ε}) × Pred(Γ) × Instr(Γ) × Q (whose elements are called transitions), and
* Q$_f$ ⊆ TS(Γ) (whose elements are called final states).
A configuration of A is a tuple (q, c, w) where
* q is a state (the current state),
* c is a tree stack (the current tree stack), and
* w is a word over Σ (the remaining word to be read).
A transition τ = (q$_1$, u, p, f, q$_2$) is applicable to a configuration (q, c, w) if
* q$_1$ = q,
* p is true on c,
* f is defined for c, and
* u is a prefix of w.
The transition relation of A is the binary relation ⊢ on configurations of A that is the union of all the relations ⊢$_τ$ for a transition τ = (q$_1$, u, p, f, q$_2$) where, whenever τ is applicable to (q, c, w), we have (q, c, w) ⊢$_τ$ (q$_2$, f(c), v) and v is obtained from w by removing the prefix u.
The language of A is the set of all words w for which there is some state q ∈ Q$_f$ and some tree stack c such that (q$_i$, c$_i$, w) ⊢$^*$ (q, c, ε) where
* ⊢$^*$ is the reflexive transitive closure of ⊢ and
* c$_i$ = (t$_i$, ε) such that t$_i$ assigns for ε the symbol @ and is undefined otherwise.

## Related formalisms

Tree stack automata are equivalent to Turing machines.
A tree stack automaton is called k-restricted for some positive natural number k if, during any run of the automaton, any position of the tree stack is accessed at most k times from below.
1-restricted tree stack automata are equivalent to pushdown automata and therefore also to context-free grammars. k-restricted tree stack automata are equivalent to linear context-free rewriting systems and multiple context-free grammars of fan-out at most k (for every positive integer k).