Regular sets of descendants for constructor-based rewrite systems
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].
- Tree automata for rewrite strategies
- Regular sets of descendants by leftmost strategy
- Reachability analysis of innermost rewriting
- scientific article; zbMATH DE number 4164137 (Why is no real title available?)
- scientific article; zbMATH DE number 4049112 (Why is no real title available?)
- scientific article; zbMATH DE number 2090069 (Why is no real title available?)
- Homomorphisms and concurrent term rewriting
- Reachability analysis over term rewriting systems
- Termination criteria for tree automata completion
- Descendants of a recognizable tree language for sets of linear monadic term rewrite rules
This page was built for publication: Regular sets of descendants for constructor-based rewrite systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4938423)
