Proving and Disproving Termination of Higher-Order Functions

Jürgen Giesl, René Thiemann, Peter Schneider-Kamp

The dependency pair technique is one of the most powerful methods
for automated termination proofs of term rewrite systems (TRSs). We
present two important extensions of this technique: First, we show how
to prove termination of higher-order functions with dependency pairs. To
this end, the dependency pair technique is extended to handle (untyped)
applicative TRSs. Second, we introduce a method to prove non-termination
in the dependency pair framework, while up to now dependency pairs were
only used to verify termination. We implemented and evaluated our results
in the automated termination prover AProVE.