The Herbrand Functional Interpretation of the Double Negation Shift

This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$\mathrm{.}Itisassumedthroughoutthat$R$isa$T$-algebra\mathrm{.}Weshowthat$J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$\mathrm{.}Weusethistoderivethattheexplicitlycontrolledproductof$T$-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector’s bar recursion. We then prove several properties of this product in the special case when $T$ is the finite power set monad $\mathcal{P}(\cdot )$. These are used to show that when $T X = {\mathcal P}(X)$theexplicitlycontrolledproductof$T$-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.