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.

Keywords

Partial combinatory algebra computability theory Turing degree effective operation computable functional realizability topos realizability

1. Introduction

Effective operations have originally been studied in computability theory, with as famous results the theorems of Myhill–Shepherdson and Rice–Shapiro. They have also been studied in relation to computable functionals (e.g. see [3]), although the two notions are not quite the same. For example, it is known that not every functional that can be realized as effective operation is also a computable functional ([3]). In realizability, partial combinatory algebras (pcas) are used as models for abstract Turing machines. The notion of effective operation can be extended to pcas in a straightforward way. In this paper, we discuss effective operations on arbitrary partial combinatory algebras, and present a way to force a functional to be realizable as effective operation: for a (partial) functional $F : A^{A} \to A$ , where A is a pca, we construct a pca $A [F]$ for which F, restricted to the total functions on $A [F]$ , is realizable as an effective operation. In Theorem 3.1, we characterize $A [F]$ by a universal property in the category of pcas.

In [8], Kleene introduced the notion of a computable functional, and with it the notion of computability relative to a functional. It turns out that for $A = K_{1}$ , Kleene’s first model, the functions computable in $K_{1} [F]$ are precisely the functions computable relative to F in Kleene’s sense. This yields an alternative approach to computation in a type 2 functional that generalizes to arbitrary pcas.

The recursive application defined by $A [F]$ can also be characterized in the lattice of local operators on $RT (A)$ , the realizability topos on A. This is shown in Theorem 6.1. The theory of recursive hierarchies of functionals (e.g. see [4]) can therefore be applied to study subtoposes of realizability toposes, especially their computational complexity.

As an example, we look at a specific local operator J due to A. Pitts that is studied in [15]. It turns out that the functions “computable in J” are precisely the functions computable relative to a certain functional.

On the way we also prove that a strengthening of our definition of a pca, that we call strict pcas, is (up to applicative isomorphism) not a proper strengthening at all. This is posed as an open question in [2]. The result is convenient, since in the literature there has not been wide consensus on the definition of pca; several authors have been using strict pcas by default. We will catch a glimpse of the usefulness of this result by exhibiting a pca that at first sight seems a long way from being strict (Proposition 6.3).

In the last section, we discuss the generalization of our results to higher types. Although Kleene’s definitions of recursive functionals generalize to higher types, the connection with effective operations gets lost. A generalization of our results on effective operations seems to demand for a more complicated method of “forcing” than what we have described for a type two functional. Further investigations of this kind could thus be useful in computability theory and the study of realizability toposes.

2. Preliminaries

We start by reviewing the definition of a partial combinatory algebra and some basic constructions.

Definition 2.1.
A partial applicative structure on a set A is a partial map $A \times A \to A$ that we denote by $\begin{matrix} (a, b) \mapsto a b . \end{matrix}$
We write $a b ↓$ to say that $a b$ is defined, $a b = c$ to say that $a b$ is defined and has value c. In writing compositions of the application, we adopt the convention of associating to the left, so: $\begin{matrix} a b c d = (((a b) c) d) . \end{matrix}$

For $V = {x_{0}, x_{1}, \dots}$ an enumerable set of variables, we define the set of terms by:
Definition 2.2.
For all $a \in A$ , $x \in V$
a is a term;

x is a term;

For t, s terms, $(t s)$ is a term.

A term t without free variables is called closed and might denote or not. This is defined inductively:
a denotes and has value a;

If t denotes and has value a, and s denotes and has value b, and $a b = c$ , then $(t s)$ denotes and has value c.
We write $t ↓$ if t denotes, and $t = a$ if t denotes and has value a. We write $t ≲ s$ if $s ↓$ implies that $t ↓$ , and in that case $s = t$ . We write $t ≃ s$ if $t ≲ s$ and $s ≲ t$ . As a warning, note that other authors sometimes define the relation “≲” the other way around (this is comparable to the two conventions used to order forcing conditions in set theory). Here, we stick to the convention used in [14].

We denote a term t with free variables $x_{1}, \dots, x_{n}$ by $\begin{matrix} t (x_{1}, \dots, x_{n}) . \end{matrix}$ For $a_{1}, \dots, a_{n} \in A$ , we can substitute $x_{1}, \dots, x_{n}$ by $a_{1}, \dots, a_{n}$ , resulting in a closed term $t (a_{1}, \dots, a_{n})$ .
Definition 2.3.
A partial combinatory algebra is a partial applicative structure A, with elements $k, s \in A$ such that for all $a, b \in A$ :
$s a b ↓$ ;

$k a b = a$ ;

$s a b c ≲ a c (b c)$ .

We also say that the applicative structure on A is combinatory complete.
Example 2.1.
There are several examples of pcas, [14] treats a lot of them. Here we just list a few with little explanation:
The trivial pca, $A = {}$ with $ * = $ .

Kleene’s first model* $K_{1}$ , with underlying set $N$ . Application is given by: $\begin{matrix} n m ≃ ϕ_{n} (m), \end{matrix}$ where $ϕ_{n}$ is the nth partial function for some model of computation and coding.

An introduction to partial combinatory algebras and its basic properties can be found in Chapter 1 of [14]. Here we will just quickly present some tools that we need later on, the proofs can all be found in [14]. For a pca A, an element $a \in A$ defines a partial function $A \to A$ by: $\begin{matrix} b \mapsto a b . \end{matrix}$ We say that a is an index for this partial function. By abuse of language, we sometimes say that a is a partial (computable) function.

An important result for pcas is the recursion theorem:
Theorem 2.1 (Recursion theorem).

For every $f \in A$ , there exists e such that for all $a \in A$ : $\begin{matrix} e a ≲ f e a . \end{matrix}$

Also important is the fact that a pca is combinatory complete. This means that for every term $t (x_{1}, \dots, x_{n})$ with free variables $x_{1}, \dots, x_{n}$ , there is an element $⟨ x_{1} \dots x_{n} ⟩ t \in A$ such that for all $a_{1}, \dots, a_{n} \in A$ : $\begin{array}{l} (1) & (⟨ x_{1} \dots x_{n} ⟩ t) a_{1} \dots a_{n - 1} ↓, \\ (2) & (⟨ x_{1} \dots x_{n} ⟩ t) a_{1} \dots a_{n - 1} a_{n} ≲ t (a_{1}, \dots, a_{n}) . \end{array}$ The notation $⟨ x_{1} \dots x_{n} ⟩ t$ should remind the reader of λ-abstraction in λ-calculus. We use a different notation because it is slightly different from λ-abstraction, but it is applied in the same way.

Besides $k$ and $s$ , we identify (a choice of) other canonical elements of A, among which:

Boolean combinators $T$ and $F$ that satisfy for all $a, b \in A$ : $\begin{array}{l} (3) & T a b = a, \\ (4) & F a b = b . \end{array}$ Indeed, one can take $T = k$ .

