TRS Relative

The TRS Relative category is concerned with the question "Will every possible sequence of rewrites eventually stop using a certain subset of the given rewrite rules?". In other words, ifevery rule has a cost which is either 0 or 1, then does every possible reduction has a finite total cost?

Syntax & Semantic

Formally, a relative term rewrite system is a set R = {l₁ → r₁,...,l_n → r_n} and a set S = {a₁ → b₁,...,a_n → b_n} of finitely many rewrite rules denoted by R/S, see [1].

A relative term rewrite system R is terminating if there exists no infinite rewrite sequence s₀₀ →_R s₀₁ →_S ... →_S s₁₀ →_R s₁₁ →_S ... →_S s₂₀ →_R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule. Rules with cost 1 are in R and rules with costs 0 are in S. Then, relative termination is equal to the statement that every possible reduction has a finite total cost. The syntax and the semantics of term rewrite systems with costs at the rules are described here.

Problem

Input: A relative term rewrite system R/S.

Question: Does R terminate?

Possible Outputs:

• "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
• "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
• "MAYBE" (indicating that the solver cannot prove termination).

References

• [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.