TRS Conditional

The TRS Conditional category is concerned with the question "Will every possible sequence of conditional rewrites steps terminate?" where a conditional rewrite step may depend on the reachability between two independent terms, e.g., can 'leq(t,s)' be evaluated to 'true'?

Syntax & Semantic

Formally, a conditional term rewrite system is a set R = {l₁ → r₁ | c₁,...,l_n → r_n | c_n} of finitely many conditional rewrite rules. A conditional rewrite rule is a rewrite rule l → r with an additional condition, a reachability constraint, that has to be satisfied to use the rewrite rule. There are multiple different ways one can interpret these conditions, e.g., oriented, joined, and convertible.

Problem

Input: A conditional term rewrite system R.

Question: Does R terminate?

Possible Outputs:

• "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
• "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite of R.
• "MAYBE" (indicating that the solver cannot prove termination of R).