Regular sets of descendants for constructor-based rewrite systems (Q4938423)

In the area of term rewriting systems, an important issue of study, with applications to automated deduction and program validation, is representing the set \(R^*(E)\) of descendants (i.e., reachable terms) for a given (starting) set \(E\). The topic is especially elaborated for regular tree languages; algorithms constructing finite tree automaton recognizing \(R^*(E)\) for a regular tree language \(E\) have been developed for rewrite systems satisfying various restrictions. The paper is a contribution to the mentioned area, showing one such algorithm. The author considers constructor-based rewrite systems whose right-hand sides satisfy: linearity (each variable appears at most once), no nested function symbols, function arguments are variables or ground terms (while left-linearity is not assumed). As the starting set \(E\), he takes the set of the ground constructor-instances (data-instances) of a given linear term. The paper ends with sketching some applications, including unification of linear equations and program testing. For the entire collection see [Zbl 0921.00037].