The equivalence of bar recursion and open recursion

Research output: Contribution to journalArticlepeer-review

11 Citations (SciVal)

Abstract

Several extensions of Gödel's system 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 used to give a direct computational interpretation to choice principles.
Original languageEnglish
Pages (from-to)1727-1754
JournalAnnals of Pure and Applied Logic
Volume165
Issue number11
DOIs
Publication statusPublished - 2014

Fingerprint

Dive into the research topics of 'The equivalence of bar recursion and open recursion'. Together they form a unique fingerprint.

Cite this