Abstract

First-order applicative term rewrite systems provide a natural framework for modeling higher-order aspects. In this paper we present a transformation from untyped applicative term rewrite systems to functional term rewrite systems that preserves and reflects termination. Our transformation is less restrictive than other approaches. In particular, head variables in right-hand sides of rewrite rules can be handled. To further increase the applicability of our transformation, we present a version for dependency pairs.

BibTeX Entry

@inproceedings{HMZ-LPAR08,
 author    = "Nao Hirokawa and Aart Middeldorp and Harald Zankl",
 title     = "Uncurrying for Termination",
 booktitle = "Proceedings of the 15th International Conferences on Logic
              for Programming, Artificial Intelligence and Reasoning",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 5330,
 pages     = "667--681",
 year      = 2008,
 doi       = "10.1007/978-3-540-89439-1\_46"
}