Uncurrying for Termination and Complexity

Nao Hirokawa, Aart Middeldorp, and Harald Zankl

Journal of Automated Reasoning 50(3), pp. 279 – 315, 2013.


First-order applicative rewrite systems provide a natural framework for modeling higher-order aspects. In this article 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 study the method for innermost rewriting and derivational complexity, and present a version for dependency pairs.


  PDF |    doi:10.1007/s10817-012-9248-3  |  © Creative Commons


author = "N.~Hirokawa and A.~Middeldorp and H.~Zankl",
title = "Uncurrying for Termination and Complexity",
journal = "Journal of Automated Reasoning",
volume = 50,
number = 3,
pages = "279--315",
year = 2013
Nach oben scrollen