The Derivational Complexity Induced by the Dependency Pair Method

TL;DR

This paper analyzes the derivational complexity of the dependency pair method in term rewriting, showing it remains primitive recursive relative to the base techniques used, and matches traditional termination orders in complexity.

Contribution

It provides upper bounds on the derivational complexity induced by the dependency pair method, demonstrating its complexity is primitive recursive relative to the base methods.

Findings

Dependency pair method's complexity is primitive recursive in base techniques.

Complexity matches that of traditional termination orders like KBO, LPO, MPO.

Enhanced with refinements, the method's complexity remains bounded.

Abstract

We study the derivational complexity induced by the dependency pair method, enhanced with standard refinements. We obtain upper bounds on the derivational complexity induced by the dependency pair method in terms of the derivational complexity of the base techniques employed. In particular we show that the derivational complexity induced by the dependency pair method based on some direct technique, possibly refined by argument filtering, the usable rules criterion, or dependency graphs, is primitive recursive in the derivational complexity induced by the direct method. This implies that the derivational complexity induced by a standard application of the dependency pair method based on traditional termination orders like KBO, LPO, and MPO is exactly the same as if those orders were applied as the only termination technique.