We give the first mechanized proof of the fact that for showing termination of a term rewrite system, we may restrict to well-formed terms using just the function symbols actually occurring in the rules of the system. Or equivalently, termination of a term rewrite system is preserved under signature extensions. We did not directly formalize the existing proofs for this well-known result, but developed a new and more elegant proof by reusing facts about dependency pairs. We also investigate signature extensions for termination proofs that use dependency pairs. Here, we were able to develop counterexamples which demonstrate that signature extensions are unsound in general. We further give two conditions where signature extensions are still possible.
展开▼
