The Herbrand Functional Interpretation of the Double Negation Shift

TL;DR

This paper generalizes selection functions over strong monads, showing their relation to the continuation monad and Spector's bar recursion, and demonstrates their role in the Herbrand functional interpretation of the double negation shift.

Contribution

It introduces a generalized framework for selection functions over strong monads and connects them to established recursion principles and interpretations.

Findings

The monad $J^T_R$ is strong and embeds into the continuation monad.

Explicitly controlled product of $T$-selection functions is definable from bar recursion.

When $T$ is the finite power set monad, the product computes a witness for the Herbrand interpretation.

Abstract

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$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of $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)$ the explicitly controlled product of $T$-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.