Termination

In this chapter we will first sketch a proof of the well-known fact that termination is undecidable. In Chapter 6 this result will be strengthened in several respects. In Section 5.2 standard methods for proving termination are reviewed: Polynomial interpretations yield polynomial termination, whereas recursive path orderings show simple termination. As a matter of fact, there are several other properties related to termination that form the so-called termination hierarchy. We will review this hierarchy in Section 5.3. After that, some newer techniques for proving termination will be treated: the dependency pair method, semantic labeling, and type introduction. Finally, we will study innermost termination.