What Would the World Look Like if Everything was Computable?: An Introduction to Hyland’s Effective Topos

Suppose that we wanted to construct a mathematical universe where all objects were computable in some sense. How would we do it?

Well, we could certainly allow the set \mathbb{N} into our universe: natural numbers are the most basic computational objects there are. (Notation: I’ll use N to refer to \mathbb{N} when we’re considering it as part of the universe we’ll building, and just \mathbb{N} when we’re talking about the set of natural numbers in the “real” world.) What should we take as our set of functions N^N from N to N? Since we want to admit only computable things, we should let N^N be the set of computable functions from \mathbb{N} to \mathbb{N}, which we can represent non-uniquely by their indices (i.e., by the programs which compute them).

(For clarity, I’ll use the following notation for computable functions: \phi_e denotes the partial function from \mathbb{N} to \mathbb{N} computed by the eth Turing machine. Given n\in\mathbb{N}, it is possible that the computation \phi_e(n) never halts; in that case, I’ll write \phi_e(n){\uparrow} and say that \phi_e(n) is undefined. If it does halt, I’ll write \phi_e(n){\downarrow} and say that \phi_e(n) is defined. If it halts, then it yields an output m. To indicate what it is, I’ll write \phi_e(n) = m or \phi_e(n){\downarrow} = m.)

So, we’ve decided that N^N should equal \{e \mid \forall n\in\mathbb{N}\, \phi_e(n){\downarrow}\}. What should N^{\left(N^N\right)} equal? At this point, there is a slight subtlety: It’s not simply the set of computable functions from N^N (considered as a subset of \mathbb{N}) to N (considered as N), because we would like to only admit those functions from N^N to N that return the same number when given inputs which represent the same element of \mathbb{N}^\mathbb{N}.

Therefore, we’ll let N^{(N^N)} be the set of e\in\mathbb{N} such that, for all n\in N^N, \phi_e(n){\downarrow}, and whenever n,m\in N^N are such that for all x\in\mathbb{N}, \phi_n(x) = \phi_m(x), then \phi_e(n) = \phi_e(m).

We can similarly define (N^N)^{(N^N)}, except that there are now two places where we should take into account that we consider n,m\in N^N equivalent if for all x\in\mathbb{N}, \phi_n(x) = \phi_m(x): We’ll let (N^N)^{(N^N)} be the set of e such that, whenever n, m \in N^N are equivalent in the aforementioned sense, \phi_e(n) and \phi_e(m) are defined and equivalent in the aforementioned sense.

In a similar fashion, we can define (N^{(N^N)})^{(N^N)} and so on; these sets are called the sets of hereditarily computable functions.

Can we generalize this construction to a category that incorporates all possible computable representations of real objects? More ambitiously, can we generalize to a category that is a genuine mathematical universe in the sense that questions like “Does the Riemann Hypothesis hold in this category?” are meaningful? The answer, due to Martin Hyland, is yes.

This material is from Jaap van Oosten‘s book “Realizability: A Categorical Perspective” (link to Preface, Introduction and Table of Contents). Unfortunately, I don’t know of a freely available explanation of the effective topos on the web, which is part of the reason why I’m writing this blog entry. (If you know of one, please leave a comment. Edit: Found one.) However, the Stanford Encyclopedia of Philosophy has a pretty good section on the realizability interpretation of intuitionistic logic, on which Hyland’s effective topos is based.

Back to the math. Notice that what we did in the N^N case was the following: Although we represented the computable functions as a subset of \mathbb{N}, we still kept the “real” set \mathbb{N}^\mathbb{N} hiding around in the background: we used it to determine what the appropriate elements of N^{(N^N)} should be: If two elements of N^N represented the same element of the “real set” \mathbb{N}^\mathbb{N}, then an element of N^{(N^N)} should assign the same number to both of them.

