TRS Parallel Innermost Derivational Complexity

The TRS Innermost Derivational 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.

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

TODO: clarify the difference to [TRS Innermost Derivational Complexity | TRS Innermost Derivational Complexity]!

The syntax and the semantics of term rewrite systems are described here and here.

Formally, a term rewrite system R = {l₁ → r₁,...,l_n → r_n} 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 →ⁱ_R-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 T_B.

The innermost derivational complexity of an ARS 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., dc_→R (n) = sup{m | t ∈ T_B, |t| <= n, t →ⁱ_Rⁿ s}.

The goal is to find an asymptotic upper bound and lower bound on the innermost derivational complexity of a given TRS R. Possible complexity classes are O(1), O(n), O(n²), ..., 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).