SRS Relative

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

Syntax & Semantic

Strings are terms where every function symbol has arity 1, i.e., exactly one argument. Formally, a relative string 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 where all the occuring terms are strings.

A relative string rewrite system R/S 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 string rewrite systems with costs at the rules are described here.

Problem

Input: A relative string rewrite system R/S.

Question: Does R/S 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 of R/S).