http://termination-portal.org/mediawiki/index.php?action=history&feed=atom&title=TRS_Contextsensitive
TRS Contextsensitive - Revision history
2026-06-24T00:59:43Z
Revision history for this page on the wiki
MediaWiki 1.34.2
http://termination-portal.org/mediawiki/index.php?title=TRS_Contextsensitive&diff=2201&oldid=prev
JCKassing: Small fixes
2026-06-09T12:17:24Z
<p>Small fixes</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 12:17, 9 June 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l10" >Line 10:</td>
<td colspan="2" class="diff-lineno">Line 10:</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>Formally, a term 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, see [1].</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>Formally, a term 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, see [1].</div></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>Additionally, every n-ary function <del class="diffchange diffchange-inline">symbbol </del>f has a corresponding replacement map μ(f) which indicates which arguments of f may be evaluated.</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>Additionally, every n-ary function <ins class="diffchange diffchange-inline">symbol </ins>f has a corresponding replacement map μ(f) which indicates which arguments of f may be evaluated.</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>A term rewrite system R is terminating w.r.t. μ 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><del class="diffchange diffchange-inline">1</del></sub> &rarr;<sub>R</sub> ... that respects the replacement map μ.</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>A term rewrite system R is terminating w.r.t. μ 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><ins class="diffchange diffchange-inline">2</ins></sub> &rarr;<sub>R</sub> ... that respects the replacement map μ.</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>== Problem ==</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>== Problem ==</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><b>Input</b>: A term rewrite system R and a replacement map μ</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><b>Input</b>: A term rewrite system R and a replacement map μ<ins class="diffchange diffchange-inline">.</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><b>Question</b>: Does R terminate w.r.t. μ?</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><b>Question</b>: Does R terminate w.r.t. μ?</div></td></tr>
</table>
JCKassing
http://termination-portal.org/mediawiki/index.php?title=TRS_Contextsensitive&diff=2170&oldid=prev
JCKassing: Added TRS Contextsensitive Page
2026-03-18T11:25:18Z
<p>Added TRS Contextsensitive Page</p>
<p><b>New page</b></p><div>The TRS Contextsensitive category is concerned with the question "Will every possible sequence of rewrites eventually stop if we prohibit to rewrite within certain arguments of function symbols". <br />
<br />
== Category Motivation ==<br />
<br />
Context-sensitive rewriting is a restriction of first-order term rewriting which is used, e.g., to model different evaluation strategies for the analysis of functional programming languages.<br />
<br />
== Syntax & Semantic ==<br />
<br />
The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and specifically for context-sensitive rewriting [https://project-coco.uibk.ac.at/ARI/cstrs.php here].<br />
<br />
Formally, a term 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, see [1].<br />
Additionally, every n-ary function symbbol f has a corresponding replacement map μ(f) which indicates which arguments of f may be evaluated.<br />
<br />
A term rewrite system R is terminating w.r.t. μ 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> ... that respects the replacement map μ.<br />
<br />
== Problem ==<br />
<br />
<b>Input</b>: A term rewrite system R and a replacement map μ<br />
<br />
<b>Question</b>: Does R terminate w.r.t. μ?<br />
<br />
<b>Possible Outputs</b>: <br />
* "<b>YES</b>" followed by a termination proof, e.g., a ranking function proving termination of R w.r.t. μ.<br />
* "<b>NO</b>" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence w.r.t. μ.<br />
* "<b>MAYBE</b>" (indicating that the solver cannot prove termination).<br />
<br />
<br />
== References ==<br />
<br />
* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.<br />
<br />
<br />
[[Category:Categories]]</div>
JCKassing