Some decidability results on one-pass reductions (Q2423761)

One-pass reduction by a term-rewriting system (TRS) means that the processing of an input tree (i.e., term) proceeds in one direction, either inside-out (IO) from the leaves towards the root, or outside-in (OI) from the root towards the leaves, without ever rewriting anything already previously rewritten. In this paper the author considers some second-order decidability problems concerning one-pass rewriting; `second-order' signifies that the problems concern tree languages rather than individual trees. Let \(R\) be a given TRS. The IO sentential forms of a tree \(t\) are the trees appearing in some IO one-pass reduction sequence of \(R\) that begins with \(t\). For any tree language \(L\), let \(\operatorname{IOSF}(L)\) denote the set of all IO sentential forms of the members of \(L\). The set \(\operatorname{OISF}(L)\) of OI sentential forms of \(L\) is defined in a corresponding way. It is shown that for certain classes of TRSs and any recognizable tree languages \(L\) and \(M\) the following questions are decidable: (1) the inclusion problem ``\(\operatorname{IOSF}(L) \subseteq M?\)'', (2) the reachability problem ``\(\operatorname{IOSF}(L) \cap M \neq \emptyset?\)'', and (3) the common ancestor problems ``Is there a tree \(t\) such that \(\operatorname{IOSF}(t) \cap L \neq \emptyset\) and \(\operatorname{IOSF}(t) \cap M \neq \emptyset\)?'' and ``Is there a tree \(t\) such that \(\operatorname{OISF}(t) \cap L \neq \emptyset\) and \(\operatorname{OISF}(t) \cap M \neq \emptyset\)?''