BOTTOM-UP TREE PUSHDOWN-AUTOMATA - CLASSIFICATION AND CONNECTION WITH REWRITE SYSTEMS

We define different types of bottom-up tree pushdown automata and study their connections with rewrite systems. Along this line of research we complete and generalize the results of Gallier, Book and Salomaa. We define the notion of a tail-reduction-free (trf) rewrite system. Using the decidability of ground reducibility, we prove the decidability of the trf property. Monadic rewrite systems of Book, Gallier and Salomaa become a natural particular case of trf rewrite systems. We associate a deterministic bottom-up tree pushdown automaton with any left-linear trf rewrite system. Finally, we generalize monadic rewrite systems by introducing the notion of a semi-monadic rewrite system and show that, like a monadic rewrite system, it preserves recognizability.