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 <>
Submitted on : Wednesday, May 24, 2006 - 4:32:19 PM
Last modification on : Friday, May 25, 2018 - 12:02:05 PM
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