We study language-theoretical properties of
the set of reducible
ground terms and its complement - the set of ground normal forms
induced by a given rewriting system.
As a tool for our analysis we introduce the property of finite
irreducibility of a term
with respect to a variable and prove it to be decidable. It turns out
that this property generalizes numerous interesting properties of
the language of ground normal forms. In particular, we show that
testing regularity of this language can be reduced to verifying this
property. In this way we prove the decidability of the regularity of the set of ground
normal forms, the problem mentioned in the
list of open problems in
rewriting [N.Dershowitz, J.-P.Jouannaud, J.W.Klop, Open Problems in
Rewriting, Proceedings 4th Conference on Rewriting Techniques and
Applications, Lect. Notes Comput. Sci, vol. 488, 1991]. Also, the
decidability
of the existence of an equivalent ground term rewriting system and
some other results are proved.