Advertisement

Complexity Bounds for Ordinal-Based Termination

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

Abstract

‘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

Keywords

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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), http://arxiv.org/abs/1208.4041
  5. 5.
    Ben-Amram, A.M., Vainer, M.: Bounded termination of monotonicity-constraint transition systems (preprint, 2014), http://arxiv.org/abs/1202.4281
  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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)CrossRefMATHGoogle Scholar
  12. 12.
    Clote, P.: On the finite containment problem for Petri nets. Theor. Comput. Sci. 43, 99–105 (1986)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle Scholar
  26. 26.
    Lepper, I.: Simply terminating rewrite systems with long derivations. Arch. Math. Logic 43(1), 1–18 (2004)MathSciNetCrossRefMATHGoogle Scholar
  27. 27.
    Löb, M.H., Wainer, S.S.: Hierarchies of number theoretic functions, I. Arch. Math. Logic 13, 39–51 (1970)CrossRefMATHGoogle Scholar
  28. 28.
    McAloon, K.: Petri nets and large finite sets. Theor. Comput. Sci. 32(1-2), 173–183 (1984)MathSciNetCrossRefMATHGoogle 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), http://arxiv.org/abs/1312.5686 (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), http://cel.archives-ouvertes.fr/cel-00727025
  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), http://arxiv.org/abs/1402.2908 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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

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

Personalised recommendations