JCKassing: Small fixes

2026-06-09T12:15:33Z

Small fixes

JCKassing: Added TRS Equational Page

2026-03-18T11:29:46Z

Added TRS Equational Page

New page

The TRS Equational category is concerned with the question "Will every possible sequence of rewrites steps on equivalence classes terminate?".

== Syntax & Semantic ==

Formally, an equational term rewrite system is a set R = {l1 → r1,...,ln → rn} of finitely rewrite rules together a set S = {a1 = b1,...,an = bn} of finitely many term equations, called a ''theory''.

An equational term 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 where we can use the equations from S mid rewriting.

Here, a ''theory'' may be added to declarations of function symbols.

<pre>
fun ::= ( fun identifier number theory? )
theory ::= :theory [A | C | AC]
</pre>

* full rewriting modulo associativity / commutativity / associativity and commutativity

== Problem ==

Input: n equational term 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).

== References ==

[[Category:Categories]]

@@ Line 1: / Line 1: @@
-The TRS Equational category is concerned with the question "Will every possible sequence of rewrites steps on equivalence classes terminate?".
+The TRS Equational category is concerned with the question "Will every possible sequence of rewrite steps on equivalence classes terminate?".
 == Syntax & Semantic ==
-Formally, an equational 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>} of finitely rewrite rules together a set S = {a<sub>1</sub> = b<sub>1</sub>,...,a<sub>n</sub> = b<sub>n</sub>} of finitely many term equations, called a ''theory''.
+Formally, an equational 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>} of finitely many rewrite rules together with a set S = {a<sub>1</sub> = b<sub>1</sub>,...,a<sub>m</sub> = b<sub>m</sub>} of finitely many term equations, called a ''theory''.
 An equational 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> =<sub>S</sub> ... =<sub>S</sub> s<sub>1<sub>0</sub></sub> &rarr;<sub>R</sub> s<sub>1<sub>1</sub></sub> =<sub>S</sub> ... =<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 where we can use the equations from S mid rewriting.
@@ Line 18: / Line 18: @@
 == Problem ==
-<b>Input</b>: n equational term rewrite system R/S.
+<b>Input</b>: An equational term rewrite system R/S.
 <b>Question</b>: Does R/S terminate?
@@ Line 26: / Line 26: @@
 * "<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 of R/S).
 [[Category:Categories]]

TRS Equational - Revision history

JCKassing: Small fixes

JCKassing: Added TRS Equational Page