We extend the termination method using dynamic dependency pairs to higher order rewriting systems with beta as a rewrite step, also called Algebraic Functional Systems (AFSs). We introduce a variation of usable rules, and use monotone algebras to solve the constraints generated by dependency pairs. This approach differs in several respects from those dealing with higher order rewriting modulo beta (e.g. HRSs).
@InProceedings{kop_et_al:LIPIcs.RTA.2011.203, author = {Kop, Cynthia and van Raamsdonk, Femke}, title = {{Higher Order Dependency Pairs for Algebraic Functional Systems}}, booktitle = {22nd International Conference on Rewriting Techniques and Applications (RTA'11)}, pages = {203--218}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-30-9}, ISSN = {1868-8969}, year = {2011}, volume = {10}, editor = {Schmidt-Schauss, Manfred}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.203}, URN = {urn:nbn:de:0030-drops-31177}, doi = {10.4230/LIPIcs.RTA.2011.203}, annote = {Keywords: higher order rewriting, termination, dynamic dependency pairs} }
Feedback for Dagstuhl Publishing