(This post was originally published on Nov 30th 2017, and is 1 of 4 posts brought forwarded today as part of the AI Alignment Forum launch sequence on fixed points.)

1 Introduction

Before the work of Turing, one could justifiably be skeptical of the idea of a universal computable function. After all, there is no computable function such that for all computable there is some index such that for all . If there were, we could pick , and then a contradiction. Of course, universal Turing machines don't run into this obstacle; as Gödel put it, "By a kind of miracle it is not necessary to distinguish orders, and the diagonal procedure does not lead outside the defined notion." [1]

The miracle of Turing machines is that there is a partial computable function such that for all partial computable there is an index such that for all . Here, we look at a different "miracle", that of reflective oracles [2,3]. As we will see in Theorem 1, given a reflective oracle , there is a (stochastic) -computable function such that for any (stochastic) -computable function , there is some index such that and have the same distribution for all . This existence theorem seems to skirt even closer to the contradiction mentioned above.

We use this idea to answer "in spirit" the converse Lawvere problem posed in [4]. These methods also generalize to prove a similar analogue of the ubiquitous converse Lawvere problem from [5]. The original questions, stated in terms of topology, remain open, but I find that the model proposed here, using computability, is equally satisfying from the point of view of studying reflective agents. Those references can be consulted for more motivation on these problems from the perspective of reflective agency.

Section 3 proves the main lemma, and proves the converse Lawvere theorem for reflective oracles. In section 4, we use that to give a (circular) proof of Brouwer's fixed point theorem, as mentioned in [4]. In section 5, we prove the ubiquitous converse Lawvere theorem for reflective oracles.

2 Definitions

For any measurable space , the set of probability measures on is denoted .

A probabilistic oracle is a map . A probabilistic oracle machine is a probabilistic Turing machine that can query a probabilistic oracle . On a given query , it gets the answer with probability and the answer otherwise. Different queries are independent events, so this completely determines the behavior of such a machine.

We denote by the stochastic partial -computable function , where represents nonhalting, computed by the probabilistic Turing machine with index . The notation indicates the event that halts on input , and is the event that halts and outputs . Finally, is the event that does not halt on input .

We use to represent a computable coding function, in order to biject arbitrary countable sets to the naturals for the purpose of computability.

A reflective oracle is a probabilistic oracle such that for all and , For more on reflective oracles, see Fallenstein et al., 2015 [2].

A function is -computable if there is an index such that for all , we have and That is, represents by probabilistically outputting either or .

For any , a function is -computable if each coordinate for is -computable.

A function is -computable if the corresponding function given by is -computable.

For any point , a probabilistic oracle is compatible with if for all , we have if and if . More generally, for any and any , a probabilistic oracle is compatible with if for all such that and all , we have if and if .

A function is -computable if for each coordinate , there is an index such that whenever is compatible with , we have and

A map is -computably ubiquitous if for every -computable map , there is some such that .

3 Converse Lawvere property

We first need a lemma that tells us that we can replace certain partial -computable functions with total ones when working relative to a reflective oracle. As discussed in the introduction, this contrasts strongly with the situation for computable functions. All of our theorems will make essential use of this lemma.

Lemma 1 (totalizing): There is a computable map such that for all and any reflective oracle , we have and for ,

Proof: We construct using a recursive procedure that ensures that upper-bounds using what may be thought of as repeated subdivision or binary search. This is essentially the same as the function in [3], but we handle computability issues differently. Let be the set of pairs of dyadic rationals such that . We recursively define a stochastic -computable function ; the intent is to have equal if that quantity is in the interval , and take the closest possible value, either or , otherwise. Then, we will be able to define to be .

Construct so that a call first queries , where , and also flips a fair coin . Then, it either outputs , , or the result of a recursive call, as follows: We can now choose so that .

This algorithm upper bounds the probabilities and by binary search. Once the initial call has recursed to , it has already halted outputting with probability , confirming that this is an upper bound since it received answer from a call to . Similarly, it has output with probability , confirming this bound since it received the answer from a call to . Further, since each call to halts without recursing with probability , halts almost surely. Thus, we get the totality property and the bounds for .

