Document Open Access Logo

An Intuitionistic Analysis of Size-change Termination

Author Silvia Steila

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Silvia Steila

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

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.

Subject Classification

Keywords
  • Intuitionism
  • Ramsey's Theorem
  • Termination

Metrics

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

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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact