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 programming 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 techniques 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.

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
}