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

@inproceedings{NHAMHZ-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,
publisher   = "Springer-Verlag",
year        = 2008,
pages       = "667--681"
}