cl-banner

Signature Extensions Preserve Termination – An Alternative Proof via Dependency Pairs

Christian Sternagel and René Thiemann

Proceedings of the 19th Annual Conference of the European Association for Computer Science Logic (CSL 2010), Lecture Notes in Computer Science 6247, pp. 514 – 528, 2010.

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.

 

  PDF |    doi:10.1007/978-3-642-15205-4_39  |  © Springer

BibTeX 

@inproceedings{NHAM-IJCAR10,
author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "Signature Extensions Preserve Termination -- An Alternative Proof via Dependency Pairs",
booktitle = "Proceedings of the 19th Annual Conference of the European Association for
Computer Science Logic",
series = "Lecture Notes in Computer Science",
volume = 6247,
pages = "514--528",
publisher = "Springer-Verlag",
year = 2010
}
Nach oben scrollen