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.