Sciweavers

Share
CSL
2010
Springer

Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs

9 years 1 months ago
Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs
Abstract. 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.
Christian Sternagel, René Thiemann
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where CSL
Authors Christian Sternagel, René Thiemann
Comments (0)
books