SRS Relative - Revision history

JCKassing: Use the transitive-reflexive closure!

2026-06-09T12:24:08Z

Use the transitive-reflexive closure!

JCKassing: Small fixes

2026-06-09T12:23:17Z

Small fixes

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]]

@@ Line 8: / Line 8: @@
 Formally, a relative string rewrite system is a set R = {l<sub>1</sub> &rarr; r<sub>1</sub>,...,l<sub>n</sub> &rarr; r<sub>n</sub>} and a set S = {a<sub>1</sub> &rarr; b<sub>1</sub>,...,a<sub>m</sub> &rarr; b<sub>m</sub>} 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<sub>0<sub>0</sub></sub> &rarr;<sub>R</sub> s<sub>0<sub>1</sub></sub> &rarr;<sub>S</sub> ... &rarr;<sub>S</sub> s<sub>1<sub>0</sub></sub> &rarr;<sub>R</sub> s<sub>1<sub>1</sub></sub> &rarr;<sub>S</sub> ... &rarr;<sub>S</sub> s<sub>2<sub>0</sub></sub> &rarr;<sub>R</sub>  ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.
+A relative string rewrite system R/S is terminating if there exists no infinite rewrite sequence s<sub>0</sub> &rarr;<sub>R</sub> s'<sub>0</sub> &rarr;<sup>*</sup><sub>S</sub> s<sub>1</sub> &rarr;<sub>R</sub> s'<sub>1</sub> &rarr;<sup>*</sup><sub>S</sub> s<sub>2</sub> &rarr;<sub>R</sub>  ..., 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.

@@ Line 1: / Line 1: @@
 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?
+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.
-Formally, a relative string rewrite system is a set R = {l<sub>1</sub> &rarr; r<sub>1</sub>,...,l<sub>n</sub> &rarr; r<sub>n</sub>} and a set S = {a<sub>1</sub> &rarr; b<sub>1</sub>,...,a<sub>n</sub> &rarr; b<sub>n</sub>} of finitely many rewrite rules denoted by R/S where all the occuring terms are strings.
+Additionally, the same variable appears on both the left and right sides of each rule.
 A relative string rewrite system R/S is terminating if there exists no infinite rewrite sequence s<sub>0<sub>0</sub></sub> &rarr;<sub>R</sub> s<sub>0<sub>1</sub></sub> &rarr;<sub>S</sub> ... &rarr;<sub>S</sub> s<sub>1<sub>0</sub></sub> &rarr;<sub>R</sub> s<sub>1<sub>1</sub></sub> &rarr;<sub>S</sub> ... &rarr;<sub>S</sub> s<sub>2<sub>0</sub></sub> &rarr;<sub>R</sub>  ..., 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.
+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.