کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4661634 | 1633447 | 2015 | 25 صفحه PDF | دانلود رایگان |
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 H stands 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].
Journal: Annals of Pure and Applied Logic - Volume 166, Issue 12, December 2015, Pages 1382–1406