Document

# An Intuitionistic Analysis of Size-change Termination

## File

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

## Cite As

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.
##### Keywords
• Intuitionism
• Ramsey's Theorem
• Termination

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## 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.
2. Thorsten Altenkirch. A formalization of the strong normalization proof for system F in LEGO. In TLCA, pages 13-28, 1993.
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.
4. Stefano Berardi, Paulo Oliva, and Silvia Steila. Proving termination with transition invariants of height omega. CoRR, abs/1407.4692, 2014.
5. Stefano Berardi and Silvia Steila. Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic. In TYPES, pages 64-83, 2013.
6. Stefano Berardi and Silvia Steila. Ramsey theorem as an intuitionistic property of well founded relations. In RTA-TLCA, pages 93-107, 2014.
7. Stefano Berardi, Silvia Steila, and Keita Yokoyama. Notes on H-closure. In preparation.
8. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Abstraction refinement for termination. In SAS, pages 87-101, 2005.
9. Thierry Coquand. A direct proof of Ramsey’s Theorem. Author’s website, revised in 2011, 1994.
10. Paul Erdős and George Szekeres. A combinatorial problem in geometry. Compositio Mathematica, 2:463-470, 1935.
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.
12. Alfons Geser. Relative termination. PhD thesis, Universitat Passau, 1990.
13. Matthias Heizmann, Neil D. Jones, and Andreas Podelski. Size-change termination and transition invariants. In SAS, pages 22-50, 2010.
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.
15. M.H. Löb and S.S. Wainer. Hierarchies of number-theoretic functions. i. Arch. Math. Logic, 13(1-2):39-51, 1970.
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.
17. Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory. J. of Symb. Comp., 2(4):325-355, 1986.
18. Andreas Podelski and Andrey Rybalchenko. Transition invariants. In LICS, pages 32-41, 2004.
19. Frank Plumpton Ramsey. On a problem in formal logic. Proc. London Math. Soc., 30:264-286, 1930.
20. Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop when you are almost-full - adventures in constructive termination. In ITP, pages 250-265, 2012.