JCKassing: Small fixes

2026-06-09T12:13:18Z

Small fixes

JCKassing: Added TRS Innermost Derivational Complexity

2026-03-19T10:26:59Z

Added TRS Innermost Derivational Complexity

New page

The TRS Innermost Derivational Complexity category is concerned with the question "What is the time complexity of a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.
his helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

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 = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height dh(t) of a term t is the supremum over all innermost →iR-rewrite sequences starting with t.
The innermost derivational complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all objects of size at most n, i.e., dc→R (n) = sup{m | |t| <= n, t →iRn s}.

The goal is to find an asymptotic upper bound and lower bound on the derivational complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n^2), O(n^3), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

@@ Line 4: / Line 4: @@
 Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.
-his helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.
+This helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.
 Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
@@ Line 16: / Line 16: @@
 Let |t| be the size of the term t, i.e., the number of its positions.
-Then the <i>innermost derivation height</i> dh(t) of a term t is the supremum over all innermost &rarr;<sup>i</sup><sub>R</sub>-rewrite sequences starting with t.
+Then the <i>innermost derivation height</i> idh(t) of a term t is the supremum over all innermost &rarr;<sup>i</sup><sub>R</sub>-rewrite sequences starting with t.
-The <i>innermost derivational complexity</i> of an ARS is a function that maps every natural number n
+The <i>innermost derivational complexity</i> of an TRS is a function that maps every natural number n
-to the greatest derivation height of all objects of size at most n, i.e., dc<sub>&rarr;<sub>R</sub> </sub>(n) = sup{m | |t| <= n, t &rarr;<sup>i</sup><sub>R</sub><sup>n</sup> s}.
+to the greatest derivation height of all objects of size at most n, i.e., idc<sub>&rarr;<sub>R</sub> </sub>(n) = sup{m | |t| <= n, idh(t) >= m}.
-The goal is to find an asymptotic upper bound and lower bound on the derivational complexity of a given TRS R.
+The goal is to find an asymptotic upper bound and lower bound on the innermost derivational complexity idc<sub>&rarr;<sub>R</sub> </sub>(n) of a given TRS R.
 == Problem ==
@@ Line 33: / Line 31: @@
 * "<b>WORST_CASE(f(n),g(n))</b>" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
 * "<b>MAYBE</b>" (indicating that the solver cannot prove any complexity bound).
 [[Category:Categories]]

TRS Innermost Derivational Complexity - Revision history

JCKassing: Small fixes

JCKassing: Added TRS Innermost Derivational Complexity