TRS Contextsensitive

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 here and specifically for context-sensitive rewriting here.

Formally, a term rewrite system R = {l₁ → r₁,...,l_n → r_n} 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 s₀ →_R s₁ →_R s₁ →_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.