The Higher-Order Dependency Pair Framework

Cynthia Kop

Proceedings of the 7th International Workshop on Higher-Order Rewriting (HOR 2014), 2014.


In recent years, two different dependency pair approaches have been introduced: the dynamic and static styles. The static style is based on a computability argument, and is limited to plain function-passing systems. The dynamic style has no limitations, but standard techniques to simplify sets of dependency pairs – such as the subterm criterion, usable rules and reduction pairs – are either not applicable or significantly weaker. On the other hand, we can significantly improve the dynamic approach for local systems. In this paper, I will discuss how to combine the dynamic and static styles in a single dependency pair framework, extending various notions from the first-order setting.




author = "Cynthia Kop",
title = "The Higher-Order Dependency Pair Framework",
booktitle = "Proceedings of the 7th International Workshop on Higher-Order Rewriting",
editor = "Kristoffer Rose",
year = 2014
Nach oben scrollen