{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:55Z","timestamp":1753889755841,"version":"3.41.2"},"reference-count":38,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,6,19]],"date-time":"2012-06-19T00:00:00Z","timestamp":1340064000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Netherlands Organisation for Scientific Research","doi-asserted-by":"crossref","award":["2300137663"],"award-info":[{"award-number":["2300137663"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We extend the higher-order termination method of dynamic dependency pairs to\nAlgebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms\nwith algebraic reduction and separate {\\beta}-steps are considered. For\nleft-linear AFSs, the method is shown to be complete. For so-called local AFSs\nwe define a variation of usable rules and an extension of argument filterings.\nAll these techniques have been implemented in the higher-order termination tool\nWANDA.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:10)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":6,"title":["Dynamic Dependency Pairs for Algebraic Functional Systems"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Cynthia","family":"Kop","sequence":"first","affiliation":[]},{"given":"Femke","family":"van Raamsdonk","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,6,19]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"T. Aoto and Y. Yamada. Dependency pairs for simply typed term rewriting. In J. Giesl, editor,Proceedings of RTA 2005, volume 3467 ofLNCS, pages 120-134, Nara, Japan, 2005. Springer.","key":"10.2168\/LMCS-8(2:10)2012_aot:yam:05:1","DOI":"10.1007\/978-3-540-32033-3_10"},{"issue":"1-2","key":"10.2168\/LMCS-8(2:10)2012_art:gie:00:1","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts and J. Giesl","year":"2000","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"F. Blanqui, J.-P. Jouannaud, and A. Rubio. The computability path ordering: The end of a quest. InCSL 2008, volume 5213 ofLNCS, pages 1-14, Bertinoro, Italy, 2008. Springer.","key":"10.2168\/LMCS-8(2:10)2012_bla:jou:rub:08:1","DOI":"10.1007\/978-3-540-87531-4_1"},{"unstructured":"H.J.S. Bruggink.Equivalence of Reductions in Higher-Order Rewriting. PhD thesis, Utrecht University, 2008.","key":"10.2168\/LMCS-8(2:10)2012_bru:08"},{"key":"10.2168\/LMCS-8(2:10)2012_cag:hin:98:1","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/S0304-3975(97)00250-8","volume":"198","author":"N. Cagman and Roger Hindley","year":"1998","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.2168\/LMCS-8(2:10)2012_fuh:gie:par:sch:swi:11","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s10817-010-9215-9","volume":"47","author":"C. Fuhs, J. Giesl, M. Parting, P. Schnei","year":"2011","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"C. Fuhs and C. Kop. Harnessing first order termination provers using higher order dependency pairs. In C. Tinelli and V. Sofronie-Stokkermans, editors,Frontiers of Combining Systems, volume 6989 ofLNCS, pages 147-162. Springer, 2011.","key":"10.2168\/LMCS-8(2:10)2012_fuh:kop:11:1","DOI":"10.1007\/978-3-642-24364-6_11"},{"unstructured":"C. Fuhs and C. Kop. Polynomial interpretations for higher-order rewriting. In A. Tiwari, editor,Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA '12), volume 15 of LIPIcs, pages 176-192. Dagstuhl, 2012.","key":"10.2168\/LMCS-8(2:10)2012_fuh:kop:12:1"},{"doi-asserted-by":"crossref","unstructured":"J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. InProceedings of LPAR 2004, volume 3452 ofLNCS, pages 301-331. Springer, 2005.","key":"10.2168\/LMCS-8(2:10)2012_gie:thi:sch:05:2","DOI":"10.1007\/978-3-540-32275-7_21"},{"issue":"3","key":"10.2168\/LMCS-8(2:10)2012_gie:thi:sch:fal:06","first-page":"155","volume":"37","author":"J. Giesl, R. Thiemann, P. Schneider-Kamp","year":"2006","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(2:10)2012_gra:95:1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1995-24121","volume":"24","author":"B. Gramlich","year":"1995","journal-title":"Fundamenta Informaticae"},{"doi-asserted-by":"crossref","unstructured":"N. Hirokawa and A. Middeldorp. Dependency pairs revisited. InProceedings of RTA 2004, volume 3091 ofLNCS, pages 249-268. Springer, 2004.","key":"10.2168\/LMCS-8(2:10)2012_hir:mid:04:1","DOI":"10.1007\/978-3-540-25979-4_18"},{"issue":"1-2","key":"10.2168\/LMCS-8(2:10)2012_hir:mid:05:1","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1016\/j.ic.2004.10.004","volume":"199","author":"N. Hirokawa and A. Middeldorp","year":"2005","journal-title":"Information and Computation"},{"issue":"4","key":"10.2168\/LMCS-8(2:10)2012_hir:mid:07:1","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1016\/j.ic.2006.08.010","volume":"205","author":"N. Hirokawa and A. Middeldorp","year":"2007","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"N. Hirokawa, A. Middeldorp, and H. Zankl. Uncurrying for termination. InLPAR 2008, volume 5330 ofLNAI, pages 667-681, Doha, 2008. Springer-Verlag.","key":"10.2168\/LMCS-8(2:10)2012_hir:mid:zan:08","DOI":"10.1007\/978-3-540-89439-1_46"},{"unstructured":"G. Huet and D.C. Oppen. Equations and rewrite rules: a survey. In R.V. Book, editor,Formal Language Theory: Perspectives and Open Problems, pages 349-405. Academic Press, London, 1980.","key":"10.2168\/LMCS-8(2:10)2012_hue:opp:80:1"},{"unstructured":"J.-P. Jouannaud and M. Okada. A computation model for executable higher-order algebraic specification languages. InLICS 1991, pages 350-361, Amsterdam, The Netherlands, 1991. IEEE Computer Society Press.","key":"10.2168\/LMCS-8(2:10)2012_jou:oka:91:1"},{"unstructured":"J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. InLICS 1999, pages 402-411, Trento, Italy, 1999.","key":"10.2168\/LMCS-8(2:10)2012_jou:rub:99:1"},{"unstructured":"C. Kop. Wanda. http:\/\/www.few.vu.nl\/ kop\/code.html.","key":"10.2168\/LMCS-8(2:10)2012_kop:10:1"},{"doi-asserted-by":"crossref","unstructured":"C. Kop. Simplifying algebraic functional systems. In F. Winkler, editor,Proceedings of CAI 2011, volume 6742 ofLNCS, pages 201-215. Springer, 2011.","key":"10.2168\/LMCS-8(2:10)2012_kop:11:1","DOI":"10.1007\/978-3-642-21493-6_13"},{"doi-asserted-by":"crossref","unstructured":"C. Kop and F. van Raamsdonk. A higher-order iterative path ordering. In I. Cervesato, H. Veith, and A. Voronkov, editors,Proceedings of LPAR 2008, volume 5330 ofLNAI, pages 697-711. Springer, 2008.","key":"10.2168\/LMCS-8(2:10)2012_kop:raa:08:1","DOI":"10.1007\/978-3-540-89439-1_48"},{"unstructured":"C. Kop and F. van Raamsdonk. Higher-order dependency pairs with argument filterings. InProceedings of WST 2010, Edinburgh, UK, 2010. http:\/\/www.few.vu.nl\/ kop\/wst10.pdf.","key":"10.2168\/LMCS-8(2:10)2012_kop:raa:10:1"},{"unstructured":"C. Kop and F. van Raamsdonk. Higher order dependency pairs for algebraic functional systems. In M. Schmidt-Schau\u00df, editor,Proceedings of RTA 2011, volume 10 ofLIPIcs, pages 203-218. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2011.","key":"10.2168\/LMCS-8(2:10)2012_kop:raa:11:1"},{"issue":"SIG 7 PRO11","key":"10.2168\/LMCS-8(2:10)2012_kus:01:1","first-page":"35","volume":"42","author":"K. Kusakari","year":"2001","journal-title":"IPSJ Transactions on Programming"},{"issue":"10","key":"10.2168\/LMCS-8(2:10)2012_kus:iso:sak:bla:09:1","first-page":"2007","volume":"92","author":"K. Kusakari, Y. Isogai, M. Sakai, and F.","year":"2009","journal-title":"IEICE Transactions on Information and Systems 92(10):2007-2015, 2009"},{"issue":"5","key":"10.2168\/LMCS-8(2:10)2012_kus:sak:07:1","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/s00200-007-0046-9","volume":"18","author":"K. Kusakari and M. Sakai","year":"2007","journal-title":"AAECC"},{"issue":"92-D","key":"10.2168\/LMCS-8(2:10)2012_kus:sak:09:1","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1587\/transinf.E92.D.235","volume":"2","author":"K. Kusakari and M. Sakai","year":"2009","journal-title":"IEICE Transactions"},{"unstructured":"P.-A. Melli\u00e8s.Description Abstraite des Syst\u00e8mes de R\u00e9\u00e9criture. PhD thesis, Universit\u00e9 Paris VII, 1996.","key":"10.2168\/LMCS-8(2:10)2012_mel:96"},{"unstructured":"T. Nipkow. Higher-order critical pairs. InLICS 1991, pages 342-349, Amsterdam, The Netherlands, 1991.","key":"10.2168\/LMCS-8(2:10)2012_nip:91:1"},{"key":"10.2168\/LMCS-8(2:10)2012_oos:97:1","first-page":"308","volume":"1232","author":"V. van Oostrom","year":"1997","journal-title":"LNCS"},{"unstructured":"J.C. van de Pol.Termination of Higher-order Rerwite Systems. PhD thesis, University of Utrecht, 1996.","key":"10.2168\/LMCS-8(2:10)2012_pol:96:1"},{"doi-asserted-by":"crossref","unstructured":"J.C. van de Pol and H. Schwichtenberg. Strict functionals for termination proofs. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors,Typed Lambda Calculi and Applications, volume 902 ofLecture Notes in Computer Science, pages 350-364. Springer Berlin \/ Heidelberg, 1995.","key":"10.2168\/LMCS-8(2:10)2012_pol:sch:95:1","DOI":"10.1007\/BFb0014064"},{"doi-asserted-by":"crossref","unstructured":"M. Sakai and K. Kusakari. On dependency pair method for proving termination of higher-order rewrite systems.IEICE Transactions on Information and Systems, E88-D(3):583-593, 2005.","key":"10.2168\/LMCS-8(2:10)2012_sak:kus:05:1","DOI":"10.1093\/ietisy\/e88-d.3.583"},{"unstructured":"M. Sakai, Y. Watanabe, and T. Sakabe. An extension of the dependency pair method for proving termination of higher-order rewrite systems.IEICE Transactions on Information and Systems, E84-D(8):1025-1032, 2001.","key":"10.2168\/LMCS-8(2:10)2012_sak:wat:sak:01"},{"issue":"2","key":"10.2168\/LMCS-8(2:10)2012_suz:kus:bla:11","first-page":"1","volume":"4","author":"S. Suzuki, K. Kusakari, and F. Blanqui","year":"2011","journal-title":"IPSJ Transactions on Programming"},{"unstructured":"Terese.Term Rewriting Systems, volume 55 ofCambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.","key":"10.2168\/LMCS-8(2:10)2012_ter:03"},{"unstructured":"Wiki. Termination portal. http:\/\/www.termination-portal.org\/.","key":"10.2168\/LMCS-8(2:10)2012_termcomp"},{"key":"10.2168\/LMCS-8(2:10)2012_zan:94:1","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H. Zantema","year":"1994","journal-title":"Journal of Symbolic Computation"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/668\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/668\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:53:34Z","timestamp":1681242814000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,19]]},"references-count":38,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:10)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1205.2519","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1205.2519","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,6,19]]},"article-number":"668"}}