We present decidability results for termination of classes of term rewritingsystems modulo permutative theories. Termination and innermost terminationmodulo permutative theories are shown to be decidable for term rewrite systems(TRS) whose right-hand side terms are restricted to be shallow (variables occurat depth at most one) and linear (each variable occurs at most once). Innermosttermination modulo permutative theories is also shown to be decidable forshallow TRS. We first show that a shallow TRS can be transformed into a flat(only variables and constants occur at depth one) TRS while preservingtermination and innermost termination. The decidability results are then provedby showing that (a) for right-flat right-linear (flat) TRS, non-termination(respectively, innermost non-termination) implies non-termination starting fromflat terms, and (b) for right-flat TRS, the existence of non-terminatingderivations starting from a given term is decidable. On the negative side, weshow PSPACE-hardness of termination and innermost termination for shallowright-linear TRS, and undecidability of termination for flat TRS.
展开▼
