کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4661720 1633459 2014 28 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
The equivalence of bar recursion and open recursion
ترجمه فارسی عنوان
هم ارزی بازگشت نوار و بازگشت باز
کلمات کلیدی
TT سیستم Gödel ؛ هم ارزی بازگشتی اولیه؛ بازگشت نوار؛ بازگشت باز
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

Several extensions of Gödel's system TT with new forms of recursion have been designed for the purpose of giving a computational interpretation to classical analysis. One can organise many of these extensions into two groups: those based on bar recursion, which include Spector's original bar recursion, modified bar recursion and the more recent products of selections functions, or those based on open recursion   which in particular include the symmetric Berardi–Bezem–Coquand (BBC) functional. We relate these two groups by showing that both open recursion and the BBC functional are primitive recursively equivalent to a variant of modified bar recursion. Our results, in combination with existing research, essentially complete the classification up to primitive recursive equivalence of those extensions of system TT used to give a direct computational interpretation to choice principles.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 165, Issue 11, November 2014, Pages 1727–1754
نویسندگان
,