Transforming Termination by Self-Labelling(Theory of Rewriting Systems and Its Applications)
Maria Ferreira, Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema · Institutional Repositories DataBase (IRDB) · 1995
We introduce a new technique for proving termination of term rewriting systems.The technique, a $\mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{a}$ ] $\mathrm{i}_{\mathrm{Z}}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$ of Zantelna's semantic labelling technique, is especially useful for establishing the correctness of transformation methods that attempt to prove termination by transforlning $\mathrm{t}\mathrm{e}\mathrm{r}\ln$ rewriting $\mathrm{s}\mathrm{y}\mathrm{s}\iota \mathrm{e}\mathrm{l}\mathrm{n}\mathrm{S}$ into systems whose termination is $\mathrm{e}\mathrm{a}s$ ier to prove.We apply the technique to distribution elimination, dummy elimination, and currying, resulting in shorter correctness prook, stronger results, and a positive solution to an open problem.