Computability relative to a partial function f on the natural numbers can be formalized using the notion of an oracle for this function f. This can be generalized to arbitrary partial combinatory algebras, yielding a notion of ‘adjoining a partial function to a partial combinatory algebra A’. A similar construction is known for second-order functionals, but the third-order case is more difficult. In this paper, we prove several results for this third-order case. Given a third-order functional Φ on a partial combinatory algebra A, we show how to construct a partial combinatory algebra A[Φ] where Φ is ‘computable’, and which has a ‘lax’ factorization property (Theorem 7.3 below). Moreover, we show that, on the level of first-order functions, the effect of making a third-order functional computable can be described as adding an oracle for a first-order function.

Abstract We consider two preorder-enriched categories of ordered partial combinatory algebras: OPCA, where the arrows are functional (i.e., projective) morphisms, and OPCA†, where the arrows are applicative morphisms. We show that OPCA has small products and finite biproducts, and that OPCA† has finite coproducts, all in a suitable 2-categorical sense. On the other hand, OPCA† lacks all nontrivial binary products. We deduce from this that the pushout, over Set, of two nontrivial realizability toposes is never a realizability topos. In contrast, we show that nontrivial subtoposes of realizability toposes are closed under pushouts over Set.