Document Open Access Logo

An Intuitionistic Analysis of Size-change Termination

Author Silvia Steila

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2014.288.pdf
  • Filesize: 430 kB
  • 20 pages

Document Identifiers

Subject Classification

Keywords
  • Intuitionism
  • Ramsey's Theorem
  • Termination

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (SCT) for first order functional programs, a sufficient condition for termination. They proved that a program is size-change terminating if and only if it has a certain property which can be statically verified from the recursive definition of the program. Their proof of the size-change termination theorem used Ramsey's Theorem for pairs, which is a purely classical result. In 2012 Vytiniotis, Coquand and Wahlsteldt intuitionistically proved a classical variant of the size-change termination theorem by using the Almost-Full Theorem instead of Ramsey's Theorem for pairs. In this paper we provide an intuitionistic proof of another classical variant of the SCT theorem: our goal is to provide a statement and a proof very similar to the original ones. This can be done by using the H-closure Theorem, which differs from Ramsey's Theorem for pairs only by a contrapositive step.  As a side result we obtain another proof of the characterization of the functions computed by a tail-recursive SCT program, by relating the SCT Theorem with the Termination Theorem by Podelski and Rybalchenko. Finally, by investigating the relationship between them, we provide a property in the "language" of size-change termination which is equivalent to Podelski and Rybalchenko's termination.

Cite As Get BibTex

Silvia Steila. An Intuitionistic Analysis of Size-change Termination. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 288-307, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TYPES.2014.288

Author Details

Silvia Steila

References

  1. Peter Aczel. Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter An introduction to inductive definitions, pages 739-782. Elsevier, 1977. Google Scholar
  2. Thorsten Altenkirch. A formalization of the strong normalization proof for system F in LEGO. In TLCA, pages 13-28, 1993. Google Scholar
  3. Amir M. Ben-Amram. General size-change termination and lexicographic descent. In Torben Mogensen, David Schmidt, and I. Hal Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of LNCS, pages 3-17. Springer-Verlag, 2002. Google Scholar
  4. Stefano Berardi, Paulo Oliva, and Silvia Steila. Proving termination with transition invariants of height omega. CoRR, abs/1407.4692, 2014. Google Scholar
  5. Stefano Berardi and Silvia Steila. Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic. In TYPES, pages 64-83, 2013. Google Scholar
  6. Stefano Berardi and Silvia Steila. Ramsey theorem as an intuitionistic property of well founded relations. In RTA-TLCA, pages 93-107, 2014. Google Scholar
  7. Stefano Berardi, Silvia Steila, and Keita Yokoyama. Notes on H-closure. In preparation. Google Scholar
  8. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Abstraction refinement for termination. In SAS, pages 87-101, 2005. Google Scholar
  9. Thierry Coquand. A direct proof of Ramsey’s Theorem. Author’s website, revised in 2011, 1994. Google Scholar
  10. Paul Erdős and George Szekeres. A combinatorial problem in geometry. Compositio Mathematica, 2:463-470, 1935. Google Scholar
  11. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In LICS, pages 269-278. IEEE Press, 2011. Google Scholar
  12. Alfons Geser. Relative termination. PhD thesis, Universitat Passau, 1990. Google Scholar
  13. Matthias Heizmann, Neil D. Jones, and Andreas Podelski. Size-change termination and transition invariants. In SAS, pages 22-50, 2010. Google Scholar
  14. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In POPL, pages 81-92, 2001. Google Scholar
  15. M.H. Löb and S.S. Wainer. Hierarchies of number-theoretic functions. i. Arch. Math. Logic, 13(1-2):39-51, 1970. Google Scholar
  16. David Park. Concurrency and automata on infinite sequences. In Proceedings of the 5th GI-Conference on Theoretical Computer Science, pages 167-183. Springer-Verlag, 1981. Google Scholar
  17. Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory. J. of Symb. Comp., 2(4):325-355, 1986. Google Scholar
  18. Andreas Podelski and Andrey Rybalchenko. Transition invariants. In LICS, pages 32-41, 2004. Google Scholar
  19. Frank Plumpton Ramsey. On a problem in formal logic. Proc. London Math. Soc., 30:264-286, 1930. Google Scholar
  20. Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop when you are almost-full - adventures in constructive termination. In ITP, pages 250-265, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact