Skip to main content
SpringerLink
Log in

Stop When You Are Almost-Full

Adventures in Constructive Termination

  • Conference paper
Book cover Interactive Theorem Proving (ITP 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7406))

Included in the following conference series:

Abstract

Disjunctive well-foundedness, size-change termination, and well-quasi-orders are examples of techniques that have been successfully applied to program termination. Although these works originate in different communities, they rely on closely related principles and both employ similar arguments from Ramsey theory. At the same time there is a notable absence of these techniques in programming systems based on constructive type theory. In this paper we’d like to highlight the aforementioned connection and make the core ideas widely accessible to theoreticians and programmers, by offering a development in type theory which culminates in some novel tools for induction. Inevitably, we have to present some Ramsey-like arguments: Though similar proofs are typically classical, we offer an entirely constructive development based on the work of Bezem and Veldman, and Richman and Stolzenberg.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abel, A.: Termination and productivity checking with continuous types. In: Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications, TLCA 2003, Valencia, Spain, pp. 1–15. Springer, Heidelberg (2003), http://dl.acm.org/citation.cfm?id=1762348.1762349 , ISBN: 3-540-40332-9

  2. Ben-Amram, A.M.: General Size-Change Termination and Lexicographic Descent. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 3–17. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Berghofer, S.: A Constructive Proof of Higman’s Lemma in Isabelle. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 66–82. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)

    Google Scholar 

  5. Blanqui, F., Koprowski, A.: Color: a COQ library on well-founded rewrite relations and its application to the automated verification of termination certificates. MSCS 21(4), 827–859 (2011)

    MathSciNet  MATH  Google Scholar 

  6. Bolingbroke, M., Jones, S.P., Vytiniotis, D.: Termination combinators forever. In: Proceedings of the 4th ACM Symposium of Haskell 2011, pp. 23–34. ACM (2011)

    Google Scholar 

  7. Bove, A., Capretta, V.: Modelling general recursion in type theory. MSCS 15, 671–708 (2005)

    MathSciNet  MATH  Google Scholar 

  8. Charguéraud, A.: The Optimal Fixed Point Combinator. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 195–210. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  9. Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of PLDI 2006, pp. 415–426. ACM (2006)

    Google Scholar 

  10. Coquand, T.: An analysis of Ramsey’s Theorem. Inf. Comput. 110, 297–304 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  11. Coquand, T., Siles, V.: A Decision Procedure for Regular Expression Equivalence in Type Theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 119–134. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  12. Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Appl. Algebra Eng. Commun. Comput. 12(1/2), 117–156 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  13. Fridlender, D.: Higman’s Lemma in Type Theory. In: Giménez, E. (ed.) TYPES 1996. LNCS, vol. 1512, pp. 112–133. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Geser, A.: Relative termination. PhD thesis, Universität Passau (1990)

    Google Scholar 

  15. Heizmann, M., Jones, N.D., Podelski, A.: Size-Change Termination and Transition Invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 22–50. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Jones, N.D., Bohr, N.: Call-by-value termination in the untyped lambda-calculus. Logical Methods in Computer Science 4(1) (2008)

    Google Scholar 

  17. Krauss, A., Sternagel, C., Thiemann, R., Fuhs, C., Giesl, J.: Termination of Isabelle Functions via Termination of Rewriting. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 152–167. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  18. Krauss, A.: Certified Size-Change Termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 460–475. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Krauss, A.: Partial and nested recursive function definitions in higher-order logic. Journal of Automated Reasoning 44, 303–336 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  20. Kruskal, J.B.: Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture. Trans. Amer. Math. Soc. 95, 210–225 (1960)

    MathSciNet  MATH  Google Scholar 

  21. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of POPL 2001, pp. 81–92. ACM (2001)

    Google Scholar 

  22. Leuschel, M.: Homeomorphic Embedding for Online Termination of Symbolic Methods. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 379–403. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  23. Megacz, A.: A coinductive monad for Prop-bounded recursion. In: Stump, A., Xi, H. (eds.) Proceedings of PLPV 2007, pp. 11–20. ACM (2007)

    Google Scholar 

  24. Bezem, M.A., Nakata, K., Uustalu, T.: On streams that are finitely red. To appear in Logical Methods in Computer Science (2011)

    Google Scholar 

  25. Nash-Williams, C.S.J.A.: On well-quasi-ordering finite trees. In: Mathematical Proceedings of the Cambridge Philosophical Society, vol. 59, pp. 833–835. Cambridge Univ. Press (1963)

    Google Scholar 

  26. Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of LICS 2004, pp. 32–41. IEEE Computer Society, Washington, DC (2004)

    Google Scholar 

  27. Richman, F., Stolzenberg, G.: Well-quasi-ordered sets. Advanced Mathematics, 145–193 (1993)

    Google Scholar 

  28. Sagiv, Y.: A termination test for logic programs. In: ISLP, pp. 518–532 (1991)

    Google Scholar 

  29. Seisenberger, M.: An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument for Higman’s Lemma. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 233–242. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  30. Sereni, D.: Termination analysis and call graph construction for higher-order functional programs. In: Proceedings of ICFP 2007, pp. 71–84. ACM (2007)

    Google Scholar 

  31. Sørensen, M.H., Glück, R.: An algorithm of generalization in positive supercompilation. In: Proceedings of ILPS 1995, The International Logic Programming Symposium, pp. 465–479. MIT Press (1995)

    Google Scholar 

  32. Sozeau, M.: Subset Coercions in COQ. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 237–252. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  33. Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning 2(1), 41–62 (2009)

    MathSciNet  MATH  Google Scholar 

  34. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)

    Google Scholar 

  35. Veldman, W., Bezem, M.: Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society s2-47(2), 193–211 (1993)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Cambridge, UK

    Dimitrios Vytiniotis

  2. University of Gothenburg, Sweden

    Thierry Coquand & David Wahlstedt

Authors
  1. Dimitrios Vytiniotis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thierry Coquand
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Wahlstedt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Princeton University, 35 Olden Street, 08540, Princeton, NJ, USA

    Lennart Beringer

  2. School of Electrical Engineering and Computer Science, University of Ottawa, 800 King Edward Ave., K1N 6N5, Ottawa, ON, Canada

    Amy Felty

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vytiniotis, D., Coquand, T., Wahlstedt, D. (2012). Stop When You Are Almost-Full. In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, vol 7406. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32347-8_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32347-8_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32346-1

  • Online ISBN: 978-3-642-32347-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation