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].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.