Difference between revisions of "TRS Equational"
From Termination-Portal.org
Jump to navigationJump to search (Added TRS Equational Page) |
(Small fixes) |
||
| Line 1: | Line 1: | ||
| − | The TRS Equational category is concerned with the question "Will every possible sequence of | + | The TRS Equational category is concerned with the question "Will every possible sequence of rewrite steps on equivalence classes terminate?". |
== Syntax & Semantic == | == Syntax & Semantic == | ||
| − | Formally, an equational term rewrite system is a set R = {l<sub>1</sub> → r<sub>1</sub>,...,l<sub>n</sub> → r<sub>n</sub>} of finitely rewrite rules together a set S = {a<sub>1</sub> = b<sub>1</sub>,...,a<sub> | + | Formally, an equational term rewrite system is a set R = {l<sub>1</sub> → r<sub>1</sub>,...,l<sub>n</sub> → r<sub>n</sub>} of finitely many rewrite rules together with a set S = {a<sub>1</sub> = b<sub>1</sub>,...,a<sub>m</sub> = b<sub>m</sub>} of finitely many term equations, called a ''theory''. |
An equational 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 where we can use the equations from S mid rewriting. | An equational 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 where we can use the equations from S mid rewriting. | ||
| Line 18: | Line 18: | ||
== Problem == | == Problem == | ||
| − | <b>Input</b>: | + | <b>Input</b>: An equational term rewrite system R/S. |
<b>Question</b>: Does R/S terminate? | <b>Question</b>: Does R/S terminate? | ||
| Line 26: | Line 26: | ||
* "<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 of R/S). | * "<b>MAYBE</b>" (indicating that the solver cannot prove termination of R/S). | ||
| − | |||
| − | |||
| − | |||
| − | |||
[[Category:Categories]] | [[Category:Categories]] | ||
Latest revision as of 12:15, 9 June 2026
The TRS Equational category is concerned with the question "Will every possible sequence of rewrite steps on equivalence classes terminate?".
Syntax & Semantic
Formally, an equational term rewrite system is a set R = {l1 → r1,...,ln → rn} of finitely many rewrite rules together with a set S = {a1 = b1,...,am = bm} of finitely many term equations, called a theory.
An equational 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 where we can use the equations from S mid rewriting.
Here, a theory may be added to declarations of function symbols.
fun ::= ( fun identifier number theory? ) theory ::= :theory [A | C | AC]
- full rewriting modulo associativity / commutativity / associativity and commutativity
Problem
Input: An equational 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).
