Decidable properties and optimal normalization in persistent term rewriting systems

Zurab Khasidashvili 1
1 PARA - Parallélisme
Inria Paris-Rocquencourt
Abstract : We introduce Persistent Term Rewriting Systems (PTRSs) by restriting ways of redex-creation during reductions in Orthogonal Term Rewriting Systems (OTRSs). In particular, Recursive (Applicative) Program Schemes (RPSs), considered as TRSs are persistent. We establish criteria for weak and strong normalization of terms in PTRSs and prove that they are decidable. The decidability of weak normalization implies immediately that RPSs do not have full computational power. We find a decidable, necessary and sufficient condition for syntactical equivalence of PTRSs. We also prove that the reducibility problem is decidable in PTRSs. Finally, we design an optimal, sequential normalizing strategy for PTRSs. In particular, if is a normalizable term in an RPS, then the number of steps in the optimal reduction of t to normal coincides with the minimum number of redex families contracted in reductions of t to normal form.
Type de document :
[Research Report] RR-1837, INRIA. 1993
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 16:32:19
Dernière modification le : samedi 17 septembre 2016 - 01:27:52
Document(s) archivé(s) le : mardi 12 avril 2011 - 16:01:06



  • HAL Id : inria-00074835, version 1



Zurab Khasidashvili. Decidable properties and optimal normalization in persistent term rewriting systems. [Research Report] RR-1837, INRIA. 1993. 〈inria-00074835〉



Consultations de la notice


Téléchargements de fichiers