TRS Innermost

The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?". In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions eventually reach a normal form (a term where no rule applies)?

Syntax & Semantic

The syntax and the semantics of term rewrite systems are described here.

Formally, a term rewrite system R = {l₁ → r₁,...,l_n → r_n} is a finite set of rewrite rules, see [1].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R. A term rewrite system R is innermost terminating if there exists no infinite rewrite sequence s₀ →ⁱ_R s₁ →ⁱ_R s₂ →ⁱ_R ...

Problem

Input: A term rewrite system R.

Question: Does R innermost terminate?

Possible Outputs:

• "YES" followed by a termination proof, e.g., a ranking function proving innermost termination of R.
• "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost rewrite sequence.
• "MAYBE" (indicating that the solver cannot prove termination).

References

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