Difference between revisions of "TRS Relative"
(Added TRS Relative Category Page) |
(Fixed some typos) |
||
| Line 6: | Line 6: | ||
Formally, a relative term rewrite system is a set R = {l<sub>1</sub> → r<sub>1</sub>,...,l<sub>n</sub> → r<sub>n</sub>} and a set S = {a<sub>1</sub> → b<sub>1</sub>,...,a<sub>n</sub> → b<sub>n</sub>} of finitely many rewrite rules denoted by R/S, see [1]. | Formally, a relative term rewrite system is a set R = {l<sub>1</sub> → r<sub>1</sub>,...,l<sub>n</sub> → r<sub>n</sub>} and a set S = {a<sub>1</sub> → b<sub>1</sub>,...,a<sub>n</sub> → b<sub>n</sub>} of finitely many rewrite rules denoted by R/S, see [1]. | ||
| − | A relative term rewrite system R is terminating if there exists no infinite rewrite sequence s<sub>0<sub>0</sub></sub> →<sub>R</sub> s<sub>0<sub>1</sub></sub> →<sub>S</sub> ... →<sub>S</sub> s<sub>1<sub>0</sub></sub> →<sub>R</sub> s<sub>1<sub>1</sub></sub> →<sub>S</sub> ... →<sub>S</sub> s<sub>2<sub>0</sub></sub> →<sub>R</sub> ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R. | + | A relative term rewrite system R/S is terminating if there exists no infinite rewrite sequence s<sub>0<sub>0</sub></sub> →<sub>R</sub> s<sub>0<sub>1</sub></sub> →<sub>S</sub> ... →<sub>S</sub> s<sub>1<sub>0</sub></sub> →<sub>R</sub> s<sub>1<sub>1</sub></sub> →<sub>S</sub> ... →<sub>S</sub> s<sub>2<sub>0</sub></sub> →<sub>R</sub> ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R. |
Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule. | Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule. | ||
| Line 17: | Line 17: | ||
<b>Input</b>: A relative term rewrite system R/S. | <b>Input</b>: A relative term rewrite system R/S. | ||
| − | <b>Question</b>: Does R terminate? | + | <b>Question</b>: Does R/S terminate? |
<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/S. | * "<b>YES</b>" followed by a termination proof, e.g., a ranking function proving termination of R/S. | ||
* "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R. | * "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R. | ||
| − | * "<b>MAYBE</b>" (indicating that the solver cannot prove termination). | + | * "<b>MAYBE</b>" (indicating that the solver cannot prove termination of R/S). |
Latest revision as of 17:12, 9 March 2026
The TRS Relative category is concerned with the question "Will every possible sequence of rewrites eventually stop using a certain subset of the given rewrite rules?". In other words, ifevery rule has a cost which is either 0 or 1, then does every possible reduction has a finite total cost?
Syntax & Semantic
Formally, a relative term rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} of finitely many rewrite rules denoted by R/S, see [1].
A relative 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.
Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule. Rules with cost 1 are in R and rules with costs 0 are in S. Then, relative termination is equal to the statement that every possible reduction has a finite total cost. The syntax and the semantics of term rewrite systems with costs at the rules are described here.
Problem
Input: A relative 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
- [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
