Dynamic Dependency Pairs for Algebraic Functional Systems
Logic in Computer Science
2015-07-01 v2
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.
Cite
@article{arxiv.1205.2519,
title = {Dynamic Dependency Pairs for Algebraic Functional Systems},
author = {Cynthia Kop and Femke van Raamsdonk},
journal= {arXiv preprint arXiv:1205.2519},
year = {2015}
}