Effective Operations of type 2 in PCAs

Abstract

We exhibit a way of “forcing a partial functional to be realizable as effective operation” for arbitrary partial combinatory algebras (pcas). This gives a method of defining new pcas from old ones for some fixed type 2 (partial) functional, where the new partial functions can be viewed as computable relative to that functional. It is shown that this generalizes a notion of computation relative to a functional as defined by Kleene for the natural numbers. The resulting notion of computation can be characterized by a universal property both in the category of pcas and in the lattice of local operators on the corresponding realizability topos. Our result is useful in two ways. For one thing, we expect that the emphasis on forcing the applicative structure to satisfy certain properties yields new methods to tackle problems in complexity theory, for example in connection to higher computability. Second, the methods are defined for abstract notions of computation, which provides a connection with realizability toposes and categories of assemblies. We will see an instance of this in the effective topos using an example of a functional that forces every arithmetical set to be decidable and a local operator defined by A. Pitts in his thesis [The theory of triposes, PhD thesis, Cambridge University, 1981]. As an intermezzo we also prove the convenient result that the two definitions of a pca that are common in the literature are essentially the same.