That suggests a generalization. Let an assembly be a pair (X,E), where X is a set, and E is a function from X to \mathcal{P}(\mathbb{N}), the power set of \mathbb{N}. We think of E as assigning to each element of X its computable representations. We let a morphism between two assemblies (X,E) and (Y,E') be a function from X to Y such that there is an e\in \mathbb{N} such that, whenever x\in X, and n\in E(x), \phi_e(n){\downarrow} \in E'(f(x)).

With these morphisms, the class of assemblies forms a category. Let A=(X,E_0) and B=(Y,E_1) be two assemblies. Then they have a direct product A\times B given by (X\times Y, E_2), where E_2(x,y) = \{ \langle n,m\rangle \mid n\in E_0(x)\text{ and } m\in E_1(y)\} and \langle {\cdot}, {\cdot}\rangle \colon \mathbb{N}^2 \to \mathbb{N} is a pairing function. They have an exponential A^B given by (X^Y, E_2), where E_2(f) = \{e\mid \forall y\in Y\,\forall m\in E_1(y)\, \phi_e(m){\downarrow}\in E_0(f(y))\}.

If we let N be the assembly (\mathbb{N}, E), where E(n) = \{n\}, then the iterated exponential objects of N correspond precisely to our initial definition of the sets of hereditarily computable objects above.

This is all great, but we still can’t call the category of assemblies a mathematical universe. Why not? Well, in the real world, we ask questions like “Is the Riemann Hypothesis true?”, “Is Goldbach’s conjecture true”, etc., but we don’t yet know how to ask questions like “Is the Riemann Hypothesis true in the category of assemblies?” any more than it makes sense to ask whether or not the Riemann Hypothesis is true in the group \mathbb{Z} or in the number 17. What we need is a way to interpret statements being true or not in this category.

In turning the category of assemblies into one in which we can interpret logical statements, there are three considerations, each of which builds on the previous ones.

  1. The object of truth values should have more than two elements. Let’s step back to the ordinary category of sets for a moment. Say we have two sets S and T and an injection i from S to T. Given x\in T, what is the truth value of the proposition that x is in the image of i? Well, I don’t know, but it’s clearly either \text{true} or \text{false}. But in the category of assemblies it’s more complicated due to the computational information we have lying around. Say that we have an injective morphism from an assembly (S,E) to an assembly (T,E'). Given x\in T, now what is the truth value of the proposition that x is in the image of i? What if there is a y\in S such that i(y) = x but E(y)\ne E'(x)? Without resolving the issue now, one plausible answer is that the truth value should be the set of indices of all computable functions taking E(y) to E'(x), so that the more “alike” E(y) and E(x), the more “true” the proposition is, and furthermore this “alikeness” is represented in a computational way. So, a working hypothesis is that the set of truth values should be something like \mathcal{P}(\mathbb{N}).
  2. Objects should come equipped with an equivalence relation. In the category of assemblies, there is no question about whether or not two elements of a given object are equal. If we are making a category where the object of truth values is something like \mathcal{P}(\mathbb{N}), however, we should allow that the proposition that different elements are equal has a truth value in that object, rather than in the classical set \{\text{true}, \text{false}\} of truth values. Therefore, objects should be something like (X,\sim), where X is a set and \sim is a map from X\times X to \mathcal{P}(\mathbb{N}). (We can represent an assembly (X,E) as the object (X,\sim) in our new category where x\sim x = E(x) and x\sim y= \emptyset if x\ne y).
  3. Morphisms should be more general than functions. If we’re allowing objects to come equipped with some sort of equivalence relation, we will have to let morphisms be more general than functions: If f is a morphism from (X,\sim) and (Y,\sim), f(x) = y and y\sim y'\ne \emptyset, then f(x) = y' is also true to some degree. So morphisms should probably be some sort of relation on X\times Y that resembles a function in some way.

Now, after listing all those (somewhat vague) considerations, I’ll describe the category that takes them into account. It’s called the Effective Topos and it was discovered/invented by Martin Hyland.

Description of the category

The objects of the effective topos are pairs (X,\sim) where X is a set and \sim is a map from X\times X to \mathcal{P}(\mathbb{N}). This map is required to satisfy the following properties:

  • There must be a number s\in\mathbb{N} such that for all x,y\in X if n\in (x\sim y) then \phi_s(n){\downarrow} \in (y\sim x).
  • There must be a number t\in \mathbb{N} such that for all x,y,z\in X if n\in (x\sim y) and m\in (y\sim z) then \phi_t(\langle n,m\rangle)\in (x\sim z).

(In the above, s stands for “symmetric” and t stands for “transitive.”)

A morphism from (X,\sim) to (Y,\sim) is represented by a function F\colon X\times Y\to \mathcal{P}(\mathbb{N}) satisfying the following:

  • There must be a number st\in \mathbb{N} such that for all x\in X, y\in Y if n\in F(x,y) then \phi_{st}(n) = \langle m,p\rangle where m\in (x\sim x) and p\in (y\sim y).
  • There must be a number rl\in\mathbb{N} such that for all x,x'\in X, y,y'\in Y, if n\in (x\sim x'), m\in F(x,y), and p\in (y\sim y'), then \phi_{rl}(\langle n,m,p\rangle) \in F(x',y').
  • There must be a number sv\in\mathbb{N} such that for all x\in X, y,y'\in Y, if n\in F(x,y) and m\in F(x,y') then \phi_{sv}(\langle n,m\rangle)\in (y\sim y').
  • There must be a number tl\in \mathbb{N} such that for all x\in X, if n\in (x\sim x) then \phi_{tl}(x){\downarrow}\in \bigcup_{y\in Y}F(x,y).

(In the above, st stands for “strict,” rl stands for “relational,” sv stands for “single-valued” and tl stands for “total.”)

We say that two such representations F and F' are equivalent if there exist e_0,e_1\in \mathbb{N} such that for all x\in X, y\in Y, if n\in F(x,y) then \phi_{e_0}(n){\downarrow}\in F'(x,y) and conversely if n\in F'(x,y) then \phi_{e_1}(n){\downarrow}\in F(x,y). (Thus, a morphism in the Effective Topos is actually an equivalence class of representations as above.)

Figuring out how to compose such morphisms is an exercise left to the websurfer.

Let (X,\sim) and (Y,\sim) be two objects. Their direct product is given by (X\times Y, \sim) where (x,y)\sim (x',y') = (x\sim x')\times (y\sim y'). To form the exponential (Y,\sim)^{(X,\sim)}, take the object (\mathcal{P}(\mathbb{N})^{X\times Y},\sim), where in the definition of \sim, you emulate the definition of a morphism given above.

The object of truth values (often denoted \Omega in any topos) is (\mathcal{P}(\mathbb{N}),\sim), where S\sim T = \{\langle e_0,e_1\rangle \mid \forall n\in S\,\phi_{e_0}(n){\downarrow}\in T\text{ and }\forall m\in T\,\phi_{e_1}(m){\downarrow}\in S.

The object 1 playing the role of a singleton set is (\{0\},\sim) where 0\sim 0 = \{0\}.

The map from 1 to \Omega representing the truth value \text{true} is given by the equivalence class of the map F\colon \{0\}\times \mathcal{P}(\mathbb{N})\to\mathcal{P}(\mathbb{N}) defined by (0,S)\mapsto (S\equiv \mathbb{N}).

The natural numbers object of the effective topos is N = (\mathbb{N},\sim), where n\sim n = \{n\} and n\sim m = \emptyset where n\ne m.

Interpretation of logical formulas in the effective topos.

I’ll now describe how logical formulas can be interpreted in Hyland’s effective topos. If x_1,\ldots, x_n are variables intended to range over the objects X_1,\ldots, X_n respectively and \phi(x_1,\ldots, x_n) is a formula with free variables from \{x_1,\ldots,x_n\}, then I’ll show how to find a map \|\phi\| from X_1\times \cdots X_n to \Omega interpreting that formula. If n = 0, and thus the formula has no free variables and is a sentence, then the interpretation will give a map from 1 to \Omega. We say that a sentence holds in the effective topos if its interpretation is equal to the map \text{true} defined above.

The only atomic relation is equality, and the interpretation of atomic formulas is given by the \sim component of the objects of the effective topos.

For clarity, assume that \phi and \psi contain only one free variable, and that it ranges over the object X. If we know the interpretations of \phi and \psi already, then we have the following:

  • \|\phi\wedge\psi\| is represented by the map taking x\in X to \{\langle n,m\rangle \mid n\in \|phi\|(x),m\in\|\psi\|(x)\}.
  • \|\phi\vee\psi\| is represented by the map taking x\in X to \{\langle 0,n\mid n\in \|\phi\|(x)\}\cup \{\langle 1,m\mid m\in \|\psi\|(x)\}.
  • \|\phi\rightarrow \psi\| is represented by the map taking x to \{e\mid \forall n\in \|\phi\|(x)\, \phi_e(n){\downarrow}\in\|\psi\|(x)\}.

Now suppose that \phi has two free variables ranging over X and Y respectively, and I’ll show you how to interpret quantifiers.

  • \|\exists_{y\in Y}\phi\| is represented by the map taking x\in X to \bigcup_{y\in Y}\|\phi\|(x,y).
  • \|\forall_{y\in Y}\phi\| is represented by the map taking x\in X to \{e\in \mathbb{N}\mid \forall n\in \mathbb{N}\forall y\in Y\, \phi_e(n){\downarrow}\in \|\phi\|(x,y)\}.

Now, once we observe that we can interpret the power “set” of an object X in the effective topos as the exponential \Omega^X, we know how to interpret all first- and higher-order sentences as holding or not in the effective topos.

Here are some interesting sentences given by Van Oosten that highlight some differences between the effective topos and the ordinary category of sets.

  • Note that we may write the relation “\phi_e(n) = m” as a relation on N\times N\times N in our language. Then the sentence \forall f\in N^N\exists e\in N\, \phi_e = f is true in the effective topos.
  • For every formula \phi(S,x), where S is a variable ranging over \Omega^{N} and n is a variable ranging over N, the sentence \forall S\exists x\phi(S,x)\rightarrow \exists x\forall S\phi(S,x) holds in the effective topos.
  • We may construct the rationals Q and the reals R in the effective topos just as we do in the category of sets. However, they have different properties. For example, in the effective topos the statement “There exists a bounded monotonic sequence in R that does not converge to a limit.” holds, contradicting the Bolzano-Weierstrass theorem. Intuitively, this is because we can find a bounded, monotonic sequence converging to a real number whose binary expansion encodes the halting problem but such that every member of the sequence has a decidable binary expansion.
  • The sentence \neg \forall x\in R (x \leq 0 \vee x \geq 0) holds in the effective topos.
  • Similar to the above, we may can show that the intermediate value theorem fails in the effective topos.
  • In the effective topos, the statement “All functions from R to R are continuous” holds.

3 thoughts on “What Would the World Look Like if Everything was Computable?: An Introduction to Hyland’s Effective Topos

  1. Yes, it’s quite well written. Wesley Phoa is a fiendishly intelligent bloke who I believe works in a financial industry (around Sydney, Australia), but who is still connected in some way with promoting categorical logic.

  2. Thanks: this is a nice exposition. As you say, there seems to be relatively little about the effective topos available freely on the web. And since Martin Hyland was my supervisor (on a quite different subject), I’ve always wanted to know more about it.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s