Rewrite systems are directed equations used to compute by repeatedly replacing subterms of a given formula with equal terms until the simplest form possible is obtained. This simplest form is what we call a normal form. The theory of rewriting is in essence a theory of normal forms. Most frequently we are interested in ground normal forms (normal forms without any variables). Since we are only looking at ground terms, the set of ground normal forms of a rewrite system R may be viewed as a formal language generated by R.
In this paper we study the language of ground normal forms (GNFR for short) and give effective algorithms for deciding certain problems about it such as finiteness and representation. To solve these problems pumping lemmas are stated and proved for GNFR.
The results we obtain here have a number of direct applications to problems appearing in Inductive theorem proving, Logic programming, Functional programming, Machine Learning, Algebraic specifications, Equational Logic, Communicating processus etc...