Difference between revisions of "SRS Standard"
(Added SRS Standard Category Page) |
(Mentioned strings in the def of SRSs) |
||
| Line 7: | Line 7: | ||
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. | ||
| − | 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. | + | 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>1</sub> →<sub>R</sub> ... of 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>1</sub> →<sub>R</sub> ... of strings. | ||
Latest revision as of 16:27, 10 March 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.
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 s1 →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).
