Decidable properties and optimal normalization in persistent term rewriting systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1993

Decidable properties and optimal normalization in persistent term rewriting systems

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-1837.pdf (928.11 Ko) Télécharger le fichier

Dates et versions

inria-00074835 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00074835 , version 1

Citer

Zurab Khasidashvili. Decidable properties and optimal normalization in persistent term rewriting systems. [Research Report] RR-1837, INRIA. 1993. ⟨inria-00074835⟩
60 Consultations
29 Téléchargements

Partager

Gmail Facebook X LinkedIn More