Difference between revisions of "TRS Innermost"
(Added TRS Innermost Category Page) |
(Small fixes) |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?". | The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?". | ||
In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions eventually reach a normal form (a term where no rule applies)? | In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions eventually reach a normal form (a term where no rule applies)? | ||
| + | |||
| + | == Category Motivation == | ||
| + | |||
| + | This category investigates termination under the innermost rewriting strategy, roughly corresponding to a call-by-value evaluation strategy in programming languages, | ||
| + | which is one of the most used evaluation strategies. | ||
== 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]. | ||
| Line 20: | Line 25: | ||
* "<b>YES</b>" followed by a termination proof, e.g., a ranking function proving innermost termination of R. | * "<b>YES</b>" followed by a termination proof, e.g., a ranking function proving innermost termination of R. | ||
* "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost rewrite sequence. | * "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost rewrite sequence. | ||
| − | * "<b>MAYBE</b>" (indicating that the solver cannot prove termination). | + | * "<b>MAYBE</b>" (indicating that the solver cannot prove innermost termination). |
Latest revision as of 12:14, 9 June 2026
The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?". In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions eventually reach a normal form (a term where no rule applies)?
Category Motivation
This category investigates termination under the innermost rewriting strategy, roughly corresponding to a call-by-value evaluation strategy in programming languages, which is one of the most used evaluation strategies.
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].
An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R. A term rewrite system R is innermost terminating if there exists no infinite rewrite sequence s0 →iR s1 →iR s2 →iR ...
Problem
Input: A term rewrite system R.
Question: Does R innermost terminate?
Possible Outputs:
- "YES" followed by a termination proof, e.g., a ranking function proving innermost termination of R.
- "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost rewrite sequence.
- "MAYBE" (indicating that the solver cannot prove innermost termination).
References
- [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
