Dynamic Dependency Pairs for Algebraic Functional Systems
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 loc...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/668/pdf |
| _version_ | 1827322952084881408 |
|---|---|
| author | Cynthia Kop Femke van Raamsdonk |
| author_facet | Cynthia Kop Femke van Raamsdonk |
| author_sort | Cynthia Kop |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:59Z |
| format | Article |
| id | doaj.art-c5401532772d46d1b1314b89abfbd1dd |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:59Z |
| publishDate | 2012-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-c5401532772d46d1b1314b89abfbd1dd2024-03-08T09:27:56ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-06-01Volume 8, Issue 210.2168/LMCS-8(2:10)2012668Dynamic Dependency Pairs for Algebraic Functional SystemsCynthia KopFemke van RaamsdonkWe 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.https://lmcs.episciences.org/668/pdfcomputer science - logic in computer sciencef4.1,f4.2 |
| spellingShingle | Cynthia Kop Femke van Raamsdonk Dynamic Dependency Pairs for Algebraic Functional Systems Logical Methods in Computer Science computer science - logic in computer science f4.1,f4.2 |
| title | Dynamic Dependency Pairs for Algebraic Functional Systems |
| title_full | Dynamic Dependency Pairs for Algebraic Functional Systems |
| title_fullStr | Dynamic Dependency Pairs for Algebraic Functional Systems |
| title_full_unstemmed | Dynamic Dependency Pairs for Algebraic Functional Systems |
| title_short | Dynamic Dependency Pairs for Algebraic Functional Systems |
| title_sort | dynamic dependency pairs for algebraic functional systems |
| topic | computer science - logic in computer science f4.1,f4.2 |
| url | https://lmcs.episciences.org/668/pdf |
| work_keys_str_mv | AT cynthiakop dynamicdependencypairsforalgebraicfunctionalsystems AT femkevanraamsdonk dynamicdependencypairsforalgebraicfunctionalsystems |