Kop, Cynthia and van Raamsdonk, Femke - Dynamic Dependency Pairs for Algebraic Functional Systems

lmcs:668 - Logical Methods in Computer Science, June 19, 2012, Volume 8, Issue 2
Dynamic Dependency Pairs for Algebraic Functional Systems

Authors: Kop, Cynthia and van Raamsdonk, Femke

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.


Source : oai:arXiv.org:1205.2519
DOI : 10.2168/LMCS-8(2:10)2012
Volume: Volume 8, Issue 2
Published on: June 19, 2012
Submitted on: November 11, 2011
Keywords: Computer Science - Logic in Computer Science,F4.1,F4.2


Share

Consultation statistics

This page has been seen 76 times.
This article's PDF has been downloaded 60 times.