Regular Sets of Descendants for Constructor-based Rewrite Systems

Pierre Rety

Keywords : term rewriting, tree automata.

Abstract :
Starting from the regular tree language $E$ of ground constructor-instances
of any linear term, we build a finite tree automaton that recognizes
the set of descendants $R^*(E)$ of $E$ for a constructor-based term
rewrite system whose right-hand-sides fulfill the following three
restrictions\,: linearity, no nested function symbols, function arguments are
variables or ground terms.
Note that left-linearity is not assumed.
We next present several applications.