Deterministic tree pushdown automata and monadic tree rewriting systems (Q1118421)

The starting point of this study is a paper by \textit{J. H. Gallier} and \textit{R. V. Book} [Theor. Comput. Sci. 37, 123-150 (1985; Zbl 0602.68069)]. First a streamlined version of the deterministic tree pushdown automaton (dtpda) of Gallier and Book is considered. It is shown that the capabilities to publicate or to delete arbitrarily large subtrees in the stacks strictly increase the recognition power of these automata. Following Gallier and Book, a tree rewriting system is said to be monadic if in all of its rules \(s\to t\), s is linear, hg(s)\(\geq 1\), var(t)\(\subseteq var(s)\) and hg(t)\(\leq 1\), where var(u) and hg(u) denote, respectively, the set of variables and the height of the tree u. Gallier and Book proved that any finite union of congruence classes of a canonical monadic tree rewriting system can be recognized by a dtpda with the capability to check whether the final stack belongs to a given regular forest. Here the author shows that this additional power is not needed, and some further related results are also presented.