HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 4:32:19 PM
Last modification on : Friday, February 4, 2022 - 3:08:36 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 4:01:06 PM


  • 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⟩



Record views


Files downloads