Difference between revisions of "TRS Conditional"
(Added TRS Conditional Page) |
(Small fixes) |
||
| Line 1: | Line 1: | ||
| − | The TRS Conditional category is concerned with the question "Will every possible sequence of conditional | + | The TRS Conditional category is concerned with the question "Will every possible sequence of conditional rewrite steps terminate?" |
where a conditional rewrite step may depend on the reachability between two independent terms, e.g., can 'leq(<i>t</i>,<i>s</i>)' be evaluated to 'true'? | where a conditional rewrite step may depend on the reachability between two independent terms, e.g., can 'leq(<i>t</i>,<i>s</i>)' be evaluated to 'true'? | ||
| Line 16: | Line 16: | ||
<b>Possible Outputs</b>: | <b>Possible Outputs</b>: | ||
* "<b>YES</b>" followed by a termination proof, e.g., a ranking function proving termination of R. | * "<b>YES</b>" followed by a termination proof, e.g., a ranking function proving termination of R. | ||
| − | * "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite of R. | + | * "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence of R. |
* "<b>MAYBE</b>" (indicating that the solver cannot prove termination of R). | * "<b>MAYBE</b>" (indicating that the solver cannot prove termination of R). | ||
| − | |||
| − | |||
| − | |||
| − | |||
[[Category:Categories]] | [[Category:Categories]] | ||
Latest revision as of 12:18, 9 June 2026
The TRS Conditional category is concerned with the question "Will every possible sequence of conditional rewrite 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.
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 sequence of R.
- "MAYBE" (indicating that the solver cannot prove termination of R).
