Difference between revisions of "TRS Standard"
m (JCKassing moved page Category TRS Standard to TRS Standard: removed Category) |
(Added a motivation and link to the ari format) |
||
| Line 1: | Line 1: | ||
The TRS Standard category is concerned with the question "Will every possible sequence of rewrites eventually stop?". | The TRS Standard category is concerned with the question "Will every possible sequence of rewrites eventually stop?". | ||
In other words, does every computation defined by the rewrite rules eventually reach a normal form (a term where no rule applies)? | In other words, does every computation defined by the rewrite rules eventually reach a normal form (a term where no rule applies)? | ||
| + | |||
| + | == Category Motivation == | ||
| + | |||
| + | This category evaluates tools on termination of standard first-order term rewrite systems with unrestricted rewriting which is one of the basic problems in the competition. Many of the other termination problems are either special forms of this problem, or can be reduced to this problem. | ||
== Syntax & Semantic == | == Syntax & Semantic == | ||
| − | The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]]. | + | The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here]. |
Formally, a term rewrite system R = {l<sub>1</sub> → r<sub>1</sub>,...,l<sub>n</sub> → r<sub>n</sub>} is a finite set of rewrite rules, see [1]. | Formally, a term rewrite system R = {l<sub>1</sub> → r<sub>1</sub>,...,l<sub>n</sub> → r<sub>n</sub>} is a finite set of rewrite rules, see [1]. | ||
Latest revision as of 09:04, 11 March 2026
The TRS Standard category is concerned with the question "Will every possible sequence of rewrites eventually stop?". In other words, does every computation defined by the rewrite rules eventually reach a normal form (a term where no rule applies)?
Category Motivation
This category evaluates tools on termination of standard first-order term rewrite systems with unrestricted rewriting which is one of the basic problems in the competition. Many of the other termination problems are either special forms of this problem, or can be reduced to this problem.
Syntax & Semantic
The syntax and the semantics of term rewrite systems are described here and here.
Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].
A term rewrite system R is terminating if there exists no infinite rewrite sequence s0 →R s1 →R s1 →R ...
Problem
Input: A 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.
- "MAYBE" (indicating that the solver cannot prove termination).
References
- [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
