Dynamic Dependency Pairs for Algebraic Functional SystemsArticle
Authors: Cynthia Kop ; Femke van Raamsdonk
NULL##NULL
Cynthia Kop;Femke van Raamsdonk
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.
Volume: Volume 8, Issue 2
Secondary volumes: Selected Papers of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011)
Published on: June 19, 2012
Imported on: November 11, 2011
Keywords: Computer Science - Logic in Computer Science, F4.1,F4.2
Funding:
Source : OpenAIRE Graph- Higher-Order Termination; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 612.000.629