{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T02:39:44Z","timestamp":1777516784020,"version":"3.51.4"},"reference-count":26,"publisher":"SAGE Publications","issue":"2","license":[{"start":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T00:00:00Z","timestamp":1548374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Computability"],"published-print":{"date-parts":[[2019,6,17]]},"abstract":"<jats:p>We show that the bar recursion operators of Spector and Kohlenbach, considered as third-order functionals acting on total arguments, are not computable in G\u00f6del\u2019s 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 [Formula: see text] within a variety of partial and total models, for instance the Kleene\u2013Kreisel continuous functionals. The paper thus supplies proofs of some results stated in the book by Longley and Normann.<\/jats:p>\n                  <jats:p>The proof of the main theorem makes serious use of the theory of nested sequential procedures (also known as PCF B\u00f6hm 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.<\/jats:p>","DOI":"10.3233\/com-180200","type":"journal-article","created":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T15:54:41Z","timestamp":1548431681000},"page":"119-153","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":2,"title":["Bar recursion is not computable via iteration"],"prefix":"10.1177","volume":"8","author":[{"given":"John","family":"Longley","sequence":"first","affiliation":[{"name":"School of Informatics, University of Edinburgh, 10 Crichton Street, Edinburgh, EH8 9AB, United Kingdom. ;\u00a0"}]}],"member":"179","published-online":{"date-parts":[[2019,1,25]]},"reference":[{"key":"ref001","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"ref002","unstructured":"S.\u00a0Berardi, P.\u00a0Oliva and S.\u00a0Steila, An analysis of the Podelski-Rybalchenko termination theorem via bar recursion,\n                      Journal of Logic and Computation\n                      (2015)."},{"key":"ref003","unstructured":"U.\u00a0Berger, Minimization vs. recursion on the partial continuous functionals, in: In the Scope of Logic, Methodology and Philosophy of Science, Cracow, August 1999, P.\u00a0G\u00e4rdenfors, J.\u00a0Wole\u0144ski and K.\u00a0Kijania-Placek, eds, Kluwer, Dordrecht, 2002, pp.\u00a057\u201364."},{"key":"ref004","unstructured":"J.\u00a0Bergstra, Continuity and computability in finite types, Ph.D. dissertation, University of Utrecht, 1976."},{"key":"ref005","doi-asserted-by":"publisher","DOI":"10.2307\/2274319"},{"key":"ref006","doi-asserted-by":"crossref","unstructured":"M.H.\u00a0Escard\u00f3 and P.\u00a0Oliva, Computing Nash equilibria of unbounded games, in: Proceedings of the Turing Centenary Conference, EPiC Series, Vol.\u00a010, Manchester, 2012, pp.\u00a053\u201365.","DOI":"10.29007\/1wpl"},{"key":"ref007","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2014.82"},{"key":"ref008","doi-asserted-by":"crossref","unstructured":"J.\u00a0Hedges, P.\u00a0Oliva, E.\u00a0Winschel, V.\u00a0Winschel and P.\u00a0Zahn, Higher-order decision theory, in: Proceedings of the 5th International Conference on Algorithmic Decision Theory, 2017.","DOI":"10.1007\/978-3-319-67504-6_17"},{"key":"ref009","unstructured":"J.M.E.\u00a0Hyland, Recursion Theory on the Countable Functionals, D.Phil. Dissertation, University of Oxford, 1975."},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"issue":"1","key":"ref011","first-page":"1","volume":"91","author":"Kleene S.C.","year":"1959","journal-title":"Transactions of the American Mathematical Society"},{"key":"ref012","unstructured":"U.\u00a0Kohlenbach, Theory of Majorizable and Continuous Functionals and their Use for the Extraction of Bounds from Non-Constructive Proofs: Effective Moduli of Uniqueness for Best Approximations from Ineffective Proofs of Uniqueness, Ph.D. dissertation, Frankfurt, 1990."},{"key":"ref013","unstructured":"U.\u00a0Kohlenbach, Applied Proof Theory: Proof Interpretations and Their, Use in Mathematics, Springer-Verlag, 2008."},{"key":"ref014","unstructured":"G.\u00a0Kreisel, Interpretation of analysis by means of constructive functionals of finite types, in: Constructivity in Mathematics: Proceedings of the Colloquium Held in Amsterdam, 1957, A.\u00a0Heyting, ed. North-Holland, Amsterdam, 1959, pp.\u00a0101\u2013128."},{"key":"ref015","unstructured":"G.\u00a0Kreisel, Set theoretic problems suggested by the notion of potential totality, in: Infinitistic Methods, Proceedings of the Symposium on Foundations of Mathematics, Pergamon Press, Warsaw, 1959, pp.\u00a0103\u2013140, Oxford, 1961."},{"key":"ref016","doi-asserted-by":"crossref","unstructured":"J.\u00a0Longley and D.\u00a0Normann, Higher-Order Computability, Theory and Applications of Computability, Springer-Verlag, 2015.","DOI":"10.1007\/978-3-662-47992-6"},{"key":"ref017","unstructured":"J.R.\u00a0Longley, Bar recursion is not T + min definable, Informatics Research Report EDI-INF-RR-1420, University of Edinburgh, 2015."},{"key":"ref018","first-page":"1","volume":"14","author":"Longley J.R.","year":"2018","journal-title":"Logical Methods in Computer Science"},{"key":"ref019","unstructured":"J.R.\u00a0Longley, On the relative expressive power of some sublanguages of PCF, in preparation."},{"key":"ref020","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"ref021","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000340"},{"key":"ref022","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002692"},{"key":"ref024","doi-asserted-by":"publisher","DOI":"10.1007\/BF01876321"},{"key":"ref025","first-page":"123","volume":"23","author":"Scarpellini B.","year":"1971","journal-title":"Compositio Mathematica"},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"C.\u00a0Spector, Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, in: Recursive Function Theory, Proceedings of Symposia in Pure Mathematics, Vol.\u00a05, J. Dekker, ed., AMS, Providence, 1962, pp.\u00a01\u201327. doi:10.1090\/pspum\/005\/0154801.","DOI":"10.1090\/pspum\/005\/0154801"}],"container-title":["Computability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/COM-180200","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/COM-180200","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/COM-180200","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T16:00:00Z","timestamp":1777392000000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/COM-180200"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,25]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,6,17]]}},"alternative-id":["10.3233\/COM-180200"],"URL":"https:\/\/doi.org\/10.3233\/com-180200","relation":{},"ISSN":["2211-3568","2211-3576"],"issn-type":[{"value":"2211-3568","type":"print"},{"value":"2211-3576","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,25]]}}}