On Spector's bar recursion
Bar recursion, introduced by \textit{C. Spector} [Proc. Sympos. Pure Math. 5, 1--27 (1962; Zbl 0143.25502)], is a generalized form of recursion. It is the computational analogue of the well-known principle of bar induction, in the same sense as primitive recursion is related with the logical principle of induction.NEWLINENEWLINEIn fact, Spector describes in [loc. cit.] two forms of bar recursion: general bar recursion (inspired in the above analogy with bar induction) and restricted bar recursion (enough to construct a Dialectica realizer for the double negation shift).NEWLINENEWLINEOne may be led to think that restricted bar recursion (rBR) is strictly weaker than general bar recursion (gBR). In the present paper, the authors show that this is not the case. They prove that the restricted and the general forms of bar recursion are inter-definable over system T.NEWLINENEWLINEIt is easy to see that rBR follows from gBR over Gödel's T (see also [\textit{U. Kohlenbach}, Applied proof theory. Proof interpretations and their use in mathematics. Berlin: Springer (2008; Zbl 1158.03002); \textit{H. Luckhardt}, Extensional Gödel functional interpretation. A consistency proof of classical analysis. Lect. Notes Math. 306. Berlin-Heidelberg-NewYork: Springer-Verlag (1973; Zbl 0262.02031)]). The main contribution of the paper lies in proving that rBR is in fact as general as gBR. It is accomplished by constructing a term in T + rBR which satisfies (provably in T + rBR) the equation for gBR.NEWLINENEWLINESince these two forms of bar recursion correspond (see [\textit{M. Escardó} and \textit{P. Oliva}, Lect. Notes Comput. Sci. 6158, 141--150 (2010; Zbl 1251.03073)]) to the (explicitly controlled) iterated products of selection functions and quantifiers, we can conclude that this iterated product of selection functions is T-equivalent to the corresponding iterated product of quantifiers.
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Extensional Gödel functional interpretation. A consistency proof of classical analysis
- scientific article; zbMATH DE number 3231083 (Why is no real title available?)
- scientific article; zbMATH DE number 3259893 (Why is no real title available?)
- scientific article; zbMATH DE number 3335898 (Why is no real title available?)
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- On bar recursion of types 0 and 1
- On the No-Counterexample Interpretation
- Ordinal analysis of simple cases of bar recursion
- Selection functions, bar recursion and backward induction
- Sequential games and optimal strategies
- Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Equivalence of bar recursors in the theory of functionals of finite type
- A coalgebraic view of bar recursion and bar induction
- A short note on Spector's proof of consistency of analysis
- System T and the product of selection functions
- Selection functions, bar recursion and backward induction
- The equivalence of bar recursion and open recursion
- A direct proof of Schwichtenberg's bar recursion closure theorem
- The Herbrand functional interpretation of the double negation shift
- scientific article; zbMATH DE number 7269245 (Why is no real title available?)
- scientific article; zbMATH DE number 7297814 (Why is no real title available?)
- Bar recursion over finite partial functions
- Bar recursion is not computable via iteration
- Bar recursion and products of selection functions
- Modified bar recursion
- Logical Approaches to Computational Barriers
- Diller-Nahm bar recursion
This page was built for publication: On Spector's bar recursion
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2910991)
