No label defined (Q3976041)

[For the entire collection see Zbl 0731.00026.] This paper concerns the following problem (P): given a set \(R\) of rewrite rules, is the tree language of ground normal forms generated by the set \(R\) (GNFR, for short) finite? How can the language GNFR be finitely represented? In Section 1 the author says us how we can solve the problem (P): ``The main tool to develop effective methods for solving the questions of the problem (P) is the concept of reducibility trees (trees whose nodes are labeled by terms). We compute dynamically a finite reducibility tree for a given set of rewrite rules. Its construction is based on the characterization of the reducibility properties of its node labels. This leads us to produce a class of pumping theorems which are somewhat similar to pumping lemmas which have been produced for a number of classes of string languages. Theorems 3, 4 and 5 state that if there exists a `small' irreducible term, then there always exist a `bigger' irreducible term obtained by pumping. And this process can be repeated, the number of times, as often as we like. This provides an effective mean of getting finite reducibility trees, the leaf labels of which allow to decide the finiteness and the representation questions (see corollaries 1 and 2).''.