Third-order functionals on partial combinatory algebras (Q2105095)

This paper is concerned with computability on higher-order functions in the context of partial combinatory algebras (PCAs). The paper [\textit{J. van Oosten}, Notre Dame J. Formal Logic 47, No. 3, 311--318 (2006; Zbl 1113.03014)] offered a notion of oracle computability for general PCAs, while the paper [\textit{E. Faber} and \textit{J. van Oosten}, Computability 5, No. 2, 127--146 (2016; Zbl 1437.03136)] generalized this to second-order functional. This paper is now concerned with the third-order case. It was shown in [\textit{J. van Oosten}, Notre Dame J. Formal Logic 52, No. 4, 431--448 (2011; Zbl 1248.03026)] that, for each PCA \(A\), there is another PCA \(\mathcal{B}A\) whose elements are partial functions on \(A\). The main strategy in this paper is to view higher-order functional on \(A\) as lower-order ones on \(\mathcal{B}A\). The synopsis of the paper goes as follows: \begin{itemize} \item[\S 2] introduces partial combinatory algebras and the realizability toposes \textsf{RT}. In this paper, PCAs are always relative and ordered. \item[\S 3] introduces the relevant morphisms between PCAs, yielding a preorder-enriched bicategory of PCAs. \item[\S 4] revisits the paper [\textit{J. van Oosten}, Notre Dame J. Formal Logic 47, No. 3, 311--318 (2006; Zbl 1113.03014)], showing how to freely adjoin a partial function \(f:A\rightarrow A\) to get a new PCA \(A[f]\). \item[\S 5] introduces the PCA \(\mathcal{B}A\) of partial functions as in [\textit{J. van Oosten}, Notre Dame J. Formal Logic 52, No. 4, 431--448 (2011; Zbl 1248.03026)]. One of the central views of this paper is that \(\mathcal{B}A\) is best as a relative, ordered PCA, even if \(A\) itself is an ordinary PCA. It is shown how, at the level of realizability toposes, \(A[f]\) may be reconstructed using the construction \(\mathcal{B}-\), slicing, and image toposes, depending heavily on the fact that there is a geometric surjection \[ \mathsf{RT}(\mathcal{B}A)\rightarrow\mathsf{RT}(A) \] \item[\S 6] treats the second-order case, where the construction in [\textit{E. Faber} and \textit{J. van Oosten}, Computability 5, No. 2, 127--146 (2016; Zbl 1437.03136)] is reinterpreted as a construction actually taking place in \(\mathcal{B}A\). The author gives an example demonstrating that the elements of \(\mathcal{B}A\) enjoy a kind of double life in the sense that they are surely elements of \(\mathcal{B}A\), while, for each \(\alpha\in\mathcal{B}A\), there are other elements from \(\mathcal{B}A\) computing \(\alpha\) in a specific sense. \item[\S 7] is concerned with the third-order case. \end{itemize}