TRS Outermost

The TRS Outermost category is concerned with the question "Will every outermost rewrite sequence eventually stop?". In other words, does every computation defined by the rewrite rules that only evaluates outermost 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 outermost rewrite step is a rewrite step that rewrites an outermost reducible expression, i.e., there is no other redex at a position above the redex we want to rewrite. A term rewrite system R is outermost terminating if there exists no infinite rewrite sequence s₀ →^o_R s₁ →^o_R s₂ →^o_R ...

Problem

Input: A term rewrite system R.

Question: Does R outermost terminate?

Possible Outputs:

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

References

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