http://termination-portal.org/mediawiki/index.php?action=history&feed=atom&title=SRS_StandardSRS Standard - Revision history2026-04-30T23:06:42ZRevision history for this page on the wikiMediaWiki 1.34.2http://termination-portal.org/mediawiki/index.php?title=SRS_Standard&diff=2118&oldid=prevJCKassing: Mentioned strings in the def of SRSs2026-03-10T16:27:46Z<p>Mentioned strings in the def of SRSs</p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 16:27, 10 March 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l7" >Line 7:</td>
<td colspan="2" class="diff-lineno">Line 7:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Strings are terms where every function symbol has arity 1, i.e., exactly one argument.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Strings are terms where every function symbol has arity 1, i.e., exactly one argument.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Formally, a string rewrite system R = {l<sub>1</sub> &rarr; r<sub>1</sub>,...,l<sub>n</sub> &rarr; r<sub>n</sub>} is a finite set of rewrite rules.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Formally, a string rewrite system R = {l<sub>1</sub> &rarr; r<sub>1</sub>,...,l<sub>n</sub> &rarr; r<sub>n</sub>} is a finite set of rewrite rules <ins class="diffchange diffchange-inline">where all occurring terms are strings</ins>.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>A string rewrite system R is terminating if there exists no infinite rewrite sequence s<sub>0</sub> &rarr;<sub>R</sub> s<sub>1</sub> &rarr;<sub>R</sub> s<sub>1</sub> &rarr;<sub>R</sub> ... of strings.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>A string rewrite system R is terminating if there exists no infinite rewrite sequence s<sub>0</sub> &rarr;<sub>R</sub> s<sub>1</sub> &rarr;<sub>R</sub> s<sub>1</sub> &rarr;<sub>R</sub> ... of strings.</div></td></tr>
</table>JCKassinghttp://termination-portal.org/mediawiki/index.php?title=SRS_Standard&diff=2116&oldid=prevJCKassing: Added SRS Standard Category Page2026-03-10T16:24:41Z<p>Added SRS Standard Category Page</p>
<p><b>New page</b></p><div>The SRS Standard category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop?". <br />
In other words, does every computation defined by the string rewrite rules eventually reach a normal form (a string where no rule applies)?<br />
<br />
== Syntax & Semantic ==<br />
<br />
The syntax and the semantics of string rewrite systems are described [[Term Rewriting | here]].<br />
Strings are terms where every function symbol has arity 1, i.e., exactly one argument.<br />
<br />
Formally, a string rewrite system R = {l<sub>1</sub> &rarr; r<sub>1</sub>,...,l<sub>n</sub> &rarr; r<sub>n</sub>} is a finite set of rewrite rules.<br />
<br />
A string rewrite system R is terminating if there exists no infinite rewrite sequence s<sub>0</sub> &rarr;<sub>R</sub> s<sub>1</sub> &rarr;<sub>R</sub> s<sub>1</sub> &rarr;<sub>R</sub> ... of strings.<br />
<br />
== Problem ==<br />
<br />
<b>Input</b>: A string rewrite system R.<br />
<br />
<b>Question</b>: Does R terminate?<br />
<br />
<b>Possible Outputs</b>: <br />
* "<b>YES</b>" followed by a termination proof, e.g., a ranking function proving termination of R.<br />
* "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence.<br />
* "<b>MAYBE</b>" (indicating that the solver cannot prove termination).<br />
<br />
<br />
[[Category:Categories]]</div>JCKassing