Dynamic Dependency Pairs for Algebraic Functional Systems

TL;DR

This paper extends the dynamic dependency pairs method to Algebraic Functional Systems, providing a complete approach for left-linear AFSs and practical techniques for local AFSs, implemented in the WANDA tool.

Contribution

It introduces a novel extension of dynamic dependency pairs to AFSs, including new techniques for local AFSs, and implements these in the WANDA termination tool.

Findings

Method is complete for left-linear AFSs.

New techniques for local AFSs improve termination analysis.

Implementation in WANDA demonstrates practical applicability.

Abstract

We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reduction and separate {\beta}-steps are considered. For left-linear AFSs, the method is shown to be complete. For so-called local AFSs we define a variation of usable rules and an extension of argument filterings. All these techniques have been implemented in the higher-order termination tool WANDA.