JCKassing: Fixed some typos

2026-03-09T17:12:38Z

Fixed some typos

JCKassing: Added TRS Relative Category Page

2026-03-09T09:48:02Z

Added TRS Relative Category Page

New page

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 = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} 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 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 term rewrite systems with costs at the rules are described [[Term Rewriting | 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.

[[Category:Categories]]

@@ Line 6: / Line 6: @@
 Formally, a relative term 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, see [1].
-A relative term rewrite system R 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 term 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.
@@ Line 17: / Line 17: @@
 <b>Input</b>: A relative term rewrite system R/S.
-<b>Question</b>: Does R terminate?
+<b>Question</b>: Does R/S terminate?
 <b>Possible Outputs</b>:
 * "<b>YES</b>" followed by a termination proof, e.g., a ranking function proving termination of R/S.
 * "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
-* "<b>MAYBE</b>" (indicating that the solver cannot prove termination).
+* "<b>MAYBE</b>" (indicating that the solver cannot prove termination of R/S).

TRS Relative - Revision history

JCKassing: Fixed some typos

JCKassing: Added TRS Relative Category Page