The following definition is from Doner (1970)
A bottom-up tree automaton is a tuple $\mathcal{A} = \langle Q, \Sigma, \delta, q_0, F \rangle$ where
- $Q$ is a finite set of states.
- $\Sigma$ is an alphabet.
- $\delta: S \times S \times \Sigma \to S$ is the transition function.
- $q_0 \in S$ is the initial states.
- $F \subseteq Q$ is the set of final states.
Associated with $\mathcal{A}$ is the function $\delta': \Sigma^{\#} \to S$ defined by $\delta'(\Lambda) = q_0, \delta'(\sigma[\tau, \tau']) = \delta(\delta'(\tau), \delta'(\tau'), \sigma)$ for all $\sigma \in \Sigma$ and $\tau, \tau' \in \Sigma$. $\mathcal{A}$ accepts a tree $\tau \in \Sigma^{\#}$ if $\delta'(\tau) \in F$. $T(\mathcal{A})$ is the set of $\Sigma$-trees accepted by $\mathcal{A}$.
I have the following definition:
A non-deterministic top-down tree automaton is a tuple $\mathcal{A} = \left(Q, \Sigma, \delta, q_0, F\right)$, where
- $Q$ is a finite set of states.
- $\Sigma$ is an alphabet.
- $\delta: Q \times \Sigma \rightarrow \mathcal{P}(Q \times Q)$ is the transition function.
- $q_0$ is the initial state.
- $F \subseteq Q$ is the set of final states.
A run $\varrho$ of $\mathcal{A}$ on $t \in T_{\Sigma}$ is a $Q$-labelled tree $\varrho$ with $\operatorname{dom}(\varrho)= \{\lambda\} \cup \{u b \mid u \in \operatorname{dom}(t), b \in\{0,1\}\}$ such that $\varrho(u)=q_0$, and $(\varrho(u 0), \varrho(u 1)) \in \delta(\varrho(u), t(u))$, for all $u \in \operatorname{dom}(t)$.
$\varrho$ is accepting if all leaves of $\varrho$ are labeled with states in $F$, i.e. $\varrho(u) \in F$, for all $u \in \operatorname{dom}(\varrho) \backslash \operatorname{dom}(t)$.
A tree $t$ is recognized by $\mathcal{A}$ if there is an accepting run of $\mathcal{A}$ on $t$.
$T(\mathcal{A})$ denotes the set of trees that are recognized by $\mathcal{A}$.
The definition of Doner is very neat. What would be the way to adapt the second definition so that it resembles the first?
My personal preference is to have a direction-neutral nondeterministic tree automaton. The transition relation holds of triples $(s,c),(s_0,c_0),(s_1,c_1)$ (where $s$ is a state, $c$ a character) if runs are allowed to have nodes with state $s$ and symbol $c$ whose children have state-symbol pairs $(s_0,c_0)$ and $(s_1,c_1)$.
You can then require that the states of the root fall into some allowed set and the states of the leaves fall into some allowed set.
Alternately, you could patch up the definition you provided by specifying allowed state-character pairs on the leaves.