Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity

TL;DR

This paper analyzes the derivational complexity of rewrite systems proven terminating within the dependency pair framework, establishing tight multiple recursive bounds based on the complexity of base techniques.

Contribution

It demonstrates that the derivational complexity in the dependency pair framework is tightly bounded by a multiple recursive function, given certain conditions on base techniques.

Findings

Derivational complexity is bounded by a multiple recursive function.

The upper bound on complexity is tight.

The results apply to systems proven terminating via reduction pairs, dependency graphs, or the subterm criterion.

Abstract

We study the derivational complexity of rewrite systems whose termination is provable in the dependency pair framework using the processors for reduction pairs, dependency graphs, or the subterm criterion. We show that the derivational complexity of such systems is bounded by a multiple recursive function, provided the derivational complexity induced by the employed base techniques is at most multiple recursive. Moreover we show that this upper bound is tight.