JCKassing: Added SRS Relative Category Page

2026-03-10T16:27:05Z

Added SRS Relative Category Page

New page

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 = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} 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 s00 →R s01 →S ... →S s10 →R s11 →S ... →S s20 →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 [[Term Rewriting | 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).

[[Category:Categories]]

SRS Relative - Revision history

JCKassing: Added SRS Relative Category Page