Abstract

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.

BibTeX

@inproceedings{CK-HOR14,
  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
}