Relative Match-Bounds for Complexity Analysis


As soon as we have established the termination of a given TRS, it is
natural to analyze its complexity in order to determine the amount of
resources that are necessary to perform computations. In the area of term
rewriting the length of derivations provides a suitable measurement for the
complexity of rewrite systems, as proposed by Hofbauer and Lautemann. To
show feasible upper complexity bounds, currently only a few techniques are
known. Typically, termination criteria are restricted such that a
polynomial complexity of the underlying TRS can be inferred. One of the
most powerful methods to establish (linear) complexity bounds is the
match-bound technique introduced by Geser, Hofbauer, and Waldmann. Its
ability to prove termination of an arbitrary regular set of ground terms
makes it one of the most powerful methods that can be used to establish
(linear) runtime complexity. In this talk we show how the match-bound
technique can be successfully integrated into the so-called complexity
framework, a powerful and modular approach for complexity analysis based on
relative termination.