AIB 2017-02: Analyzing Runtime Complexity via Innermost Runtime Complexity

[Jera Hensel]

The following technical report is available from
http://aib.informatik.rwth-aachen.de:

Analyzing Runtime Complexity via Innermost Runtime Complexity
Florian Frohn and Jürgen Giesl
AIB 2017-02

There exist powerful techniques to infer upper bounds on the innermost
runtime complexity of term rewrite systems (TRSs), i.e., on the lengths
of rewrite sequences that follow an innermost evaluation strategy.
However, the techniques to analyze the (full) runtime complexity of TRSs
are substantially weaker. In this paper, we present a sufficient
criterion to ensure that the runtime complexity of a TRS coincides with
its innermost runtime complexity. This criterion can easily be checked
automatically and it allows us to use all techniques and tools for
innermost runtime complexity in order to analyze (full) runtime
complexity. By extensive experiments with an implementation of our
results in the tool AProVE, we show that this improves the state of the
art of automated complexity analysis significantly.