DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2014.288

An Intuitionistic Analysis of Size-change Termination

Authors: Silvia Steila

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

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

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)

Copy BibTex To Clipboard

@InProceedings{steila:LIPIcs.TYPES.2014.288,
  author =	{Steila, Silvia},
  title =	{{An Intuitionistic Analysis of Size-change Termination}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{288--307},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.288},
  URN =		{urn:nbn:de:0030-drops-55026},
  doi =		{10.4230/LIPIcs.TYPES.2014.288},
  annote =	{Keywords: Intuitionism, Ramsey's Theorem, Termination}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2013.64

Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic

Authors: Stefano Berardi and Silvia Steila

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract

We produce a first order proof of a famous combinatorial result, Ramsey Theorem for pairs and in two colors. Our goal is to find the minimal classical principle that implies the "miniature" version of Ramsey we may express in Heyting Arithmetic HA. We are going to prove that Ramsey Theorem for pairs with recursive assignments of two colors is equivalent in HA to the sub-classical principle Sigma-0-3-LLPO. One possible application of our result could be to use classical realization to give constructive proofs of some combinatorial corollaries of Ramsey; another, a formalization of Ramsey in HA, using a proof assistant. In order to compare Ramsey Theorem with first order classical principles, we express it as a schema in the first order language of arithmetic, instead of using quantification over sets and functions as it is more usual: all sets we deal with are explicitly defined as arithmetical predicates. In particular, we formally define the homogeneous set which is the witness of Ramsey theorem as a Delta-0-3-arithmetical predicate.

Cite as

Stefano Berardi and Silvia Steila. Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 64-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{berardi_et_al:LIPIcs.TYPES.2013.64,
  author =	{Berardi, Stefano and Steila, Silvia},
  title =	{{Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{64--83},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.64},
  URN =		{urn:nbn:de:0030-drops-46269},
  doi =		{10.4230/LIPIcs.TYPES.2013.64},
  annote =	{Keywords: Formalization, Constructivism, Classical logic, Ramsey Theorem}
}

Search Results

Documents authored by Steila, Silvia

An Intuitionistic Analysis of Size-change Termination

Abstract

Cite as

Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic

Abstract

Cite as

Thanks for your feedback!

Could not send message