Dynamic Dependency Pairs for Algebraic Functional Systems

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 β-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.

References in corpus (1)

• Polynomial Interpretations for Higher-Order Rewriting

Cited by in corpus (5)

• Polynomial Interpretations for Higher-Order Rewriting
• First-Order Formative Rules
• Polymorphic Higher-order Termination
• A static higher-order dependency pair framework
• Templates in Rewriting Induction