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

@inproceedings{CSAM-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,
publisher   = "Springer-Verlag",
year        = 2008,
pages       = "336--350"
}

Erratum

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.