Now we can prove our main theorem.

Theorem 1 (converse Lawvere for reflective oracles): Let be a reflective oracle. Then, there is an -computable map such that for all -computable , there is some index such that .

Proof: Using from the totalizing lemma, let Given any -computable , there is some such that Then, and similarly , so .

This theorem gives a computable analogue to the problem posed in [4]. The analogy would be strengthened if we worked in a cartesian closed category where the present notion of -computability gave the morphisms, and where is an exponential object. In addition, the totalizing lemma would have a nice analogue in this setting. I expect that all this can be done using something like an effective topos [6], but I leave this for future work.

4 Recovering Brouwer's fixed point theorem

As mentioned in [4], the intermediate value theorem would follow from the existence of a space with the converse Lawvere property, that is, a space that surjects onto the mapping space . Further, Brouwer's fixed point theorem on the -ball, , would follow from the existence of a topological space with a surjection . We can do something similar to conclude Brouwer's fixed point theorem from the converse Lawvere theorem for reflective oracles. Of course, this is circular; Kakutani's fixed point theorem, a generalization of Brouwer's fixed point theorem, is used to prove the existence of reflective oracles. Still, it is interesting to see how this can be done.

We start with two technical lemmas telling us some basic facts about reflective-oracle-computable functions . Using these, it will be easy to derive Brouwer's fixed point theorem.

Lemma 2 (continuous implies relatively computable): Take and let be continuous. Then, there is a (deterministic) oracle such that is -computable.

Proof: For each coordinate of , each rectangle with rational endpoints, and each pair of rationals with , let be if and otherwise. To see that is -computable, we compute any for any with , and any , making use of and any oracle compatible with .

We proceed by a search process similar to the argument in the totalizing lemma. Start with , and . At each step , perform an exhaustive search for a rectangle and points such that a query to returns for all , a query to any returns 0, a query to returns , and where either and , or and . In the first case, output with probability and continue with probability , and in the second case, output with probability and continue with probability .

By construction, and at each stage . Since is continuous, there is some neighbourhood of on which its image is contained in either or . There are two possibilities to consider. If , then there is some rectangle contained in such a neighbourhood of , and with . This rectangle would be chosen if considered, so the algorithm will move beyond step .

The remaining possibility is that is on the boundary of ; say, . Since was chosen previously though, we know that querying has returned at least once, so . Thus, the algorithm will almost surely eventually accept or another rectangle.

Putting this together, this algorithm almost surely halts, outputting either or . By stage , it has halted outputting with probability and outputting with probability , so overall it outputs with probability . Thus, is -computable.

Lemma 3 (composition): Let be a reflective oracle and let and be -computable. Then, is -computable.

Proof: For each with , take such that witnesses the computability of . Then, if and if , so lets us simulate a probabilistic oracle compatible with . Hence, by the -computability of , for each with , we have a probabilistic -machine that always halts, outputting either or , and that on input outputs with probability .

Theorem 2 (Brouwer's fixed point theorem): Take and . Then, has a fixed point.

Proof: By Lemma 2, we have an oracle such that is -computable. By relativizing the construction of a reflective oracle [2,3] to , we get a reflective oracle above . Notice that is -computable. Letting be the -computable function constructed in the converse Lawvere theorem for reflective oracles, define by The rest will now follow the proof of Lawvere's fixed point theorem [7].

Define by ; this is -computable by Lemma 3. Now, by converse Lawvere theorem, for each coordinate of , there is some such that . Letting , we have so , and so is a fixed point of .

5 Ubiquitous converse Lawvere property

Theorem 3 (ubiquitous converse Lawvere): Let be a reflective oracle. Then, there is an -computable, -computably ubiquitous map .

Proof: This follows by a combination of the recursion theorem and the totalizing lemma. We use the same map from Theorem 1. Let be any -computable map. There is a computable map such that for all , we have and By the recursion theorem, there is some such that . Then,