Higher Order Dependency Pairs for Algebraic Functional Systems
Cynthia Kop, Femke van Raamsdonk · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2011
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).