Root-Labeling
Christian Sternagel and Aart Middeldorp
Proceedings of the 19th International Conference on Rewriting Techniques
and Applications (RTA 2008), Lecture Notes in Computer Science 5117,
pp. 336 – 350, 2008
Abstract
In 2006 Jambox, a termination prover developed by Endrullis, surprised the termination community by winning the string rewriting division and almost beating AProVE in the term rewriting division of the international termination competition. The success of Jambox for strings is partly due to a very special case of semantic labeling. In this paper we integrate this technique, which we call root-labeling, into the dependency pair framework. The result is a simple processor with help of which TTT2 surprised the termination community in 2007 by producing the first automatically generated termination proof of a string rewrite system with non-primitive recursive complexity (Touzet, 1998). Unlike many other recent termination methods, the root-labeling processor is trivial to automate and completely unsuitable for producing human readable proofs.BibTeX Entry
@inproceedings{SM-RTA08,
author = "Christian Sternagel and Aart Middeldorp",
title = "Root-Labeling",
booktitle = "Proceedings of the 19th International Conference on Rewriting
Techniques and Applications",
series = "Lecture Notes in Computer Science",
volume = 5117,
pages = "336--350",
year = 2008,
doi = "10.1007/978-3-540-70590-1\_23"
}
© Springer
When trying to formalize the results of the paper in Isabelle/HOL, Christian Sternagel and René Thiemann discovered a serious bug in Lemmata 13 and 17. In the proofs it is claimed that by replacing in a presupposed minimal sequence all maximal proper subterms with a root symbol that belongs to F# by the same variable, a minimal sequence with the property that no function symbol occurring at a non-root position belongs to F# is obtained. This is wrong.
Consider the TRSs P = { F(x,y,z) → F(x,y,g(x,y)) } and R = { g(x,x) → h(x) }. The P-step F(F(x,y,z),F(y,x,z),g(F(x,y,z),F(y,x,z))) → F(F(x,y,z),F(y,x,z),g(F(x,y,z),F(y,x,z))) gives rise to a minimal sequence since F(x,y,z), F(y,x,z) and g(F(x,y,z),F(y,x,z)) are R-normal forms. If we replace the proper F-rooted subterms by a fresh variable u, we obtain the P-step F(u,u,g(u,u)) → F(u,u,g(u,u)) which does not result in a minimal sequence as g(u,u) is not an R-normal form.
More complicated counterexamples refute the statements of Lemmata 13 and 17. By imposing left-linearity or dropping the minimality requirement, the results in Section 4 are recovered.