Using combinatory completeness and the Boolean combinators, we can define if/else statements: for t, s closed terms: $\begin{matrix} (⟨ v ⟩ v (⟨ x ⟩ t) (⟨ x ⟩ s) k) b ≲ \{\begin{matrix} t & if b = T, \\ s & if b = F, \\ unspecified & otherwise . \end{matrix} \end{matrix}$ For legibility, we denote a term like $v (⟨ x ⟩ t) (⟨ x ⟩ s) k$ by $\begin{matrix} if v then t else s . \end{matrix}$

The pairing combinator $p$ together with projections $p_{0}$ , $p_{1}$ : $\begin{array}{l} (5) & p_{0} (p a b) = a, \\ (6) & p_{1} (p a b) = b . \end{array}$

The Curry numerals: each pca contains representables of the natural numbers, i.e. for any $n \in N$ an element $\overline{n} \in A$ . It is a basic result (for a proof, see [14]) that, for every k, there is for every k-ary partial recursive function $F : N^{k} \to N$ an index $f \in A$ such that for all $(n_{1}, \dots, n_{k}) \in dom F$ : $\begin{matrix} f \overline{n_{1}} \dots \overline{n_{k}} = \overline{F (n_{1}, \dots, n_{k})} . \end{matrix}$

When there is chance of confusion, we decorate (choices of) canonical elements by a subscript to denote the pca to which it belongs, e.g. $k_{A}$ , $s_{A}$ , $T_{A}$ , etc.

We can also code tuples of elements in a computable way. That is, there is an index $t \in A$ such that for all $n \in N$ , $u_{0}, \dots, u_{n} \in A$ we can code a tuple $\begin{matrix} [u_{0}, \dots, u_{n}] : = t \overline{n + 1} u_{0} \dots u_{n} \in A \end{matrix}$ such that projection, concatenation of tuples, and a length function (that yields the length of a tuple as a curry numeral) are all computable. We denote concatenation by ∗: $\begin{matrix} [u_{0}, \dots, u_{i}] * [u_{i + 1}, \dots, u_{n}] = [u_{0}, \dots, u_{n}] \end{matrix}$ and for $u = [u_{0}, \dots, u_{n}]$ , we write $u^{< i + 1}$ for $[u_{0}, \dots, u_{i}]$ . These basic operations can all be done computably and uniformly in the variables.

There is a notion of morphism between partial combinatory algebras due to John Longley (see [9]), called applicative morphism. In the following definition, we adopt the following notation: for a total relation $R : X \to Y$ between sets X and Y, we denote for every $x \in X$ by $R (x)$ the set: $\begin{matrix} {y \in Y ∣ x R y} . \end{matrix}$ For A a pca, $a \in A$ and $P \subseteq A$ a subset, we write $a P ↓$ if for all $b \in P$ , $a b ↓$ , and in that case $\begin{matrix} a P : = {a b ∣ b \in P} . \end{matrix}$ For $P, Q \subseteq A$ , we write $P Q ↓$ if for all $b \in P$ , $b^{'} \in Q$ , $b b^{'} ↓$ , and in that case $\begin{matrix} P Q = {b b^{'} | b \in P, b^{'} \in Q} . \end{matrix}$ Whenever we write compositions of these applications of an element and a subset, or a subset and a subset, we again associate to the left.

Definition 2.4 (Longley).

Let A, B be pcas. An applicative morphism $γ : A \to B$ is a total relation from A to B, together with an element $r \in B$ such that whenever $a, a^{'} \in A$ and $a a^{'} ↓$ , we have: $\begin{matrix} r γ (a) γ (a^{'}) ↓ and r γ (a) γ (a^{'}) \subseteq γ (a a^{'}) . \end{matrix}$ The element r is said to realize γ.

An applicative morphism γ is decidable if there is $d \in B$ such that $\begin{array}{l} (7) & d γ (T_{A}) = {T_{B}}, \\ (8) & d γ (F_{A}) = {F_{B}} . \end{array}$ We call d a decider for γ.

The composition of two applicative morphisms is defined by composition of the relations, and one can verify that this is again an applicative morphism. There is a pre-order on applicative morphisms defined as follows: for $γ : A \to B$ , $δ : A \to B$ , write $γ ⪯ δ$ when there is $t \in B$ such that for all $a \in A$ : $\begin{matrix} t γ (a) \subseteq δ (a) . \end{matrix}$ We write $γ ≃ δ$ if $γ ⪯ δ$ and $δ ⪯ γ$ , in this case γ and δ are equivalent. One can show that this pre-order is preserved by composition on both sides. We thus obtain a pre-order enriched category PCA consisting of partial combinatory algebras as objects, and applicative morphisms as arrows. The identity arrow for a pca A is denoted by $ι_{A}$ and given by the identity relation on A.

Note 2.1.
As remarked in the Introduction, Definition 2.3 is weaker than the definition that is used in some other literature (including [14]). However, it will be a consequence of Theorem 5.1 below that the corresponding categories of pcas, with morphisms as above, are equivalent.

For a pca A, we define a set ${PR}_{A}$ by: $\begin{matrix} {PR}_{A} = {f : A \to A partial ∣ (\exists a \in A) (\forall b \in A) a b ≲ f (b)} . \end{matrix}$ We also define a function $I_{1}^{A} : {PR}_{A} \to P (A)$ (here $P (A)$ is the powerset of A) by: $\begin{matrix} I_{1}^{A} (f) = {a \in A ∣ (\forall b \in A) a b ≲ f (b)} . \end{matrix}$ For $γ : A \to B$ an applicative morphism, we define a set ${PR}_{γ}$ by: $\begin{matrix} (9) & {PR}_{γ} : {f : A \to A partial ∣ (\exists b \in B) (\forall a \in A) f (a) ↓ \Rightarrow b γ (a) \subseteq γ (f (a))} . \end{matrix}$ Lastly, we also define a function $I_{1}^{γ} : {PR}_{γ} \to P (B)$ by: $\begin{matrix} I_{1}^{γ} (f) = {b \in B ∣ (\forall a \in A) f (a) ↓ \Rightarrow b γ (a) \subseteq γ (f (a))} . \end{matrix}$ Observe that ${PR}_{A} = {PR}_{ι_{A}}$ .

The following result by the second author (see [13] or [14]) tells us that we can adjoin any partial function $f : A \to A$ to a pca A, to obtain a pca $A [f]$ in which f has an index. This generalizes the notion of a Turing machine with oracle from ordinary computability theory to pcas.
Theorem 2.2 ([13]).

For A a pca and $f : A \to A$ a partial function, there exists a pca $A [f]$ defined on the set A such that the identity on A is a decidable applicative morphism $ι_{f} : A \to A [f]$ , and:

$f \in {PR}_{A [f]} = {PR}_{ι_{f}}$ .

Whenever $γ : A \to B$ is a decidable applicative morphism such that $f \in {PR}_{γ}$ , there exists a decidable $γ_{f} : A [f] \to B$ such that $γ_{f} \circ ι_{f} = γ$ . Moreover, if $δ : A [f] \to B$ is a decidable applicative morphism such that $δ \circ ι_{f} ≃ γ$ , then $δ ≃ γ_{f}$ .

The proof of the above theorem is done by defining an applicative structure on A using dialogues:

Definition 2.5.
Let $f : A \to A$ be a partial function, and $a, b \in A$ . An f-dialogue between a and b is an element $u = [u_{0}, \dots, u_{n}] \in A$ such that for all $i ⩽ n$ : $\begin{matrix} a ([b] * u^{< i}) = p F v_{i}, \end{matrix}$ where $f (v_{i})$ is defined and $f (v_{i}) = u_{i}$ .

An f-dialogue u between a and b halts if there exists $c \in A$ such that $\begin{matrix} a ([b] * u) = p T c . \end{matrix}$ We write $a \cdot^{f} b ↓$ if there is a (necessarily unique) halting f-dialogue u between a and b, and $a \cdot^{f} b = c$ if $a \cdot^{f} b ↓$ and $\begin{matrix} a ([b] * u) = p T c, \end{matrix}$ where u is a halting f-dialogue between a and b.

The applicative structure on $A [f]$ is then given by $(a, b) \mapsto a \cdot^{f} b$ . For a full proof of combinatory completeness, see [14] or [13]. Note that these sources use the strict version of a pca (Definition 5.1), but the proofs work without any modification (alternatively, one can apply Theorem 5.1). The following corollary corresponds to Corollary 1.3 in [13]: Corollary 2.1.
Let A be a pca.
If $f \in {PR}_{A}$ , then $A [f]$ and A are isomorphic pcas.

If $f, g : A \to A$ are partial functions, then $A [f] [g]$ and $A [g] [f]$ are isomorphic.

If $K_{1}^{f}$ is the pca of partial recursive application with an oracle for f, then $K_{1}^{f}$ is isomorphic to $K_{1} [f]$ .

3. Effective operations

We will now define the set of effective operations on pcas. For any pca A, let ${Tot}_{A}$ be the subset of ${PR}_{A}$ consisting of all total functions: $\begin{matrix} {Tot}_{A} = {f \in {PR}_{A} ∣ f is total} . \end{matrix}$ Similarly, define for any γ the subset ${Tot}_{γ} \subseteq {PR}_{γ}$ consisting of all total functions in ${PR}_{γ}$ .

Definition 3.1 (Effective operation).

For a pca A, we define the set $E_{A}$ of effective operations in A by: $\begin{array}{l} (10) & E_{A} = & {F : D \to A ∣ D \subseteq {Tot}_{A} and (\exists a \in A) (\forall f \in {Tot}_{A}) \\ (11) & f \in D ⟹ (a I_{1} (f) ↓ and a I_{1}^{A} (f) = {F (f)})} . \end{array}$ Define a function $I_{2}^{A} : E_{A} \to A$ by: $\begin{matrix} I_{2}^{A} (F) = {a ∣ (\forall f \in dom F) (\forall b \in I_{1}^{A} (f)) (a b = F (f))} . \end{matrix}$

Similarly, for $γ : A \to B$ an applicative morphism we define the set $E_{γ}$ of effective operations relative to γ by: $\begin{array}{l} (12) & E_{γ} = & {F : D \to A ∣ D \subseteq {Tot}_{γ} and (\exists b \in B) (\forall f \in {Tot}_{γ}) \\ (13) & f \in D ⟹ (b I_{1}^{γ} (f) ↓ and b I_{1}^{γ} (f) \subseteq γ (F (f)))} . \end{array}$

Example 3.1.
As an example, we look at the following functional $E : A^{A} \to A$ , where A is an arbitrary pca, $\begin{matrix} E (α) = \{\begin{matrix} T & if (\exists a) α (a) = T, \\ F & otherwise . \end{matrix} \end{matrix}$ For $A = K_{1}$ , it is easily seen that the above (restricted to the total computable functions) is not an effective operation (otherwise the halting problem is decidable). However, the construction below shows that there are a lot of pcas in which E, when restricted, is an effective operation.

The statement of the following theorem is very similar to Theorem 2.2. Theorem 3.1.
Let A be a pca, and $F : A^{A} \to A$ a (partial) functional. Then there exists a pca $A [F]$ defined on the set A such that the identity relation on A is a decidable applicative morphism $ι_{F} : A \to A [F]$ and:
$F ↾ {Tot}_{A [F]} \in E_{A [F]} = E_{ι_{F}}$ ;

Whenever $γ : A \to B$ is a decidable applicative morphism such that $F ↾ {Tot}_{γ} \in E_{γ}$ , there exists a unique (up to equivalence) decidable applicative morphism $γ_{F} : A [F] \to B$ such that $γ_{F} \circ ι_{F} = γ$ . Moreover, if $δ : A [F] \to B$ is a decidable applicative morphism such that $δ \circ ι_{F} ≃ γ$ , then $δ ≃ γ_{F}$ .

Remark 3.1.
Before embarking on the proof, we would like to clarify an issue that might at this point have confused the reader. It may seem that we are treating a partial functional $F : A^{A} \to A$ and an effective operation on the same level (up to restriction), which is why we say that our construction “forces F to be realizable as effective operation”. However, since for any pca A, $| {Tot}_{A} | = | A | < | A^{A} |$ , F may be defined on a lot more functions than $A [F]$ could ever contain. So F will always contain more information than the effective operation we construct from it.

However, ${Tot}_{A [F]}$ will usually contain functions that were not in ${Tot}_{A}$ , so we cannot restrict F beforehand. Indeed, $A [F ↾ {Tot}_{A}]$ is quite different from $A [F]$ ! Take for example the functional E above. In this case, $K_{1} [E ↾ {Tot}_{K_{1}}] = K_{1} [\emptyset^{'}]$ (here $\emptyset^{'}$ is the first jump of the empty set), whereas we will see (Corollary 4.1) that $K_{1} [E]$ computes all hyperarithmetical functions.

It may be better to formulate the above distinction in categorical terms (see Section 6.1). We could define an effective operation as a partial arrow $A^{A} \leftarrow D \to A$ in a category of assemblies on A. The above theorem then constructs a pca $A [F]$ for which the category of assemblies is a reflective subcategory of the assemblies on A, in which the partial functional $F : A^{A} \to A$ is realizable as partial arrow ${A [F]}^{A [F]} \leftarrow D \to A [F]$ . This corresponds to (i) in the above theorem. In fact, this reflective subcategory is induced by a local operator on the realizability topos $RT (A)$ , and this local operator turns out to be the smallest such that F is realizable. This is the content of Theorem 6.1 and corresponds to (ii) of the above theorem.
Proof.
We will construct $A [F]$ as $A [f]$ for $\begin{matrix} f = ⋃_{α} f_{α}, \end{matrix}$ where ${f_{α}}_{α}$ is a compatible family of partial functions indexed by the ordinals. We define this family by transfinite induction. For all $a, b \in A$ , we let:
$f_{0} = \emptyset$ ;

$f_{α + 1} (a) = b$ whenever there exists $g \in {Tot}_{A [f_{α}]}$ such that $a \in I_{1}^{A [f_{α}]} (g)$ and $F (g) = b$ ;

For $λ > 0$ a limit ordinal, $f_{λ} = ⋃_{α < λ} f_{α}$ .
It is not hard to see that this indeed defines a compatible family of partial functions. So $f = ⋃_{α} f_{α}$ is a partial function, and we define $A [F] : = A [f]$ . We denote the application in $A [F]$ by $\cdot^{F}$ .

For part (i), suppose $g \in {Tot}_{A [F]}$ , $a \in I_{1}^{A [F]} (g)$ , and $F (g)$ is defined. Then it is not hard to see that there is α such that $g \in {Tot}_{A [f_{α}]}$ , $a \in I_{1}^{A [f_{α}]} (g)$ . Then $f_{α + 1} (a) = F (g)$ , hence $f (a) = F (g)$ . Indeed, F is an effective operation in $A [F]$ .

For part (ii), suppose $γ : A \to B$ is a decidable applicative morphism such that $F \in E_{γ}$ . Let $r_{F} \in I_{2}^{γ} (F)$ . Denote the realizer for γ by r. Let $d$ be the decider for γ. Let $c$ be such that for all $x \in γ (a)$ , $v \in γ (u)$ , $c x y \in γ ([a] * u)$ . Let $c^{'}$ be such that for all $y \in γ (a)$ , $x \in γ (u)$ , $c^{'} x y \in γ (u * [a])$ . Let $q_{0}$ , $q_{1}$ be such that for all $x \in γ (a)$ , $q_{0} x \in γ (p_{0} a)$ , $q_{1} x \in γ (p_{1} a)$ . By the recursion theorem, let $e \in B$ be such that $\begin{array}{l} (14) & e x v ≲ & if d q_{0} (r e (c x v)) then q_{1} (r e (c x v)) \\ (15) & else e x (c^{'} v (r_{F} (r (q_{1} (r e (c x v)))))) . \end{array}$

Then one can verify that for $v \in γ ([])$ , we have for all $e \in γ (a)$ , $x \in γ (a^{'})$ such that $a \cdot^{f} a^{'} ↓$ : $\begin{matrix} e x v \in γ (a \cdot^{f} a^{'}) . \end{matrix}$ Essential is that if $a \in I_{1}^{A [F]} (f)$ , then for $b \in γ (a)$ , $r b \in I_{1}^{γ} (f)$ .

So by the above, $⟨ x y ⟩ x y v$ realizes γ as an applicative morphism $γ_{F} : A [F] \to B$ , and the fact that $γ = γ_{F} \circ ι_{F}$ is obvious.

Uniqueness is easy to check. □
Remark 3.2.
The construction of $A [F]$ can be thought of as a construction in stages: we say that $a \cdot^{F} b ↓$ at stage α if $a \cdot^{f_{α}} b ↓$ . In proofs of statements about $A [F]$ , we will often use induction on the stage at which a term denotes. The infinitary nature of computation relative in a functional, as remarked by Kleene in [8], is reflected by this construction in (transfinitely many) stages.
Example 3.2.
We again take a look at the functional E from Example 3.1. For any pca A, E is an effective operation in $A [E]$ . As a consequence, the computable predicates in $A [E]$ are closed under existential quantification: suppose $p \in A [E]$ is a total function in 2 variables, taking values in ${T, F}$ . Then: $\begin{matrix} Q (n) : = (\exists m) p n m \end{matrix}$ is clearly also a recursive predicate in $A [E]$ , so it has some index $q \in A [E]$ .

For $A = K_{1}$ , this produces a familiar (see [8]) result. Namely, it follows (by taking complements) that every arithmetical subset of $N$ is computable in $K_{1} [E]$ . We will see below that the total functions in $K_{1} [E]$ are in fact precisely the hyperarithmetical functions.
Remark 3.3.
One may want to define, for functionals $F, G : A^{A} \to A$ , a pca $A [F, G]$ in which F, G are both effective operations. It will not work to define this as $A [F] [G]$ . This follows the same reasoning as in Remark 3.1. In $A [F] [G]$ , only $F ↾ {Tot}_{A [F]}$ is realizable, whereas we want $F ↾ {Tot}_{A [F] [G]}$ to be realizable. However, if one codes any tuple of functionals into one functional H (e.g. $H (g) = p F (g) G (g)$ ), then $A [H]$ will satisfy the required properties and the analogue of Theorem 2.2 for such a tuple holds.

4. Effective operations and Kleene computability

In [8], Kleene developed a recursion theory for functionals, which included a notion of computability relative to a functional. A short overview of this theory, as well as comparisons to other notions of higher-type computation can be found in [10].

In this section we will show that a total function $f : N \to N$ is computable relative to a functional $F : N^{N} \to N$ (in Kleene’s sense) if and only if it has an index in $K_{1} [F]$ . This result will be almost immediate, since (as we will see) Kleene’s indexed set of functions computable in F is basically an explicit model of $K_{1} [F]$ . Our construction has the advantage of being independent of any explicit model of $K_{1}$ and avoids a lot of technicalities. Moreover, there is the immediate generalization to arbitrary pcas and the connection to realizability.

In his paper, Kleene defined an $N$ -indexed set of functions that may take tuples of arguments of all finite types. The definition consists of nine inductive rules, named (S1)–(S9). A function with index e is denoted by ${e}$ . A function $g : N \to N$ is then computable relative to the functional $F : N^{N} \to N$ if there is an index $e \in N$ such that for all $n \in N$ : $\begin{matrix} {e} (n, F) = g (n) . \end{matrix}$ Instead of defining Kleene’s (S1)–(S9) in full generality, we will just state eight derived rules that define the indexed set of functions computable relative to some functional F according to Kleene. The rule (S7) is missing since that applies specifically to type 1 arguments, and we only consider a specific type 2 oracle.

Definition 4.1.
Let $F : N^{N} \to N$ be a functional. Also fix some primitive recursive coding of tuples $⟨ - ⟩ : N^{< ω} \to N$ . We define an indexed set of partial functions $N^{< ω} \to N$ by the following rules: for all $n, m \in N$ :
Successor function: ${⟨ 1, 1 ⟩} (n) = n + 1$ .

Constant function: ${⟨ 2, 1, m ⟩} (n) = m$ .

Projection: for all $n_{1}, \dots, n_{m} \in N$ , ${⟨ 3, m ⟩} (n_{1}, \dots, n_{m}) = n_{1}$ .

Composition: For $g, h \in N$ , all $k, n_{1}, \dots, n_{k} \in N$ : $\begin{matrix} {⟨ 4, k, g, h ⟩} (n_{1}, \dots, n_{k}) ≃ {g} ({h} (n_{1}, \dots, n_{k}), n_{1}, \dots, n_{k}) . \end{matrix}$

Primitive recursion: For any $g, h \in N$ , if $m = ⟨ 5, 2, g, h ⟩$ then for all k: $\begin{array}{l} (16) & {m} (0, n) ≃ {g} (n), \\ (17) & {m} (k + 1, n) ≃ {h} (k, {m} (k, n), n) . \end{array}$

Permutation of arguments: For any $g \in N$ , $1 ⩽ k < r$ and $n_{1}, \dots, n_{r} \in N$ : $\begin{matrix} {⟨ 6, r, k, g ⟩} (n_{1}, \dots, n_{r}) ≃ {g} (n_{k + 1}, n_{1}, \dots, n_{k}, n_{k + 2}, \dots, n_{r}) . \end{matrix}$

Application of F: For every $h, e \in N$ : $\begin{matrix} {⟨ 8, 1, h ⟩} (n) ≃ F (λ k . {h} (k, n)) . \end{matrix}$

Index vocation: for all $m, k, l, n_{1}, \dots, n_{k + l} \in N$ $\begin{matrix} {⟨ 9, k, l ⟩} (m, n_{1}, \dots, n_{k + l}) ≃ {m} (n_{1}, \dots, n_{k}) . \end{matrix}$

Above, $a ≃ b$ has the same meaning as before: the right-hand side is defined if and only if the left-hand side is defined, and when this is the case both sides are equal.

In what follows, we assume that we have fixed some functional $F : N^{N} \to N$ , and defined the partial map ${-} (-) : N \times N \to N$ according to the above.
Theorem 4.1.
The partial map ${-} (-) : N \times N \to N$ defines a partial combinatory algebra $K_{1}^{F}$ .
Proof.
Tedious exercise using the clauses in Definition 4.1. □

The following can be viewed as the type 2 analogue of Corollary 2.1(3).
Theorem 4.2.
There is an isomorphism of pcas $K_{1} [F] ≅ K_{1}^{F}$ .
Proof.
By Church’s thesis, the identity relation on $N$ is an applicative morphism $γ : K_{1} \to K_{1}^{F}$ . It is easy to see that $F \in E_{γ}$ . By Theorem 3.1, the identity relation on $N$ is an applicative morphism $γ_{F} : K_{1} [F] \to K_{1}^{F}$ .

It is not hard to show that we can define the application in $K_{1}^{F}$ computably in $K_{1} [F]$ using the clauses of Definition 4.1 and the recursion theorem when needed. So the identity relation on $N$ is also an applicative morphism $K_{1}^{F} \to K_{1} [F]$ . Therefore $K_{1} [F] ≅ K_{1}^{F}$ . □
Corollary 4.1.
Let E be as in Example 3.1 for $A = K_{1}$ . The total functions in $K_{1} [E]$ are precisely the hyperarithmetical functions.
Proof.
This follows from Theorem 4.2 and the corresponding fact for $K_{1}^{E}$ , which is Theorem XLVIII in [8]. □

The above corollary is what we can deduce from Kleene’s original paper on recursive functionals. However, we can do a little better using the results of Hinman’s approach in [4]. There, the domains of the $N$ -indexed partial functions $N \to N$ “computable in E” are precisely the $Π_{1}^{1}$ -sets. Here we can prove something similar. In the context of pcas and applicative morphisms, domains of partial recursive functions are not particularly well-behaved (we have to impose more conditions on morphisms to preserve this structure, see for example the discussion of dominances in [9]). Theorem 5.1 also exemplifies this fact. We therefore avoid domains, and show the following instead: Proposition 4.1.
The application in $K_{1} [E]$ is $Π_{1}^{1}$ -complete.
Proof.
We show here that the application function is $Π_{1}^{1}$ , since that does not follow immediately from Hinman’s results. Let $r \in N$ be the uniform index for f in $K_{1} [f]$ , for any f. Recall that $K_{1} [E] = K_{1} [g]$ , where we defined g in stages. We will show that g is $Π_{1}^{1}$ . Let e be an index such that whenever ϕ is the characteristic function of the graph of a partial function $f : A \to A$ , then for all $b, x \in K_{1}$ : $\begin{matrix} e b \cdot^{ϕ} x ≃ b \cdot^{f} x . \end{matrix}$ It is easy to see that such e exists; since $N$ is enumerable, we can just “wait” for values of f to appear in the graph.

Define the following predicate on $N \times N^{N}$ : $\begin{matrix} (18) & Φ ([b, i], X) = (\forall s \exists t \forall y) : (e b \cdot^{X} s ↓ \land (e b \cdot^{X} t = 0 \lor i = 1) \land (e b \cdot^{X} y \neq 0 \lor i = 0)) . \end{matrix}$ It is not hard to see that Φ is $Π_{1}^{1}$ (in fact it is arithmetical) (to work out the details, one needs to use Kleene’s T-predicate and existential quantification over dialogues). Let G be the characteristic function of the graph of g. Now we claim: $\begin{matrix} (19) & G ([b, i]) ⟺ (\forall X) (\exists p, j) (Φ ([p, j], X) ⟹ X ([p, j])) ⟹ X ([b, i]) . \end{matrix}$ Proof of claim.
First, observe: $\begin{array}{l} (20) & Φ ([b, i], G) & ⟺ (\forall s) (\exists t \forall y) e b \cdot^{G} s ↓ \land (e b \cdot^{G} t = 0 \lor i = 1) \land (e b \cdot^{G} y \neq 0 \lor i = 0) \\ (21) & ⟺ (\forall s) (\exists t \forall y) b \cdot^{g} s ↓ \land (b \cdot^{g} t = 0 \lor i = 1) \land (b \cdot^{g} y \neq 0 \lor i = 0) \\ (22) & ⟺ G ([b, i]) . \end{array}$ This proves the “⇐” direction of (19) (we substitute G for X).

Now assume $G ([b, i])$ , that is: $\begin{matrix} (\forall s) (\exists t \forall y) b \cdot^{g} s ↓ \land (b \cdot^{g} t = 0 \lor i = 1) \land (b \cdot^{g} y \neq 0 \lor i = 0) . \end{matrix}$ Suppose we have X such that $\begin{matrix} (\forall p, j) : Φ ([p, j], X) ⟹ X ([p, j]) . \end{matrix}$ We need to prove that $X ([b, i])$ . We do this by showing that $\begin{matrix} (23) & (\forall p, j) : G ([p, j]) ⟹ X ([p, j]) . \end{matrix}$ This is done by induction on stages (see Remark 3.2). Recall that g is constructed as $g = ⋃_{α} g_{α}$ . Denote the corresponding graphs by $G_{α}$ . Then for $α = 0$ , $\begin{matrix} (\forall p, j) : G ([p, j]) ⟹ X ([p, j]) \end{matrix}$ clearly holds, since $g_{0} = \emptyset$ . If it holds up to α, then: $\begin{array}{l} (24) & G_{α + 1} [p, j] & ⟹ (\forall s) (\exists t \forall y) p \cdot^{g_{α}} s ↓ \land (p \cdot^{g_{α}} t = 0 \lor j = 1) \land (p \cdot^{g_{α}} y \neq 0 \lor j = 0) \\ (25) & ⟹ (\forall s) (\exists t \forall y) e p \cdot^{X} s ↓ \land (e p \cdot^{X} t = 0 \lor j = 1) \land (e p \cdot^{X} y \neq 0 \lor j = 0) \\ (26) & ⟹ Φ ([p, j], X) \\ (27) & ⟹ X ([p, j]) . \end{array}$ For limit ordinals λ, $G_{λ} [p, j] \Leftrightarrow G_{α} [p, j]$ for some $α < λ$ so that follows trivially.

Hence we have shown (23), from which $X [b, i]$ follows by assumption. □

Since the right-hand side of (19) is $Π_{1}^{1}$ , we have shown that the graph of g is $Π_{1}^{1}$ . Then for the application, we find: $\begin{array}{l} (28) & a \cdot^{g} b = c ⟺ & (\exists k \exists u = [u_{0}, \dots, u_{k}] \exists v = [v_{0}, \dots, v_{k}]) : \\ (29) & \underset{i}{⋀} G ([u_{i}, v_{i}]) \land a ([b, u_{0}, \dots, u_{i - 1}]) = p F u_{i} \land a ([b] * u) = p T c \end{array}$ which is clearly $Π_{1}^{1}$ , since any $Π_{1}^{1}$ -formula is closed under quantification.

To see that the application is $Π_{1}^{1}$ complete, see [4], Section VI.1. There one can find a proof in which a well-known $Π_{1}^{1}$ -complete set is reduced to a semi-recursive set computable from E in Hinman’s sense (i.e. a domain of a partial recursive function). This proof is easily adapted to a proof of $Π_{1}^{1}$ -completeness for our case. □

5. Strict pcas

In this short section we wish to prove a result that was announced in the Introduction: the fact that any pca as we have defined above is isomorphic to a strict pca. This result by itself seems to have little to do with the rest of the content of this paper. However, in Proposition 6.3 we use the above results to give an example of a pca that seems far from being strict. This forms a pleasing contrast with the theorem below. Moreover, it is Kleene’s (S1)–(S9) that inspired the proof of the theorem. Indeed, it is an easy observation that the application function defined in Definition 4.1 makes sense for any pca (except for primitive recursion), because we have pairing combinators and Curry numerals. We can therefore use clauses similar to Kleene’s (S1)–(S9) to define a new application function from an old one, which is exactly what is done below to “strictify” any partial combinatory algebra.

Remark 5.1.
Whenever we talk about “isomorphism” of partial combinatory algebras, we mean isomorphic as objects of the category of pcas with morphisms the applicative morphisms. However, it is not hard to see that in this case “isomorphic” coincides with “isomorphic” as algebras, i.e. the two inverse applicative morphisms have to be functions.

First, recall the definition of a strict pca:
Definition 5.1.
Let A be a partial applicative structure. Then A is called a strict pca when there are $k, s \in A$ such that for all $a, b, c \in A$ :
$s a b ↓$ ,

$k a b = a$ ,

$s a b c ≃ a c (b c)$ .
We also call the applicative structure on A strictly combinatory complete.

This definition might be preferable in some cases, for example when one would like that the set of domains of partial computable functions in a pca A form a dominance in $RT (A)$ (see [9]). However, as mentioned before, these domains are not part of the structure of a pca in the category PCA.

The following theorem supports this: in the context of applicative morphisms, the notions of a pca and a strict pca are essentially the same. Theorem 5.1.
Every pca is isomorphic to a strict pca.
Proof.
Let A be a pca. If A is trivial, then the statement is obvious, so we assume A non-trivial.

The idea is to define an explicit pca structure $A^{'}$ on the set A, such $a \mapsto {a}$ is an applicative morphism $A^{'} \to A$ . In this explicit structure, we also make sure that we can compute the application in A.

To define the new applicative structure on A, we use tuples and Curry numerals from A to ensure that what we define is actually computable in A. We denote the new application by $\cdot : A \times A \to A$ , and the resulting partial applicative structure by $A^{'}$ . The definition is by induction on the following clauses:
Constant function: for all $a, b, \in A$ : $\begin{array}{l} (30) & [\overline{1}] \cdot a = [\overline{1}, a], \\ (31) & [\overline{1}, a] \cdot b = a . \end{array}$

S-combinator: For $a, b, c \in A$ : $\begin{matrix} [\overline{2}] \cdot [a, b, c] ≃ a \cdot c \cdot (b \cdot c) . \end{matrix}$

Currying of parameters: for all $e, a, b, c \in A$ : $\begin{array}{l} (32) & [\overline{3}, e] \cdot a = [\overline{3}, e, a], \\ (33) & [\overline{3}, e, a] \cdot b = [\overline{3}, e, a, b], \\ (34) & [\overline{3}, e, a, b] \cdot c ≃ e \cdot [a, b, c] . \end{array}$

Application in A: $\begin{array}{l} (35) & [\overline{4}] \cdot a = [\overline{4}, a], \\ (36) & [\overline{4}, a] \cdot b ≃ a b . \end{array}$

Since A is non-trivial, the above is well defined. Strict combinatory completeness of A is satisfied by taking $k^{'} = [\overline{1}]$ , $s^{'} = [\overline{3}, [\overline{2}]]$ . Now $a \mapsto {a}$ is realized by $[\overline{4}]$ as an applicative morphism $A \to A^{'}$ . In the other direction, we have to simulate the above defined application in A. Using the fact that we can distinguish Curry numerals, determine length of tuples, and the recursion theorem, we can obtain an index $r \in A$ that performs the above case distinction, and in case the input is well formed (i.e. one of the tuples $[\overline{1}, \dots], \dots, [\overline{4}, \dots]$ and an element in A), yields the same value as the application function in $A^{'}$ . □
Remark 5.2.
Note that the proof above is entirely constructive; to define the application it only uses natural induction and explicit constructions with the combinators $k$ and $s$ .

Another observation is that if we would define $A^{'}$ using only the clauses (1)–(3), we obtain a strict pca $A^{'}$ , together with an applicative morphism $A^{'} \to A$ given by $a \mapsto {a}$ , that has “forgotten” a lot of the structure of A. We can then adjoin certain partial functions in A to $A^{'}$ to get some of them back (such as the application, so that we obtain A again). In the case of a decidable pca, for instance, we would lose decidability in this way. So, not only can we adjoin functions to a pca as an oracle, we are also able to forget some functions in a pca.

6. Local operators

In [15], a notion of realizability is studied that uses a specific local operator J on the Effective Topos. We will show here that some of the results in that paper can be derived easily using the functional E from Example 3.1 (for $A = K_{1}$ ) and Theorem 3.1.

We first give a definition of local operators in realizability toposes on a pca A, which we assume fixed from now on. The topos-theoretic origin is omitted here, for more about that we refer to [14] or [12]. We introduce the following notation: For $P, Q \subseteq A$ subsets, let $\begin{matrix} P \to Q = {a \in A ∣ (\forall b \in P) a b ↓ and a b \in Q} . \end{matrix}$

Definition 6.1.
A local operator is a function $J : P (A) \to P (A)$ such that there are $e_{1}, e_{2}, e_{3} \in N$ that satisfy:
$e_{1} \in ⋂_{P \subseteq A} P \to J P$ ;

$e_{2} \in ⋂_{P \subseteq A} J J P \to J P$ ;

$e_{3} \in ⋂_{P, Q \subseteq A} (P \to Q) \to (J P \to J Q)$ .

We define a pre-order on local operators as follows: we say $J ⩽ J^{'}$ whenever there is $e \in A$ such that: $\begin{matrix} e \in ⋂_{P \subseteq A} J P \to J^{'} P . \end{matrix}$ We write $J ≅ J^{'}$ if $J ⩽ J^{'}$ and $J^{'} ⩽ J$ . There is a least local operator $J_{⊥}$ , given by the identity: $J_{⊥} (P) = P$ . There is also a biggest local operator given by $J_{⊤} (P) = A$ .

The lattice of local operators (up to isomorphism) corresponds to the lattice of subtoposes of the realizability topos on A, denoted $RT (A)$ . Some of these subtoposes are realizability toposes $RT (B)$ themselves, in that case we have found a geometric inclusion $RT (B) \to RT (A)$ .
Definition 6.2 ([5]).

An applicative morphism $γ : A \to B$ is called computationally dense if there exists $m \in B$ such that: $\begin{array}{l} for every b \in B, there exists a \in A such that whenever b γ (a^{'}) ↓ for some a^{'}, \\ (37) & m γ (a a^{'}) \subseteq b γ (a^{'}) . \end{array}$

This should be read as follows: relative to γ, any application of an element b in B to an element in A (i.e. in $γ (a^{'})$ ) can be computed in A (by an element a), up to a last application in B that is uniform in b (the element m). Think of m as “translating” the result of the computation from A to B.

There is a one-to-one correspondence between geometric morphisms $RT (B) \to RT (A)$ and computationally dense morphisms $A \to B$ (the above intuition might give a feel for why the arrows get reversed!).

We can also characterize geometric inclusions $RT (B) \to RT (A)$ : they correspond precisely to computationally dense applicative morphisms $γ : A \to B$ that satisfy the additional condition $\begin{matrix} (in) there exists e \in B such that (\forall b) (\exists a) (e b \in γ (a) and m γ (a) = {b}), \end{matrix}$ where m is as in Definition 6.2 (this is a consequence of results in [5,7]). In that case the corresponding local operator in $RT (A)$ is given by $\begin{matrix} J (P) = {a \in A | m γ (a) \subseteq ⋃_{a^{'} \in P} γ (a^{'})} . \end{matrix}$ The following corresponds to Proposition 2.2 in [13].

Proposition 6.1.
For $f : A \to A$ a partial function, the identity relation on A is a computationally dense applicative morphism $ι_{f} : A \to A [f]$ that satisfies the condition (in). Therefore, there is a canonical geometric inclusion $RT (A [f]) \to RT (A)$ .

By our construction, we obtain for every (partial) functional $F : A^{A} \to A$ a subtopos $RT (A [F]) \to RT (A)$ corresponding to the local operator $\begin{matrix} J_{F} (P) = {a \in A ∣ m \cdot^{F} a \in P} . \end{matrix}$ One can check that this indeed defines a local operator according to Definition 6.1.
6.1. J-assemblies

In [6], Martin Hyland showed that for every function $f : N \to N$ , there is a least local operator that forces f to be computable in the Effective Topos. This yields an embedding of the Turing degrees into the lattice of local operators. In [11], Wesley Phoa showed that the corresponding subtopos is equivalent to $RT (K_{1}^{f})$ , the realizability topos on the pca of recursive application with oracle f. This result can be generalized to arbitrary pcas and partial functions: for (partial) functions $f : A \to A$ , the least subtopos of $RT (A)$ in which f is realizable is equivalent to $RT (A [f])$ . For a proof, see [1].

We will now carry out a similar statement for effective operations. To make things easier, we will work on a category of assemblies. The consequences for realizability toposes are immediate for anyone familiar with them. In the following we assume that we have fixed some pca A.

Definition 6.3.
Let J be a local operator for A. A J-assembly is a pair $(X, E)$ where $E : X \to A$ is a total relation.

For $(X, E)$ , $(Y, F)$ J-assemblies, a morphism of J-assemblies is a function $f : X \to Y$ together with a $t \in A$ such that $\begin{matrix} t \in ⋂_{x \in X} E (x) \to J F (f (x)) . \end{matrix}$ We say that t tracks f relative to J.

One can check that the composition $g \circ f$ of morphisms of J-assemblies $f : (X, E) \to (Y, F)$ , $g : (Y, F) \to (Z, G)$ is again a morphism of J-assemblies, so that J-assemblies form a category $Ass {(A)}_{J}$ . The category $Ass {(A)}_{J}$ has a lot of structure: it is regular, Cartesian closed and has finite colimits (in fact, it is a quasi-topos). For $(X, E)$ , $(Y, F)$ J-assemblies, the exponential $(Z, G) : = {(Y, F)}^{X, E}$ is given by: $\begin{array}{l} (38) & Z = {f : X \to Y ∣ f is a morphism (X, E) \to (Y, F)}, \\ (39) & G (f) = {t \in A ∣ t tracks f} . \end{array}$

The assembly $A = (A, {id}_{A})$ can be seen as a representation of the pca A in the category of J-assemblies. The object $A^{A}$ consists of the morphisms $A \to A$ in $Ass {(A)}_{J}$ . For $J = J_{⊥}$ , these are precisely the computable functions in A. Also, one can check that the arrows $\begin{matrix} A^{A} \to A \end{matrix}$ in $Ass {(A)}_{J_{⊥}}$ are precisely the effective operations in A. We have the following theorem: Theorem 6.1.
Let $F : A^{A} \to A$ be a total functional, and assume that F defines a morphism $\begin{matrix} A^{A} \to A \end{matrix}$ in $Ass {(A)}_{J}$ . Then $J_{F} ⩽ J$ .
Proof.
We can assume that J preserves inclusions, otherwise we let $\begin{matrix} J^{'} P = ⋃_{Q \subseteq P} J P \end{matrix}$ and show that $J^{'} ≅ J$ , which is an easy exercise using Definition 6.1.

By computational density, there exists $t \in A$ such that for all $v, x \in A$ : $\begin{matrix} m \cdot^{F} (t v x) ≲ v \cdot^{F} x . \end{matrix}$ Since m is independent of F, we also know that if the right-hand side halts at some stage, the left-hand side also halts at that stage.

We pick $e_{1}$ , $e_{2}$ , $e_{3}$ as in Definition 6.1.

Suppose that $F : A^{A} \to A$ is tracked by r as morphism of J-assemblies.

Choose $m \in A$ (using the recursion theorem) so that: $\begin{array}{l} (40) & m x y ≲ & if p_{0} (m ([x] * y)) \\ (41) & then e_{1} (p_{1} (m ([x] * y))) \\ (42) & else e_{2} (e_{3} (⟨ z ⟩ m x (y * [z])) r (⟨ w ⟩ (m (t v w) []))), \\ (43) & where v = p_{1} (m ([x] * y)) . \end{array}$

Here $[]$ is the empty sequence. We will prove by induction on the stage at which $m \cdot^{F} x ↓$ that for all x, $\begin{matrix} (44) & m x [] \in J {m \cdot^{F} x} . \end{matrix}$

Stage 0: in that case $m ([x]) = p T c$ for some c. Then $\begin{matrix} (45) & m x [] = e_{1} (p_{1} (m ([x] * []))) \in J {c} . \end{matrix}$

Stage $λ > 0$ : Let $u = [u_{0}, \dots, u_{n}]$ be the halting dialogue between m and x. It is easy to see that $\begin{matrix} m x [u_{0}, \dots, u_{n}] \in J {m \cdot^{F} x} . \end{matrix}$

Now suppose that $0 < i ⩽ n + 1$ is such that $\begin{matrix} (46) & m ([x] * u^{< i + 1}] \in J {m \cdot^{F} x} . \end{matrix}$ We know that: $\begin{matrix} m ([x] * u^{< i}) = p F v, \end{matrix}$ where v is such that at some stage $α < λ$ , for each w, $v \cdot^{F} w ↓$ . So for each w, also $m \cdot^{F} (t v w) ↓$ at stage α. Let f be the function $w \mapsto v \cdot^{F} w$ . By induction hypothesis, $\begin{matrix} m (t v w) [] \in J {v \cdot^{F} w} \end{matrix}$ for each w, so $⟨ w ⟩ m (t v w) []$ tracks f as morphism of J-assemblies. So $\begin{matrix} r (⟨ w ⟩ (m (t v w) l)) \in J {F (f)} \end{matrix}$ and $F (f) = u_{i}$ . By (46), we have: $\begin{matrix} ⟨ z ⟩ m ([x] * u^{< i} * [z]) \in {F (f)} \to J {m \cdot^{F} x} \end{matrix}$ and therefore $\begin{matrix} e_{2} (e_{3} (⟨ z ⟩ m x (u^{< i} * [z])) r (⟨ w ⟩ (m (t v w) []))) \in J {m \cdot^{F} x} \end{matrix}$ hence it follows that $\begin{matrix} (47) & m ([x] * u^{< i}) \in J {m \cdot^{F} x} . \end{matrix}$

By reverse induction, it follows that $\begin{matrix} m x [] \in J {m \cdot^{F} x}, \end{matrix}$ so this finishes the induction step, so we have (44).

Therefore $\begin{matrix} ⟨ x ⟩ m x [] \in ⋂_{P \subseteq A} J_{F} P \to J P \end{matrix}$ and we are done. □

6.2. Pitts’ local operator

In this section we will take a look at a specific local operator that is studied in [15], which we will denote by $J_{P}$ . It turns out that we can use the results of the previous section to say something about its complexity. This operator was introduced by Andrew Pitts in his thesis (Example 5.8, [12]). Denote by $\nabla (N)$ the assembly $\begin{matrix} (N, T), where T (n) = N for all n . \end{matrix}$ We can define the following subobject of $\nabla (N)$ : $\begin{matrix} (N, R) ↣ \nabla (N), where R (n) = {m \in N ∣ m ⩾ n} . \end{matrix}$ Pitts’ local operator $J_{P}$ is defined as the least local operator in $RT (K_{1})$ that forces the above arrow to be an isomorphism of $J_{P}$ -assemblies. Explicitly, it is given by: $\begin{matrix} J_{P} (S) = ⋂ {Q \subseteq N | {0} \land S \subseteq Q and {1} \land (⋃_{n \in N} (R (n) \to Q)) \subseteq Q}, \end{matrix}$ where for $R, S \subseteq N$ : $\begin{matrix} R \land S = {p r s ∣ r \in R, s \in S} . \end{matrix}$ Write N for the assembly A for $A = K_{1}$ , so $\begin{matrix} (N, N), where N (n) = {n} . \end{matrix}$ Recall the functional E from Example 3.1. For $A = K_{1}$ , we rather define it as $\begin{matrix} E (f) = \{\begin{matrix} 0 & if (\exists n) f (n), \\ 1 & otherwise . \end{matrix} \end{matrix}$

We have the following proposition:

Proposition 6.2.
There is an index $r_{E} \in N$ that tracks E as morphism of $J_{P}$ -assemblies $N^{N} \to N$ .
Proof.
Pick $e_{3}$ as in Definition 6.1.

By Corollary 1.6 of [15], there is a partial recursive function G such that for all $\begin{matrix} x_{0} \in J_{P} {a_{0}}, \dots, x_{n - 1} \in J_{P} {a_{n - 1}}, \end{matrix}$ we have $\begin{array}{l} (48) & G (⟨ x_{0}, \dots, x_{n - 1} ⟩) \in J_{P} {0} if for some i < n, a_{i} = 0, \\ (49) & G (⟨ x_{0}, \dots, x_{n - 1} ⟩) \in J_{P} {1} otherwise . \end{array}$ Now let $t_{E}$ be an index in $K_{1}$ defined by: $\begin{matrix} t_{E} e n ≃ G (⟨ e (0), \dots, e (n) ⟩) . \end{matrix}$ Then whenever e realizes a total function $f : N \to N$ , we have $(\exists n) f (n) = 0$ if and only if $(\exists n) e n \in J_{P} {0}$ , which holds if and only if there is n such that $\begin{matrix} t_{E} e \in {m ∣ m ⩾ n} \to J_{P} {0} \end{matrix}$ since otherwise $\begin{matrix} t_{E} e \in {m ∣ m ⩾ 0} \to J_{P} {1} . \end{matrix}$

By definition of $J_{P}$ , we have in the first case that $t_{E} e \in J_{P} {0}$ , and in the latter case $t_{E} e \in J_{P} {1}$ . Now $t_{E}$ tracks E as morphism of $J_{P}$ -assemblies $N^{N} \to N$ . □

The following corollary corresponds to Theorem 2.2 in [15]. Corollary 6.1.
The morphisms of $J_{P}$ -assemblies $N \to N$ are precisely the hyperarithmetical functions.
Proof.
By Theorem 6.1, $J_{E} ⩽ J_{P}$ . Therefore it is easily seen that every morphism of $J_{E}$ assemblies $N \to N$ is a morphism of $J_{P}$ -assemblies. Now it follows that every hyperarithmetical function is a morphism of $J_{P}$ -assemblies by Corollary 4.1.

For the converse, observe that every morphism $f : N \to N$ is $Π_{1}^{1}$ since: $\begin{matrix} f (n) = m ⟺ (\forall B) {p 0 m} \subseteq B \land {1} \land ({e ∣ (\exists n) (\forall m ⩾ n) e m \in B}) \subseteq B \to e (a n) \in B, \end{matrix}$ where e is a realizer for f as a morphism $N \to N$ . Notice that the above expression is $Π_{1}^{1}$ . Since f is total, it is also $Σ_{1}^{1}$ .

Therefore the morphisms of $J_{P}$ -assemblies $N \to N$ are precisely the hyperarithmetical functions. □

6.3. $J_{P}$ -representable functions

In [15], the morphisms of $J_{P}$ -assemblies $N \to N$ are called $J_{P}$ -representable. Since for every $n, m \in N$ $\begin{matrix} (50) & n \neq m ⟺ J_{P} {n} \cap J_{P} {m} = \emptyset, \end{matrix}$ the following is well defined:

Definition 6.4.
A partial function $F : N \to N$ is $J_{P}$ -representable if there exists $e \in N$ such that for all $m \in N$ : $\begin{matrix} ϕ_{e} (n) \in J_{P} {m} ⟺ F (n) = m . \end{matrix}$ Here $ϕ_{e}$ denotes the eth partial computable function from ordinary recursion theory (or the application in $K_{1}$ ).

By defining $ψ_{e} = F$ for such e, we obtain an indexed set of partial functions and a new application $\begin{matrix} e \cdot n \mapsto ψ_{e} (n) \end{matrix}$ on $N$ .

A natural question is whether the application $e \cdot n ≃ ψ_{e} (n)$ is combinatory complete in the sense of Definition 2.3. This turns out to be the case:
Proposition 6.3.
The application $e \cdot n ≃ ψ_{e} (n)$ defines a pca $P_{1}$ on $N$ .
Proof.
This is an easy exercise on pcas and Definition 6.1. □

The pca $P_{1}$ defined above is an example of a pca that is not strict (although this might be difficult to show) and it seems very hard to define it in a similar way from $J_{P}$ that would make it strict. For this specific example, Theorem 5.1 is therefore a reassuring result (although in this case, it could also have been proven, with some care, using the theorem below).

Finally, we have the following theorem: Theorem 6.2.
The pca $P_{1}$ is isomorphic to $K_{1} [E]$ .
Proof.
Let $γ : K_{1} \to P_{1}$ be the applicative morphism $n \mapsto {n}$ (it is easily verified that this is a decidable applicative morphism).

Now $E \in E_{γ}$ by Proposition 6.2. Therefore, by Theorem 3.1, γ factors through $K_{1} [E]$ , hence we have a decidable applicative morphism $γ_{E} : K_{1} [E] \to P_{1}$ , given by the identity on $N$ .

This morphism also goes the other way: this follows from the fact that the application in $K_{1} [E]$ is $Π_{1}^{1}$ -complete (Proposition 4.1), and the fact that the application in $P_{1}$ is $Π_{1}^{1}$ . □

7. Higher types

One may wonder whether Theorem 4.2 also holds for computability in higher type functionals (so, type 3 and higher). The answer to that question is positive: for functionals $x_{1}, \dots, x_{n}$ of certain types, one can define in a similar fashion a pca $\begin{matrix} K_{1} [x_{1}, \dots, x_{n}] \end{matrix}$ that is again isomorphic to the pca of recursive application relative to $x_{1}, \dots, x_{n}$ in Kleene’s sense. The idea is to define $K_{1} [x_{1}, \dots, x_{n}] = K_{1} [f]$ , where f is defined in stages, simultaneously for $x_{1}, \dots, x_{n}$ , so that the resulting applicative structure is closed under application of any of the functionals. However, we do not get much more than that. In the above, we have shown that constructing the pca of recursive application relative to a type 2 functional F is the same thing as “forcing F to be a realizable as effective operation” (taking note of Remark 3.1), or forcing F to be realizable in the corresponding category of assemblies or realizability topos. To see what goes wrong, we will sketch the case for a single type 3 functional $Φ : A^{A^{A}} \to A$ .

For such Φ, we can define a pca $A [Φ]$ as $A [f]$ , where f satisfies: $\begin{matrix} for e \in A, F : A^{A} \to A such that (\forall g : A \to A) e \cdot^{g, f} T = F (g), f (e) = Φ (F) . \end{matrix}$ Here $\cdot^{g, f}$ is defined as $\cdot^{h}$ for $h (a) = p g (a) f (a)$ . An f satisfying the above equation can again be defined in (transfinitely many) stages. The resulting pca $A [Φ]$ will satisfy the property that whenever e is an index such that $\begin{matrix} e \cdot^{g, Φ} T = F (g) (w.r.t. the application in A [Φ]) \end{matrix}$ for some functional $F : A^{A} \to A$ , then we can compute $Φ (F)$ in $A [Φ]$ , i.e. there is an index r such that $r \cdot^{Φ} e = Φ (F)$ , uniformly in such e. The reason we have to define $A [Φ]$ in this way is that Φ is defined on total functionals $A^{A} \to A$ , and we want Φ to be defined on all total functionals that are “computable” in $A [Φ]$ . By a computable functional we mean here a total functional F that has in index in A which, when given an oracle g, computes $F (g)$ .

Kleene uses a similar definition of “recursive application relative to Φ” in [8], as does Hinman in [4]. One can again show that for $A = K_{1}$ , the resulting applicative structures are the same in the sense of Theorem 4.2. The same holds for general n-tuples of higher types $x_{1}, \dots, x_{n}$ .

However, Φ is not an effective operation relative to $A [Φ]$ . For a pca A, an effective operation of type 3 should be the same thing as a morphism of assemblies $\begin{matrix} (51) & A^{A^{A}} \to A . \end{matrix}$ So it is a map that sends every effective operation of type 2 to A. It is not clear that Φ is an effective operation in this sense for $A [Φ]$ as defined above, in fact this seems completely unrelated. For instance, there could be effective operations that are not computable functionals in the above sense (an example of this kind can be found in [3]) so there is no guarantee that Φ can be evaluated on those. Conversely, the methods we have developed above do not seem to give a way to “force Φ to be realizable” as a morphism of type (51). At the very least, it seems to require a more involved method of forcing than just a transfinite induction. Denote for instance by $A {[Φ]}^{'}$ the hypothetical pca in which Φ is realizable as an effective operation of type 3. When Φ has different values on F and G, but $F ↾ {Tot}_{A} = G ↾ {Tot}_{A}$ , we will first have to make sure that either $F ↾ {Tot}_{A {[Φ]}^{'}} \neq G ↾ {Tot}_{A {[Φ]}^{'}}$ , or that F or G (or both) are no longer realizable as effective operations relative to $A {[Φ]}^{'}$ , and make sure that this property is preserved in the construction of $A {[Φ]}^{'}$ .

Another direction could be to study other notions of computable functionals, and to see to what extent these generalize to pcas and especially the theory of categories of assemblies and realizability toposes. The overview [10] is a good starting point here.

References

Faber and

van Oosten, More on geometric morphisms between realizability toposes, Theory Appl. Categ. 29 (2014), 874–895.

Frey, A characterization of realizability toposes, 2014, available at: arXiv:1404.6997.

R.O.

Gandy and

J.M.E.

Hyland, Computable and recursively countable functions of higher type, in: Logic Colloquium 76, Oxford, 1976, Studies in Logic and the Foundations of Mathematics, Vol. 87, North-Holland, Amsterdam, 1977, pp. 407–438.

P.G.

Hinman, Recursion-Theoretic Hierarchies, Perspectives in Mathematical Logic, Springer, Berlin, 1978.

Hofstra and

van Oosten, Ordered partial combinatory algebras, Math. Proc. Cambridge Philos. Soc. 134(3) (2003), 445–463.

J.M.E.

Hyland, The effective topos, in: The L.E.J. Brouwer Centenary Symposium, Noordwijkerhout, 1981, Studies in Logic and the Foundations of Mathematics, Vol. 110, North-Holland, Amsterdam, 1982, pp. 165–216.

Johnstone, Geometric morphisms of realizability toposes, Theory Appl. Categ. 28(9) (2013), 241–249.

S.C.

Kleene, Recursive functionals and quantifiers of finite types. I, Trans. Amer. Math. Soc. 91 (1959), 1–52.

J.R.

Longley, Realizability toposes and language semantics, PhD thesis, University of Edinburgh, 1995.

10.

J.R.

Longley, Notions of computability at higher types. I, in: Logic Colloquium 2000, Lecture Notes in Logic, Vol. 19, Association for Symbolic Logic, Urbana, IL, 2005, pp. 32–142.

11.

Phoa, Relative computability in the effective topos, Math. Proc. Cambridge Philos. Soc. 106(3) (1989), 419–422.

12.

A.M.

Pitts, The theory of triposes, PhD thesis, Cambridge University, 1981.

13.

van Oosten, A general form of relative recursion, Notre Dame J. Formal Logic 47(3) (2006), 311–318 (electronic).

14.

van Oosten, Realizability: An Introduction to Its Categorical Side, Studies in Logic and the Foundations of Mathematics, Vol. 152, Elsevier B.V., Amsterdam, 2008.

15.

van Oosten, Realizability with a local operator of A.M. Pitts, Theoret. Comput. Sci. 546 (2014), 237–243.