Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice

TL;DR

This paper introduces a unified parametrized bar recursion framework that encompasses various realizability interpretations of classical analysis, simplifying their comparison and highlighting their common structure.

Contribution

It presents a general parametrized recursor that unifies multiple bar recursion variants used in realizability interpretations of dependent choice, with a uniform proof of their correctness.

Findings

Most existing bar recursive realizability interpretations follow from the framework.

The framework includes interpretations based on Berardi-Bezem-Coquand functional, modified realizability, and selection functions.

It reveals a large family of potential realizability interpretations of dependent choice principles.

Abstract

During the last twenty years or so a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work we present the many variants of bar recursion used in this context as instantiations of a general, parametrised recursor, and give a uniform proof that under certain conditions this recursor realizes a corresponding family of parametrised dependent choice principles. From this proof, the soundness of most of the existing bar recursive realizability interpretations of choice, including those based on the Berardi-Bezem-Coquand functional, modified realizability and the more recent products of selection functions of Escard\'o and Oliva, follows as a simple corollary. We achieve not only a uniform framework in which familiar realizability interpretations of choice can be compared, but show that these represent just simple instances of a large family of potential interpretations of dependent choice principles.