Ramsey’s Theorem for pairs is a fundamental result in combinatorics which cannot be intuitionistically proved. In this paper we present a new form of Ramsey’s Theorem for pairs we call the H-closure Theorem, where Hstands for “homogeneous”. The H-closure Theorem is a property of well-founded relations, intuitionistically provable, informative, and simple to use in intuitionistic proofs. Using our intuitionistic version of Ramsey’s Theorem we intuitionistically prove the Termination Theorem by Podelski and Rybalchenko[25]. The Termination Theorem concerns an algorithm inferring termination for while-programs, and was originally proved from the classical Ramsey Theorem. Vytiniotis, Coquand, and Wahlstedt provided an intuitionistic proof of the Termination Theorem[29], using the Almost Full Theorem[11], an intuitionistic version of Ramsey’s Theorem different from the H-closure Theorem. We provide a second intuitionistic proof of the Termination Theorem using the H-closure Theorem. In another paper, we use our proof to extract bounds for the Termination Theorem[5].

An intuitionistic version of Ramsey Theorem and its use in Program Termination

BERARDI, Stefano;STEILA, SILVIA
2015-01-01

Abstract

Ramsey’s Theorem for pairs is a fundamental result in combinatorics which cannot be intuitionistically proved. In this paper we present a new form of Ramsey’s Theorem for pairs we call the H-closure Theorem, where Hstands for “homogeneous”. The H-closure Theorem is a property of well-founded relations, intuitionistically provable, informative, and simple to use in intuitionistic proofs. Using our intuitionistic version of Ramsey’s Theorem we intuitionistically prove the Termination Theorem by Podelski and Rybalchenko[25]. The Termination Theorem concerns an algorithm inferring termination for while-programs, and was originally proved from the classical Ramsey Theorem. Vytiniotis, Coquand, and Wahlstedt provided an intuitionistic proof of the Termination Theorem[29], using the Almost Full Theorem[11], an intuitionistic version of Ramsey’s Theorem different from the H-closure Theorem. We provide a second intuitionistic proof of the Termination Theorem using the H-closure Theorem. In another paper, we use our proof to extract bounds for the Termination Theorem[5].
2015
166
1382
1406
Stefano, Berardi; Silvia, Steila
File in questo prodotto:
File Dimensione Formato  
Steia-TLCA2014-RamseyTheoremAsAnIntuitionisticPropertyOf WellFoundedRelations.pdf

Accesso riservato

Tipo di file: PREPRINT (PRIMA BOZZA)
Dimensione 244.56 kB
Formato Adobe PDF
244.56 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Berardi-Steila-An-Intuitionistic-Version-Of-Ramsey-Theorem-1-s2.0-S0168007215000731-main.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 551.94 kB
Formato Adobe PDF
551.94 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Berardi-Steila-H-chiusura-Versioe-Rivista-Gennaio-2015.pdf

Accesso aperto

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 226.27 kB
Formato Adobe PDF
226.27 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1526155
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact