Difference between revisions of "TRS Innermost Runtime Complexity"
(Added TRS Innermost Runtime Complexity) |
(Small fixes) |
||
| Line 18: | Line 18: | ||
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>innermost derivation height</i> | + | Then the <i>innermost derivation height</i> idh(t) of a term t is the supremum over all →<sup>i</sup><sub>R</sub>-rewrite sequences starting with t. |
We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms) | We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms) | ||
| Line 25: | Line 25: | ||
The set of all basic terms is denoted T<sub>B</sub>. | The set of all basic terms is denoted T<sub>B</sub>. | ||
| − | The <i>innermost runtime complexity</i> of an | + | The <i>innermost runtime complexity</i> of an TRS is a function that maps every natural number n |
| − | to the greatest derivation height of all basic terms of size at most n, i.e., | + | to the greatest derivation height of all basic terms of size at most n, i.e., irc<sub>→<sub>R</sub> </sub>(n) = sup{m | t ∈ T<sub>B</sub>, |t| <= n, idh(t) >= m}. |
| − | The goal is to find an asymptotic upper bound and lower bound on the innermost runtime complexity | + | The goal is to find an asymptotic upper bound and lower bound on the innermost runtime complexity irc<sub>→<sub>R</sub> </sub>(n) of a given TRS R. |
| − | |||
| − | |||
== Problem == | == Problem == | ||
| Line 41: | Line 39: | ||
* "<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:11, 9 June 2026
The TRS Innermost Runtime Complexity category is concerned with the question "What is the time complexity of algorithms represented by 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.
While derivational complexity considers arbitrary initial terms, runtime complexity restricts the initial terms to model an algorithm that is given fixed data as arguments, which relates to the intuitive definition of time complexity.
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 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 innermost derivation height idh(t) of a term t is the supremum over all →iR-rewrite sequences starting with t.
We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms) and constructor symbols (the remaining function symbols, the data). A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data. The set of all basic terms is denoted TB.
The innermost runtime complexity of an TRS is a function that maps every natural number n to the greatest derivation height of all basic terms of size at most n, i.e., irc→R (n) = sup{m | t ∈ TB, |t| <= n, idh(t) >= m}.
The goal is to find an asymptotic upper bound and lower bound on the innermost runtime complexity irc→R (n) of a given TRS R.
Problem
Input: A term rewrite system R.
Question: What is the asymptotic innermost runtime 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).
