# A static higher-order dependency pair framework

## TL;DR

This paper extends the static dependency pair method for higher-order rewriting termination, introducing a new formalism, soundness criteria, a modular framework, and implementing it in the WANDA tool.

## Contribution

It presents a comprehensive extension of the dependency pair framework for higher-order rewriting, including new formalisms, criteria, and techniques, with an implementation in WANDA.

## Key findings

- Framework is sound and applicable to a large class of systems.
- The new formalism handles algebraic functional systems with meta-variables.
- Implementation in WANDA enables automatic termination proofs.

## Abstract

We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework. The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.