"Inferring Lower Bounds for Runtime Complexity" - Experiments and Proofs

There exist numerous methods to infer upper bounds for the runtime complexity of term rewrite systems (TRSs). In the paper "Inferring Lower Bounds for Runtime Complexity", we present the first automatic technique to infer lower bounds for the innermost runtime complexity of TRSs. While upper complexity bounds help to prove the absence of bugs that worsen the performance of programs, lower bounds can be used to find such bugs. Moreover, in combination with existing methods to deduce upper bounds, our technique can prove tight complexity results. For each lower bound found by our implementation, it also returns a witness, i.e., a rewrite lemma whose left-hand side represents a family of terms that leads to the reported runtime.

A full version of our paper including all proofs is available here.


Implementation in AProVE

We integrated our new technique in the termination and complexity analyzer AProVE , which is one of the most powerful termination and complexity tools for TRSs. It can be accessed via a custom web interface.


Settings

Since there are no other tools yet that infer lower bounds for the innermost runtime complexity of TRSs automatically, to evaluate the power of our approach, we compared the results of our implementation with the upper bounds for innermost runtime complexity that are computed by the tools AProVE and TcT. These were the most powerful tools for inferring upper innermost runtime complexity bounds for TRSs at the most recent Termination Competition 2014. Similar to the implementation of our technique for lower bounds, the upper bounds computed by these tools are also asymptotic bounds. As suggested by the authors of TcT, we used its version 2.0.2. All tools were run on a 3.07 GHz 8-Core Intel i7 950 Debian Linux machine with a timeout of 300 seconds for each example.


Examples

We ran the tools on 808 TRSs from the category "Runtime Complexity - Innermost Rewriting" of the Termination Problem Data Base (TPDB 9.0.2), which is the collection of examples used at the Termination Competition 2014. Here, we omitted 60 TRSs which contain rules with extra variables on the right-hand side and 58 TRSs with relative rules, since such rules are not allowed in classical term rewriting. Moreover, we disregard 87 examples with infinite innermost rewrite sequences starting in basic terms. To identify them, we adapted existing techniques for proving innermost non-termination in our tool AProVE such that they only consider innermost rewrite sequences starting with basic terms. Finally, we also disregard 51 examples where AProVE or TcT were able to prove constant innermost runtime complexity. The disregarded examples are marked in grey in the table below.


Experiments & Discussion

To assess the quality of the inferred lower bounds, the table below compares them with the minimum upper bound computed by AProVE or TcT. Here, irc stands for the innermost runtime complexity function, mapping a natural number n to the length of the longest evaluation sequence starting with a basic term of at most size n.

irc(n) Ω(1) Ω(n) Ω(n2) Ω(n3) Ω(n>3) Ω(2n) Ω(3n) Ω(ω)
Ο(1) (51) -- -- -- -- -- -- --
Ο(n) 65 201 -- -- -- -- -- --
Ο(n2) 5 57 17 -- -- -- -- --
Ο(n3) -- 10 3 8 -- -- -- --
Ο(n>3) 3 3 1 -- -- -- -- --
Ο(2n) -- -- -- -- -- -- -- --
Ο(3n) -- -- -- -- -- -- -- --
Ο(ω) 78 293 47 6 -- 10 1 (87)

Considering all 808 examples, the average runtime of our implementation was 22.5 seconds, but in most cases, it was much faster. In 694 cases, the analysis finshed within 5 seconds. The table above shows that our implementation infers non-trivial lower bounds for 657 of the 808 analyzed TRSs (i.e., for 81% of these examples). Note that non-trivial upper bounds can only be inferred for 373 (i.e., for 46%) of these examples. On the other hand, non-trivial upper bounds exist for at least 83% of all examples, since AProVE is able to prove innermost termination of 670 of the 808 analyzed TRSs. So although this is the first paper on automated inference of lower runtime bounds, the applicability of our approach already exceeds the applicability of the techniques for upper bounds, which have been developed for several years.

By adding up the numbers in the diagonal of the table, one can see that tight complexity bounds were proven for 226 TRSs (i.e., these are the examples where the inferred asymptotic upper and lower bound are the same). There are just 74 examples where non-trivial upper and lower bounds are inferred that do not coincide. For 60 of them, the lower bound just differs from the corresponding upper bound by the factor n. Of course, when the inferred lower and upper bound are different, in general it is not clear whether this imprecision is due to the lower or due to the upper bound.

To simplify the arithmetic constraints arising during the proofs of conjectures, in some cases our implementation uses a heuristic to instantiate non-induction variables before the start of the proof. For instance, for the conjecture f(γNats(x+n)) →* from Sect. 7 of our paper, it would instantiate the non-induction variable x by 1 and result in the rewrite lemma f(γNats(1+n)) →Ω(n).

Here you can find a table presenting all individual examples and the results of the tools on them. Clicking on the proven bound opens the corresponding proof. Note that even if no non-trivial lower bound was proved, all speculated rewrite conjectures can be displayed in this way. To see the example, you can click on its name. Then, you can copy the example to our web interface to analyze it.