cl-banner

From Outermost Termination to Innermost Termination

René Thiemann

Proceedings of the 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2009), Lecture Notes in Computer Science 5404, pp. 533 – 545, 2009.

Abstract

Rewriting is the underlying evaluation mechanism of functional programming languages. Therefore, termination analysis of term rewrite systems (TRSs) is an important technique for program verification. To capture the evaluation mechanism of a program-ming language one has to take care of the evaluation strategy, where we focus on the outermost strategy.
As there are only few techniques available to analyze outermost termination of TRSs directly, we introduce a new transformation such that a TRS is outermost terminating iff the transformed TRS is innermost terminating. In this way all of the several tech-niques that have been developed to investigate innermost termination become applicable to analyze outermost termination, too. We have implemented the transformation and successfully evaluated it on a large collection of TRSs.

 

  PDF |    doi:10.1007/978-3-540-95891-8_48  |  © Springer

BibTeX 

@inproceedings{RT-SOFSEM09,
author = "Ren{\'e} Thiemann",
title = "From Outermost Termination to Innermost Termination",
booktitle = "Proceedings of the 35th International Conference on Current Trends in
Theory and Practice of Computer Science",
series = "Lecture Notes in Computer Science",
volume = 5404,
pages = "533--545",
publisher = "Springer-Verlag",
year = 2009
}
Nach oben scrollen