Difference between revisions of "TRS Derivational Complexity"
(Added TRS Derivational Complexity) |
m (Small fixes) |
||
| 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. | Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows. | ||
| − | + | This helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems. | |
== Syntax & Semantic == | == Syntax & Semantic == | ||
| Line 14: | Line 14: | ||
Let |t| be the size of the term t, i.e., the number of its positions. | Let |t| be the size of the term t, i.e., the number of its positions. | ||
Then the <i>derivation height</i> dh(t) of a term t is the supremum over all →<sub>R</sub>-rewrite sequences starting with t. | Then the <i>derivation height</i> dh(t) of a term t is the supremum over all →<sub>R</sub>-rewrite sequences starting with t. | ||
| − | The <i>derivational complexity</i> of an | + | The <i>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>→<sub>R</sub> </sub>(n) = sup{m | |t| <= n, t | + | to the greatest derivation height of all objects of size at most n, i.e., dc<sub>→<sub>R</sub> </sub>(n) = sup{m | |t| <= n, dh(t) >= m}. |
| − | The goal is to find an asymptotic upper bound and lower bound on the derivational complexity | + | The goal is to find an asymptotic upper bound and lower bound on the derivational complexity dc<sub>→<sub>R</sub> </sub>(n) of a given TRS R. |
| − | |||
| − | |||
== Problem == | == Problem == | ||
| Line 30: | Line 28: | ||
* "<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>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). | * "<b>MAYBE</b>" (indicating that the solver cannot prove any complexity bound). | ||
| − | |||
| − | |||
| − | |||
[[Category:Categories]] | [[Category:Categories]] | ||
Latest revision as of 12:16, 9 June 2026
The TRS 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".
Category Motivation
Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows. This helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.
Syntax & Semantic
The syntax and the semantics of term rewrite systems are described here and 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 derivation height dh(t) of a term t is the supremum over all →R-rewrite sequences starting with t. The derivational complexity 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→R (n) = sup{m | |t| <= n, dh(t) >= m}.
The goal is to find an asymptotic upper bound and lower bound on the derivational complexity dc→R (n) of a given TRS R.
Problem
Input: A term rewrite system R.
Question: What is the asymptotic 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).
