JCKassing: Added a motivation and link to the ari format (TRS Innermost)

2026-03-11T09:08:30Z

Added a motivation and link to the ari format (TRS Innermost)

JCKassing: Added TRS Innermost Category Page

2026-03-09T17:09:10Z

Added TRS Innermost Category Page

New page

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 [[Term Rewriting | here]].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} 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 s0 →iR s1 →iR s2 →iR ...

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

[[Category:Categories]]

@@ Line 1: / Line 1: @@
 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 [[Term Rewriting | here]].
+The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]]  and [https://project-coco.uibk.ac.at/ARI/trs.php here].
 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].

TRS Innermost - Revision history

JCKassing: Added a motivation and link to the ari format (TRS Innermost)

JCKassing: Added TRS Innermost Category Page