Complexity Bounds for Ordinal-Based Termination

(Invited Talk)
  • Sylvain Schmitz
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8762)


‘What more than its truth do we know if we have a proof of a theorem in a given formal system?’ We examine Kreisel’s question in the particular context of program termination proofs, with an eye to deriving complexity bounds on program running times.

Our main tool for this are length function theorems, which provide complexity bounds on the use of well quasi orders. We illustrate how to prove such theorems in the simple yet until now untreated case of ordinals. We show how to apply this new theorem to derive complexity bounds on programs when they are proven to terminate thanks to a ranking function into some ordinal.

1998 ACM Subject Classification. F.2.0 Analysis of Algorithms and Problem Complexity; F.3.1 Logics and Meanings of Programs


Fast-growing complexity length function theorem Ramsey-based termination ranking function well quasi order 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abriola, S., Figueira, S., Senno, G.: Linearizing bad sequences: Upper bounds for the product and majoring well quasi-orders. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 110–126. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117–133. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Ben-Amram, A.M.: General size-change termination and lexicographic descent. The Essence of Computation, pp. 3–17. Springer (2002)Google Scholar
  4. 4.
    Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops (2013),
  5. 5.
    Ben-Amram, A.M., Vainer, M.: Bounded termination of monotonicity-constraint transition systems (preprint, 2014),
  6. 6.
    Blass, A., Gurevich, Y.: Program termination and well partial orderings. ACM Trans. Comput. Logic 9(3) (2008)Google Scholar
  7. 7.
    Bonfante, G., Cichoń, A.E., Marion, J.Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Funct. Programming 11, 33–53 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Buchholz, W., Cichoń, E.A., Weiermann, A.: A uniform approach to fundamental sequences and hierarchies. Math. Logic Quart. 40(2), 273–286 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Bucholz, W.: Proof-theoretic analysis of termination proofs. Ann. Pure App. Logic 75(1–2), 57–65 (1995)CrossRefGoogle Scholar
  10. 10.
    Cichoń, E.A.: Termination orderings and complexity characterisations. Proof Theory, pp. 171–194. Cambridge University Press (1993)Google Scholar
  11. 11.
    Cichoń, E.A., Tahhan Bittar, E.: Ordinal recursive bounds for Higman’s Theorem. Theor. Comput. Sci. 201(1-2), 63–84 (1998)CrossRefzbMATHGoogle Scholar
  12. 12.
    Clote, P.: On the finite containment problem for Petri nets. Theor. Comput. Sci. 43, 99–105 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Colcombet, T., Daviaud, L., Zuleger, F.: Size-change abstraction and max-plus automata. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 208–219. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  14. 14.
    Cook, B., See, A., Zuleger, F.: Ramsey vs. Lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 47–61. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  15. 15.
    Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465–476 (1979)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Dershowitz, N., Okada, M.: Proof-theoretic techniques for term rewriting theory. In: LICS 1988, pp. 104–111 (1988)Google Scholar
  17. 17.
    Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In: LICS 2011., pp. 269–278. IEEE (2011)Google Scholar
  18. 18.
    Floyd, R.W.: Assigning meaning to programs. Mathematical Aspects of Computer Science. In: Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19–32. AMS (1967)Google Scholar
  19. 19.
    Gulwani, S.: SPEED: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 51–62. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  20. 20.
    Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–379. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theor. Comput. Sci. 105(1), 129–140 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    de Jongh, D.H.J., Parikh, R.: Well-partial orderings and hierarchies. Indag. Math. 39(3), 195–207 (1977)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Jouannaud, J.P., Lescanne, P.: On multiset orderings. Inf. Process. Lett. 15(2), 57–63 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL 2001, pp. 81–92. ACM (2001)Google Scholar
  25. 25.
    Lepper, I.: Derivation lengths and order types of Knuth-Bendix orders. Theor. Comput. Sci. 269(1-2), 433–450 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Lepper, I.: Simply terminating rewrite systems with long derivations. Arch. Math. Logic 43(1), 1–18 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Löb, M.H., Wainer, S.S.: Hierarchies of number theoretic functions, I. Arch. Math. Logic 13, 39–51 (1970)CrossRefzbMATHGoogle Scholar
  28. 28.
    McAloon, K.: Petri nets and large finite sets. Theor. Comput. Sci. 32(1-2), 173–183 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Moser, G.: KBOs, ordinals, subrecursive hierarchies and all that. J. Logic Comput. (to appear, 2014)Google Scholar
  30. 30.
    Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004. pp. 32–41. IEEE (2004)Google Scholar
  31. 31.
    Schmitz, S.: Complexity hierarchies beyond Elementary (2013), (preprint)
  32. 32.
    Schmitz, S., Schnoebelen, P.: Multiply-recursive upper bounds with higman’s lemma. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 441–452. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  33. 33.
    Schmitz, S., Schnoebelen, P.: Algorithmic aspects of wqo theory. Lecture notes (2012),
  34. 34.
    Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 5–24. Springer, Heidelberg (2013), CrossRefGoogle Scholar
  35. 35.
    Schwichtenberg, H., Wainer, S.S.: Proofs and Computation. Perspectives in Logic. Cambridge University Press (2012)Google Scholar
  36. 36.
    Turing, A.M.: Checking a large routine. In: EDSAC 1949, pp. 67–69 (1949)Google Scholar
  37. 37.
    Urban, C., Miné, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 412–431. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  38. 38.
    Weiermann, A.: Complexity bounds for some finite forms of Kruskal’s Theorem. J. Symb. Comput. 18(5), 463–488 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  39. 39.
    Weiermann, A.: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths. Theor. Comput. Sci. 139(1-2), 355–362 (1995)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Sylvain Schmitz
    • 1
  1. 1.LSVENS Cachan & CNRS & INRIAFrance

Personalised recommendations