DECIDABILITY OF REGULARITY AND RELATED PROPERTIES OF GROUND NORMAL-FORM LANGUAGES

We study language-theoretical properties of the set of reducible groun d 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 p roperty of finite irreducibility of a term with respect to a variable and prove it to be decidable. It turns out that this property generali zes numerous interesting properties of the language of ground normal f orms. In particular, we show that testing regularity of this language can be reduced to verifying this property. In this way we prove the de cidability of the regularity of the set of ground normal forms, the pr oblem mentioned in the list of open problems in rewriting by Dershowit z, Jouannaud, and Klop (in ''Proceedings, 4th Conference on Rewriting Techniques and Applications'' ( R. V. Book, Ed.), Springer-Verlag, Ber lin/New York, 1991). Also, the decidability of the existence of an equ ivalent ground term rewriting system and some other results are proved . (C) 1995 Academic Press. Inc.