Abstract

Uncurrying is a termination technique for applicative term rewrite systems. During our formalization of uncurrying in the theorem prover Isabelle, we detected a gap in the original pen-and-paper proof which cannot directly be filled without further preconditions. Our final formalization does not demand additional preconditions, and generalizes the existing techniques since it allows to uncurry non-applicative term rewrite systems. Furthermore, we provide new results on uncurrying for relative termination and for dependency pairs.

BibTeX

@inproceedings{CSRT-FroCoS11,
  author      = "Christian Sternagel and Ren{\'e} Thiemann",
  title       = "Generalized and Formalized Uncurrying",
  booktitle   = "Proceedings of the 8th International Symposium on
                 Frontiers of Combining Systems",
  series      = "Lecture Notes in Artificial Intelligence",
  volume      = 6989,
  pages       = "243--258",
  publisher   = "Springer-Verlag",
  year        = 2011
}