Decision Problems for Term Rewrite Systems and Recognizable Tree Languages

Abstract : We study the connections between recognizable tree languages and rewrite systems. We investigate some decision problems. Particularly, let us consider the property (P): a rewrite system S is such that, for every recognizable tree language F, the set of S-normal forms of terms in F is recognizable too. We prove that the property (P) is undecidable. We prove that the existential fragment of the theory of ground term algebras modulo a congruence $$\mathop \leftrightarrow \limits^* E$$ generated by a set E of equations such that there exists a finite, noetherian, confluent rewrite system S satisfying (P) with $$\mathop \leftrightarrow \limits^* S = \mathop \leftrightarrow \limits^* E$$ is undecidable. Nevertheless, we develop a decision procedure for the validity of linear formulas in a fragment of such a theory.
Type de document :
Communication dans un congrès
Proceedings of the 8th Annual Symposium on Theoretical Aspects of Computer Science, STACS 91, 1991, Munich, Germany. Springer Verlag, 480, pp.148--159, 1991, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00538875
Contributeur : Rémi Gilleron <>
Soumis le : mardi 23 novembre 2010 - 14:47:52
Dernière modification le : mardi 24 avril 2018 - 13:37:37

Identifiants

  • HAL Id : inria-00538875, version 1

Collections

Citation

Rémi Gilleron. Decision Problems for Term Rewrite Systems and Recognizable Tree Languages. Proceedings of the 8th Annual Symposium on Theoretical Aspects of Computer Science, STACS 91, 1991, Munich, Germany. Springer Verlag, 480, pp.148--159, 1991, Lecture Notes in Computer Science. 〈inria-00538875〉

Partager

Métriques

Consultations de la notice

143