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ödel’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 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 Böhm 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.
S.Abramsky, R.Jagadeesan and P.Malacaria, Full abstraction for PCF, Information and Computation163(2) (2000), 409–470. doi:10.1006/inco.2000.2930.
2.
S.Berardi, P.Oliva and S.Steila, An analysis of the Podelski-Rybalchenko termination theorem via bar recursion, Journal of Logic and Computation (2015).
3.
U.Berger, Minimization vs. recursion on the partial continuous functionals, in: In the Scope of Logic, Methodology and Philosophy of Science, Cracow, August 1999, P.Gärdenfors, J.Woleński and K.Kijania-Placek, eds, Kluwer, Dordrecht, 2002, pp. 57–64.
4.
J.Bergstra, Continuity and computability in finite types, Ph.D. dissertation, University of Utrecht, 1976.
5.
M.Bezem, Strongly majorizable functionals of finite type: A model for bar recursion containing discontinuous functionals, Journal of Symbolic Logic50 (1985), 652–660. doi:10.2307/2274319.
6.
M.H.Escardó and P.Oliva, Computing Nash equilibria of unbounded games, in: Proceedings of the Turing Centenary Conference, EPiC Series, Vol. 10, Manchester, 2012, pp. 53–65.
7.
M.H.Escardó and P.Oliva, Bar recursion and products of selection functions, Journal of Symbolic Logic80(1) (2015), 1–28. doi:10.1017/jsl.2014.82.
8.
J.Hedges, P.Oliva, E.Winschel, V.Winschel and P.Zahn, Higher-order decision theory, in: Proceedings of the 5th International Conference on Algorithmic Decision Theory, 2017.
9.
J.M.E.Hyland, Recursion Theory on the Countable Functionals, D.Phil. Dissertation, University of Oxford, 1975.
10.
J.M.E.Hyland and C.-H.L.Ong, On full abstraction for PCF: I, II and III, Information and Computation163 (2000), 285–408. doi:10.1006/inco.2000.2917.
11.
S.C.Kleene, Recursive functionals and quantifiers of finite types I, Transactions of the American Mathematical Society91(1) (1959), 1–52.
12.
U.Kohlenbach, 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.
13.
U.Kohlenbach, Applied Proof Theory: Proof Interpretations and Their, Use in Mathematics, Springer-Verlag, 2008.
14.
G.Kreisel, Interpretation of analysis by means of constructive functionals of finite types, in: Constructivity in Mathematics: Proceedings of the Colloquium Held in Amsterdam, 1957, A.Heyting, ed., North-Holland, Amsterdam, 1959, pp. 101–128.
15.
G.Kreisel, 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. 103–140, Oxford, 1961.
16.
J.Longley and D.Normann, Higher-Order Computability, Theory and Applications of Computability, Springer-Verlag, 2015.
17.
J.R.Longley, Bar recursion is not T + min definable, Informatics Research Report EDI-INF-RR-1420, University of Edinburgh, 2015.
18.
J.R.Longley, The recursion hierarchy for is strict, Logical Methods in Computer Science14(3:8) (2018), 1–51.
19.
J.R.Longley, On the relative expressive power of some sublanguages of , in preparation.
P.Oliva and T.Powell, A constructive interpretation of Ramsey’s theorem via the product of selection functions, Mathematical Structures in Computer Science25(8) (2015), 1755–1778. doi:10.1017/S0960129513000340.
22.
G.D.Plotkin, LCF considered as a programming language, Theoretical Computer Science5(3) (1977), 223–255. doi:10.1016/0304-3975(77)90044-5.
23.
G.D.Plotkin, Full abstraction, totality and PCF, Mathematical Structures in Computer Science9(1) (1999), 1–20. doi:10.1017/S0960129598002692.
24.
V.Yu.Sazonov, Expressibility in D. Scott’s LCF language, Algebra and Logic15(3) (1976), 192–206. doi:10.1007/BF01876321.
25.
B.Scarpellini, A model for barrecursion of higher types, Compositio Mathematica23 (1971), 123–153.
26.
C.Spector, 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. 5, J. Dekker, ed., AMS, Providence, 1962, pp. 1–27. doi:10.1090/pspum/005/0154801.
