Inferring Lower Bounds for Runtime Complexity
Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, and
Thomas Ströder
We present the first approach to deduce lower bounds for innermost runtime
complexity of term rewrite systems (TRSs) automatically. Inferring lower
runtime bounds is useful to detect bugs and to complement existing
techniques that compute upper complexity bounds. The key idea of our
approach is to generate suitable families of rewrite sequences of a TRS
and to find a relation between the length of such a rewrite sequence and
the size of the first term in the sequence. We implemented our approach
in the tool AProVE and evaluated it by extensive experiments.