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

2026-03-11T09:11:45Z

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

JCKassing: Added TRS Outermost Category Page

2026-03-09T17:11:44Z

Added TRS Outermost Category Page

New page

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

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

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

[[Category:Categories]]

@@ Line 1: / Line 1: @@
 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 [[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 Outermost - Revision history

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

JCKassing: Added TRS Outermost Category Page