Univ.-Prof. Dr. Aart Middeldorp   

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   bibtex   pdf (preprint)   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.