TRS Equational

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 = {l₁ → r₁,...,l_n → r_n} of finitely rewrite rules together a set S = {a₁ = b₁,...,a_n = b_n} 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₀₀ →_R s₀₁ =_S ... =_S s₁₀ →_R s₁₁ =_S ... =_S s₂₀ →_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.

fun ::= ( fun identifier number theory? )
theory ::= :theory [A | C | AC]

• 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).