Higher-order dependency pairs

TL;DR

This paper extends the dependency pair technique, originally used for first-order rewrite systems, to simply typed lambda-terms, enabling termination analysis in higher-order rewriting.

Contribution

It generalizes the dependency pair framework to higher-order systems using Tait's computability, broadening termination proof methods.

Findings

Extended dependency pairs to simply typed lambda-terms

Applied Tait's computability to higher-order rewriting

Established termination analysis for higher-order systems

Abstract

Arts and Giesl proved that the termination of a first-order rewrite system can be reduced to the study of its "dependency pairs". We extend these results to rewrite systems on simply typed lambda-terms by using Tait's computability technique.