AUTOMATED TERMINATION ANALYSIS OF TERM REWRITING

Carsten Fuhs (Birkbeck, University of London)

Termination analysis of term rewrite systems (TRSs) considers the question whether a given TRS has only finite rewrite sequences (i.e., all computations halt after finitely many steps). This question is undecidable in general. Nonetheless, since the early 2000s the development of fully automated techniques and tools for termination analysis of TRSs has flourished. The state of the art is reflected in the annual International Termination and Complexity Competition, running since 2004.

This course is split into two parts. The first part will cover automated techniques for proving termination of TRSs. It includes an introduction to the Dependency Pair framework, which allows for decomposing termination problems into smaller subproblems and for incremental termination proofs. As a crucial ingredient for the proof steps, we will discuss widely used classes of well-founded orders on terms (e.g., orders induced by polynomial interpretations, matrix interpretations, ...; see also the course on Tree Automata Techniques for Term Rewriting).

Automation of the search for such orders on terms by modern termination tools is primarily based on satisfiability encodings for the considered class of orders. The resulting instances of the satisfiability problem are then solved by off-the-shelf SAT or SMT solvers (see also the course on Constraint Programming for Analysis of Rewriting).

The second part of the course deals with extensions and applications of automated termination proof technology for TRSs:

• A refinement of termination analysis that has received a lot of attention in recent years is complexity analysis. Here questions like "given a TRS, what is the maximum length of a rewrite sequence from terms of size at most n?" are investigated. We will see how techniques for termination analysis can be adapted to synthesize (asymptotic) upper bounds (like O(n²)) on the complexity of a given TRS.

• As an application of termination analysis for TRSs, we will consider termination analysis of programs in real-world programming languages (e.g., Haskell, Prolog, Java). Here the idea is to execute the program symbolically from its entry point with suitable generalization steps to obtain an over-approximation of all possible computations (in the spirit of Abstract Interpretation). A common theme for the symbolic program state representations (the "abstract domains") for the different programming languages is to capture aspects of the program states that lend themselves to a representation as terms. Then a TRS is extracted from the program analysis such that a termination proof for the TRS also implies termination of the original program. This approach enables a re-use of termination provers for term rewriting for widely used programming languages. In this way, term rewriting is used as an intermediate language for proving program termination.

Bibliography:

1. T. Arts and J. Giesl: Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1-2):133-178, 2000.

2. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke: Mechanizing and improving dependency pairs. Journal of Automated Reasoning, 37(3):155-203, 2006.

3. N. Hirokawa and A. Middeldorp: Tyrolean Termination Tool: Techniques and features. Information and Computation, 205(4):474-511, 2007.

4. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl: SAT solving for termination analysis with polynomial interpretations. Proc. SAT '07, pages 340-354, 2007.

5. J. Endrullis, J. Waldmann, and H. Zantema: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning, 40(2-3):195-220, 2008.

6. A. Yamada: Multi-dimensional interpretations for termination of term rewriting. Proc. CADE '21, pages 273-290, 2021.

7. N. Hirokawa and G. Moser: Automated complexity analysis based on the dependency pair method. Proc. IJCAR '08, pages 364-379, 2008.

8. L. Noschinski, F. Emmes, and J. Giesl: Analyzing innermost runtime complexity of term rewriting by dependency pairs. Journal of Automated Reasoning, 51(1):27-56, 2013.

9. J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann: Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems, 33(2):7:1-7:39, 2011.

10. J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs: Symbolic evaluation graphs and term rewriting - A general methodology for analyzing logic programs. Proc. PPDP '12, pages 1-12, 2012.

11. C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl: Automated termination analysis of Java Bytecode by term rewriting. Proc. RTA '10, pages 259-276, 2010.