Decidable properties and optimal normalization in persistent term rewriting systems

Projet PARAWe 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