Rewriting preserving recognizability of finite tree languages (Q1936231)

A term rewrite system (TRS) \(R\) over a ranked alphabet \(\Sigma\) is said to preserve \(\Sigma\)-recognizability if the set of all descendants of any recognizable tree language over \(\Sigma\) is a recognizable tree language, and it preserves recognizability if this holds for all recognizable tree languages over any ranked alphabet containing \(\Sigma\). Similarly, \(R\) is said to preserve \(\Sigma\)-recognizability or recognizability of finite tree languages if the respective conditions hold for finite tree languages. Finally, any of these properties may be effective in the sense that a finite tree automaton recognizing the set of descendants can be constructed from a recognizer of the given tree language. The author presents many results about several aspects of these notions. Exploring the relationships between them he shows, for example, that a linear TRS may effectively preserve \(\Sigma\)-recognizability of finite tree languages without preserving recognizability. He also studies the recognizability preservation properties of some special types of TRSs, and the main theorem states that certain TRSs effectively preserve the recognizability of finite tree languages. Furthermore, several basic questions, such as reachability, joinability, local confluence and inclusion, are shown to be decidable for TRSs that effectively preserve the recognizability of finite tree languages.