Difference between revisions of "SRS Standard"
(Mentioned strings in the def of SRSs) |
(Small fixes) |
||
| Line 6: | Line 6: | ||
The syntax and the semantics of string rewrite systems are described [[Term Rewriting | here]]. | The syntax and the semantics of string rewrite systems are described [[Term Rewriting | here]]. | ||
Strings are terms where every function symbol has arity 1, i.e., exactly one argument. | Strings are terms where every function symbol has arity 1, i.e., exactly one argument. | ||
| + | Additionally, the same variable appears on both the left and right sides of each rule. | ||
Formally, a string 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 where all occurring terms are strings. | Formally, a string 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 where all occurring terms are strings. | ||
| − | A string rewrite system R is terminating if there exists no infinite rewrite sequence s<sub>0</sub> →<sub>R</sub> s<sub>1</sub> →<sub>R</sub> s<sub> | + | A string rewrite system R is terminating if there exists no infinite rewrite sequence s<sub>0</sub> →<sub>R</sub> s<sub>1</sub> →<sub>R</sub> s<sub>2</sub> →<sub>R</sub> ... of strings. |
== Problem == | == Problem == | ||
Latest revision as of 12:21, 9 June 2026
The SRS Standard category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop?". In other words, does every computation defined by the string rewrite rules eventually reach a normal form (a string where no rule applies)?
Syntax & Semantic
The syntax and the semantics of string rewrite systems are described here. Strings are terms where every function symbol has arity 1, i.e., exactly one argument. Additionally, the same variable appears on both the left and right sides of each rule.
Formally, a string rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules where all occurring terms are strings.
A string rewrite system R is terminating if there exists no infinite rewrite sequence s0 →R s1 →R s2 →R ... of strings.
Problem
Input: A string 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).
