Dynamic dependency pairs for algebraic functional systems
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › fagfællebedømt
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.
Originalsprog | Engelsk |
---|---|
Artikelnummer | 10 |
Tidsskrift | Logical Methods in Computer Science |
Vol/bind | 8 |
Udgave nummer | 2 |
Antal sider | 51 |
ISSN | 1860-5974 |
Status | Udgivet - 2012 |
Eksternt udgivet | Ja |
ID: 148058703