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.
Higher-Order Termination; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 612.000.629
Bibliographic References
5 Documents citing this article
Akihisa Yamada, 2022, Tuple Interpretations for Termination of Term Rewriting, Journal of Automated Reasoning, 66, 4, pp. 667-688, 10.1007/s10817-022-09640-4.