Difference between revisions of "TRS Relative"
(Added TRS Relative Category Page) |
m (Small fixes) |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
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?". | 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, | + | In other words, if every rule has a cost which is either 0 or 1, then does every possible reduction have a finite total cost? |
| + | |||
| + | == Category Motivation == | ||
| + | |||
| + | Relative termination isolates the rules whose usage should be finite while allowing auxiliary rules to be used freely in between and is used in different termination and complexity analysis techniques. | ||
== Syntax & Semantic == | == Syntax & Semantic == | ||
| − | 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> | + | 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>m</sub> → b<sub>m</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 | + | A relative term rewrite system R/S is terminating if there exists no infinite rewrite sequence s<sub>0</sub> →<sub>R</sub> s'<sub>0</sub> →<sup>*</sup><sub>S</sub> s<sub>1</sub> →<sub>R</sub> s'<sub>1</sub> →<sup>*</sup><sub>S</sub> s<sub>2</sub> →<sub>R</sub> ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R. |
| − | Instead of the two | + | Instead of the two separate 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. | 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. | Then, relative termination is equal to the statement that every possible reduction has a finite total cost. | ||
| Line 17: | Line 21: | ||
<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 12:06, 9 June 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, if every rule has a cost which is either 0 or 1, then does every possible reduction have a finite total cost?
Category Motivation
Relative termination isolates the rules whose usage should be finite while allowing auxiliary rules to be used freely in between and is used in different termination and complexity analysis techniques.
Syntax & Semantic
Formally, a relative term rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,am → bm} 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 s0 →R s'0 →*S s1 →R s'1 →*S s2 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.
Instead of the two separate 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.
