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 have a finite total cost?

Syntax & Semantic

Strings are terms where every function symbol has arity 1, i.e., exactly one argument. Additionally, the same variable appears on both the left and right sides of each rule. Formally, a relative string rewrite system is a set R = {l₁ → r₁,...,l_n → r_n} and a set S = {a₁ → b₁,...,a_m → b_m} of finitely many rewrite rules denoted by R/S where all the occurring terms are strings.

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

Instead of the two separate 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).