On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems

  • Alfons Geser
  • Dieter Hofbauer
  • Johannes Waldmann
  • Hans Zantema
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


We present a new method for proving termination of term rewriting systems automatically. It is a generalization of the match bound method for string rewriting. To prove that a term rewriting system terminates on a given regular language of terms, we first construct an enriched system over a new signature that simulates the original derivations. The enriched system is an infinite system over an infinite signature, but it is locally terminating: every restriction of the enriched system to a finite signature is terminating. We then construct iteratively a finite tree automaton that accepts the enriched given regular language and is closed under rewriting modulo the enriched system. If this procedure stops, then the enriched system is compact: every enriched derivation involves only a finite signature. Therefore, the original system terminates. We present three methods to construct the enrichment: top heights, roof heights, and match heights. Top and roof heights work for left-linear systems, while match heights give a powerful method for linear systems. For linear systems, the method is strengthened further by a forward closure construction. Using these methods, we give examples for automated termination proofs that cannot be obtained by standard methods.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)Google Scholar
  2. 2.
    Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997–2001), Available at
  3. 3.
    Contejean, E., Marché, C., Monate, B., Urbain, X.: Proving Termination of Rewriting with CiME. In: Rubio, A. (ed.) Proc. 6th Int. Workshop on Termination WST 2003, Universidad Politécnica de Valencia, Spain. Technical Report DSIC II/15/03, pp. 71–73 (2003)Google Scholar
  4. 4.
    Dershowitz, N.: Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981)Google Scholar
  5. 5.
    Gécseg, F., Steinby, M.: Tree Languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 3, pp. 1–68. Springer, Heidelberg (1997)Google Scholar
  6. 6.
    Genet, T.: Decidable approximations of sets of descendants and sets of normal forms. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 151–165. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  7. 7.
    Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. Appl. Algebra Engrg. Comm. Comput. 15(3-4), 149–171 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: Tree automata that certify termination of term rewriting systems. In: Codish, M., Middeldorp, A. (eds.) Proc. 7th Int. Workshop on Termination WST-04, Aachener Informatik Berichte AIB-2004-07, RWTH Aachen, Gemany, pp. 14–17 (2004)Google Scholar
  9. 9.
    Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: Tree automata that certify termination of left-linear term rewriting systems (2005), Full version available at
  10. 10.
    Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: Finding finite automata that certify termination of string rewriting. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. LNCS, vol. 3317, pp. 134–145. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Geupel, O.: Overlap closures and termination of term rewriting systems. Technical Report MIP-8922, Universität Passau, Germany (1989)Google Scholar
  12. 12.
    Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Hirokawa, N., Middeldorp, A.: Tsukuba Termination Tool. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 311–320. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    Lankford, D.S., Musser, D.R.: A finite termination criterion. Unpublished draft, Information Sciences Institute, University of Southern California, Marina-del-Rey, CA (1978)Google Scholar
  15. 15.
    Marché, C., Rubio, A. (eds.): Termination Problems Data Base (2004),
  16. 16.
    Middeldorp, A.: Approximations for strategies and termination. In: Proc. 2nd Int. Workshop on Reduction Strategies in Rewriting and Programming. Electron. Notes Theor. Comput. Sci, vol. 70(6) (2002)Google Scholar
  17. 17.
    van Oostrom, V., de Vrijer, R.: Equivalences of Reductions. In: Terese, Term Rewriting Systems, pp. 301–474. Cambridge Univ. Press, Cambridge (2003)Google Scholar
  18. 18.
    Waldmann, J.: Matchbox: a tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85–94. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Zantema, H.: TORPA: Termination of rewriting proved automatically. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 95–104. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    Zantema, H.: Termination. In: Terese, Term Rewriting Systems, pp. 181–259. Cambridge University Press, Cambridge (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Alfons Geser
    • 1
  • Dieter Hofbauer
    • 2
  • Johannes Waldmann
    • 3
  • Hans Zantema
    • 4
  1. 1.National Institute of AerospaceHamptonUSA
  2. 2. KasselGermany
  3. 3.Fb IMNHochschule für Technik, Wirtschaft und Kultur (FH) LeipzigLeipzigGermany
  4. 4.Faculteit Wiskunde en InformaticaTechnische Universiteit EindhovenEindhovenThe Netherlands

Personalised recommendations