REGULAR TREE LANGUAGES AND REWRITE SYSTEMS

Article type: Research Article

Authors: Gilleron, Rémy | Tison, Sophie

Affiliations: LIFL, URA 369 CNRS, IEEA Université de Lille I. email: {gilleron, tison}@lifl.lifl.fr

Abstract: We present a collection of results on regular tree languages and rewrite systems. Moreover we prove the undecidability of the preservation of regularity by rewrite systems. More precisely we prove that it is undecidable whether or not for a set E of equations the set E(R) congruence closure of set R is a regular tree language whenever R is a regular tree language. It is equally undecidable whether or not for a confluent and terminating rewrite system S the set S(R) of ground S-normal forms of set R is a regular tree language whenever R is a regular tree language. Finally we study fragments of the theory of ground term algebras modulo congruence generated by a set of equations which can be compiled in a terminating, confluent rewrite system which preserves regularity.

DOI: 10.3233/FI-1995-24127

Journal: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 157-175, 1995