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

TRS Equational - Revision history

JCKassing: Added TRS Equational Page