H.: Uncurrying for termination

Abstract. First-order applicative term rewrite systems provide a natu-ral framework for modeling higher-order aspects. In this paper we present a transformation from untyped applicative term rewrite systems to func-tional 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.