Bar recursion is not computable via iteration

DOI10.3233/COM-180200MaRDI QIDQ5211057zbMATH OpenOpenAlexWikidataFDO

Authors John Longley

Publication date 17 January 2020

Published in Computability (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1804.07277

zbMATH Keywords

bar recursioncomputabilityhigher-order computabilityiterationnon-definability

Mathematics Subject Classification ID

Higher-type and set recursion theory (03D65) Abstract and axiomatic computability and recursion theory (03D75)

Abstract: We show that the bar recursion operators of Spector and Kohlenbach, considered as third-order functionals acting on total arguments, are not computable in Goedel's System T plus minimization, which we show to be equivalent to a programming language with a higher-order iteration construct. The main result is formulated so as to imply the non-definability of bar recursion in T + min within a variety of partial and total models, for instance the Kleene-Kreisel continuous functionals. The paper thus supplies proofs of some results stated in the book by Longley and Normann. The proof of the main theorem makes serious use of the theory of nested sequential procedures (also known as PCF Boehm trees), and proceeds by showing that bar recursion cannot be represented by any sequential procedure within which the tree of nested function applications is well-founded.

Recommendations

• Bar recursion over finite partial functions
• On Spector's bar recursion
• scientific article; zbMATH DE number 7297814
• The equivalence of bar recursion and open recursion
• An undecidable nested recurrence relation
• Bar recursion and products of selection functions
• Modified bar recursion
• An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
• Selection functions, bar recursion and backward induction
• scientific article; zbMATH DE number 1156830

Cited in

(5)

• On Spector's bar recursion
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• A direct proof of Schwichtenberg's bar recursion closure theorem
• Bar recursion over finite partial functions
• Asymptotic speedup via effect handlers

This page was built for publication: Bar recursion is not computable via iteration

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5211057)