JCKassing: Added TRS Contextsensitive Page

2026-03-18T11:25:18Z

Added TRS Contextsensitive Page

New page

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".

== Category Motivation ==

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.

== Syntax & Semantic ==

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].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].
Additionally, every n-ary function symbbol f has a corresponding replacement map μ(f) which indicates which arguments of f may be evaluated.

A term rewrite system R is terminating w.r.t. μ if there exists no infinite rewrite sequence s0 →R s1 →R s1 →R ... that respects the replacement map μ.

== Problem ==

Input: A term rewrite system R and a replacement map μ

Question: Does R terminate w.r.t. μ?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R w.r.t. μ.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence w.r.t. μ.
* "MAYBE" (indicating that the solver cannot prove termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Contextsensitive - Revision history

JCKassing: Added TRS Contextsensitive Page