Uncurrying for Termination

Nao Hirokawa, Aart Middeldorp, and Harald Zankl

Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 667 – 681, 2008.


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.


  PDF |    doi:10.1007/978-3-540-89439-1_46  |  © Springer


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"
Nach oben scrollen