کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4661634 1633447 2015 25 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
An intuitionistic version of Ramsey's Theorem and its use in Program Termination
ترجمه فارسی عنوان
نسخه شهودی از قضیه رمزی و استفاده از آن در خاتمه برنامه
کلمات کلیدی
شهود گرایی؛ قضیه رمزی؛ تعاریف القایی؛ خاتمه برنامه های در حال اجرا
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

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

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 166, Issue 12, December 2015, Pages 1382–1406
نویسندگان
, ,