JCKassing: Added TRS Conditional - Operation Page

2026-03-18T11:37:52Z

Added TRS Conditional - Operation Page

New page

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 = {l1 → r1 | c1,...,ln → rn | cn} 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.

TODO: clarify the difference to [[TRS Conditional|TRS Conditional]]!

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

== References ==

[[Category:Categories]]

TRS Conditional - Operational Termination - Revision history

JCKassing: Added TRS Conditional - Operation Page