Reductions in tree replacement systems (Q1082092)

Certain kinds of Church-Rosser tree replacement systems called ''reduction systems'' are studied. The concept of a tree rewriting system with a ''norm'' is introduced and studied. A new ''tree reducing machine'' which reduces every input tree to an irreducible tree is defined. As a consequence, when the norm under consideration is the size of the tree (the number of nodes), the word problem for finite Church-Rosser reduction systems is decidable in linear time (in the size of the input tree). Church-Rosser monadic reduction systems generalizing the monadic Thue systems of \textit{R. V. Book} [J. Assoc. Comput. Mach. 29, 171-182 (1982; Zbl 0478.68032)] and \textit{R. V. Book}, \textit{M. Jantzen}, and \textit{C. Wrathall} [Theor. Comput. Sci. 19, 231-251 (1982; Zbl 0488.03020)] are also studied. It is shown that every congruence class and every finite union of congruence classes defined by such a system is accepted by a deterministic bottom-up tree pushdown automaton. This new form of a tree automaton is briefly studied.