Tags:conditional term rewriting, conditional term rewriting system, idempotent substitution, narrowing, narrowing tree, oriented conditional rewrite rule, parallel composition, reachability, regular tree grammar and term rewriting
Abstract:
The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expressions for substitutions obtained by all possible innermost-narrowing derivations that start with the pair and end with non-narrowable terms. In this paper, under a certain syntactic condition, we show a transformation of the grammar representation of a narrowing tree into another regular tree grammar that generates the ranges of substitutions generated by the grammar representation. In our previous work, such a transformation is restricted to the ranges w.r.t. a given single variable, and thus, the usefulness is limited. We extend the previous transformation by representing the range of a substitution as a tuple of terms, which is obtained by the coding for finite trees.
On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions